chore: remove old versions of the sym tactic, and rename the new sym1_n tactic to sym_n

Proofs/AES-GCM/GCMGmultV8Sym.lean

@@ -13,8 +13,10 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     (h_s0_sp_aligned : CheckSPAlignment s0)
     (h_run : sf = run gcm_gmult_v8_program.length s0) :
     read_err sf = .None := by
-  simp (config := {ground := true}) only [Option.some.injEq] at h_s0_pc h_run
-  sym1_n 27
+  simp (config := {ground := true}) only at h_s0_pc
+  -- ^^ Still needed, because `gcm_gmult_v8_program.min` is somehow
+  --    unable to be reflected
+  sym_n 27
   subst h_run
   assumption
   done

Proofs/Experiments/Abs.lean

@@ -34,7 +34,7 @@ theorem correct
   read_err sf = StateError.None := by
   simp (config := {ground := true}) at h_run
 
-  sym1_n 5
+  sym_n 5
   sorry
 
 /-- info: 'Abs.correct' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] -/

Proofs/Experiments/SHA512MemoryAliasing.lean

@@ -85,7 +85,7 @@ theorem sha512_block_armv8_prelude_sym_ctx_access (s0 : ArmState)
   -- Prelude
   -- simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  -- sym1_n 4
+  -- sym_n 4
   sorry
 
 /-

Proofs/MultiInsts.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.Exec
 import Arm.Util
 import Tactics.Sym
+import Tactics.StepThms
 
 namespace multi_insts_proofs
 
@@ -18,6 +19,8 @@ def test_program : Program :=
     (0x126514#64 , 0x4ea21c5c#32),      --  mov     v28.16b, v2.16b
     (0x126518#64 , 0x4ea31c7d#32)]      --  mov     v29.16b, v3.16b
 
+#genStepEqTheorems test_program
+
 theorem small_asm_snippet_sym_experiment_1 (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x12650c#64)
   (h_s0_program : s0.program = test_program)
@@ -29,11 +32,11 @@ theorem small_asm_snippet_sym_experiment_1 (s0 s_final : ArmState)
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  sym_i_n 0 4
+  sym_n 4
   -- Final Steps
   unfold run at h_run
   subst s_final
-  simp_all (config := {decide := true}) only [@zeroExtend_eq 128, state_simp_rules, minimal_theory, bitvec_rules]  
+  simp_all (config := {decide := true}) only [@zeroExtend_eq 128, state_simp_rules, minimal_theory, bitvec_rules]
   done
 
 /-

Proofs/Popcount32.lean

@@ -78,7 +78,7 @@ theorem popcount32_sym_no_error (s0 s_final : ArmState)
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  sym1_n 27
+  sym_n 27
   try (clear h_step_1 h_step_2 h_step_3 h_step_4;
        clear h_step_5 h_step_6 h_step_7 h_step_8;
        clear h_step_9 h_step_10;
@@ -104,7 +104,7 @@ theorem popcount32_sym_no_error (s0 s_final : ArmState)
 --   -- Prelude
 --   simp_all only [state_simp_rules, -h_run]
 --   -- Symbolic Simulation
---   sym1_n 27
+--   sym_n 27
 --   try (clear h_step_1 h_step_2 h_step_3 h_step_4;
 --        clear h_step_5 h_step_6 h_step_7 h_step_8;
 --        clear h_step_9 h_step_10;

Proofs/SHA512/Sha512Sym.lean

@@ -26,7 +26,7 @@ theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState)
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  sym1_n 11
+  sym_n 11
   try (clear h_step_1 h_step_2 h_step_3 h_step_4;
        clear h_step_5 h_step_6 h_step_7 h_step_8;
        clear h_step_9 h_step_10 h_step_11)
@@ -37,7 +37,7 @@ theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState)
   done
 
 /-
-  -- sym1_n 1
+  -- sym_n 1
   -- let s0_x31 := (r (StateField.GPR 31#5) s0)
   -- simp only [state_value] at s0_x31
   -- have h_s0_x31 : s0_x31 = (r (StateField.GPR 31#5) s0) := by rfl

Proofs/SHA512/Sha512_block_armv8.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.Exec
 import Arm.Util
 import Tactics.Sym
+import Tactics.StepThms
 import Tests.SHA2.SHA512ProgramTest
 
 section SHA512_proof
@@ -25,6 +26,8 @@ def sha512_program_test_1 : Program :=
      (0x126544#64 , 0xce678af0#32)       --  sha512su1       v16.2d, v23.2d, v7.2d
      ]
 
+#genStepEqTheorems sha512_program_test_1
+
 -- set_option profiler true in
 -- set_option trace.profiler.output "new_sym.log" in
 -- set_option trace.profiler.output.pp true in
@@ -60,6 +63,8 @@ def sha512_program_test_2 : Program :=
      (0x12654c#64 , 0xce608423#32)       --  sha512h2        q3, q1, v0
      ]
 
+#genStepEqTheorems sha512_program_test_2
+
 -- set_option profiler true in
 theorem sha512_program_test_2_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x126538#64)
@@ -89,6 +94,8 @@ def sha512_program_test_3 : Program :=
     (0x1264cc#64 , 0x4cdf2034#32)       --  ld1     {v20.16b-v23.16b}, [x1], #64
   ]
 
+#genStepEqTheorems sha512_program_test_3
+
 -- set_option profiler true in
 -- set_option pp.deepTerms false in
 -- set_option pp.deepTerms.threshold 10 in

Proofs/Simple.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel, Nathan Wetzler
 import Arm.Exec
 import Arm.Util
 import Tactics.Sym
+import Tactics.StepThms
 
 section simple
 
@@ -15,6 +16,8 @@ def eor_program : Program :=
   def_program
   [(0x4005a8#64 , 0xca000000#32)]      --  eor	x0, x0, x0
 
+#genStepEqTheorems eor_program
+
 theorem small_asm_snippet_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x4005a8#64)
   (h_s0_program : s0.program = eor_program)

Tactics/Common.lean

@@ -129,6 +129,14 @@ def reflectBitVecLiteral (w : Nat) (e : Expr) : MetaM (BitVec w) := do
 /-! ## Hypothesis types -/
 namespace SymContext
 
+/-- `h_run_type state` returns an Expr for
+`<finalState> = run <steps> <initialState>`, the expected type of `h_run` -/
+def h_run_type (finalState steps initialState : Expr) : Expr :=
+  mkApp3 (mkConst ``Eq [1])
+    (mkConst ``ArmState)
+    finalState
+    (mkApp2 (mkConst ``_root_.run) steps initialState)
+
 /-- `h_err_type state` returns an Expr for `r .ERR <state> = .None`,
 the expected type of `h_err` -/
 def h_err_type (state : Expr) : Expr :=

Tactics/Sym.lean

@@ -10,14 +10,13 @@ import Tactics.ExecInst
 import Tactics.ChangeHyps
 import Tactics.SymContext
 
-import Lean.Elab
-import Lean.Expr
+import Lean
 
 initialize
   Lean.registerTraceClass `Sym
 
 open BitVec
-open Lean (FVarId TSyntax logWarning)
+open Lean
 open Lean.Elab.Tactic (TacticM evalTactic withMainContext)
 
 /-- A wrapper around `evalTactic` that traces the passed tactic script and
@@ -47,53 +46,8 @@ macro "init_next_step" h_run:ident h_step:ident sn:ident : tactic =>
      clear $h_run:ident; rename_i $h_run:ident
      simp (config := {ground := true}) only at $h_run:ident))
 
-def sym_one (curr_state_number : Nat) : TacticM Unit :=
-  withMainContext do
-    let n_str := toString curr_state_number
-    let n'_str := toString (curr_state_number + 1)
-    let mk_name (s : String) : Lean.Name :=
-      Lean.Name.mkStr Lean.Name.anonymous s
-    -- h_st: prefix of user names of hypotheses about state st
-    let h_st_prefix := Lean.Syntax.mkStrLit ("h_s" ++ n_str)
-    -- h_st_program: name of the hypothesis about the program at state st
-    let h_st_program := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_program"))
-    let h_st_pc := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_pc"))
-    let h_st_err := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_err"))
-    let h_st_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_sp_aligned"))
-    -- st': name of the next state
-    let st' := Lean.mkIdent (mk_name ("s" ++ n'_str))
-    -- h_run: name of the hypothesis with the `run` function
-    let h_run := Lean.mkIdent (mk_name "h_run")
-    -- h_step_n': name of the hypothesis with the `stepi` function
-    let h_step_n' := Lean.mkIdent (mk_name ("h_step_" ++ n'_str))
-    evalTactic (←
-      `(tactic|
-         (init_next_step $h_run:ident $h_step_n':ident $st':ident
-          -- Simulate one instruction
-          fetch_and_decode $h_step_n':ident $h_st_prefix:str
-          -- (try clear $h_step_n:ident)
-          exec_inst $h_step_n':ident $h_st_prefix:str
-          intro_fetch_decode_lemmas $h_step_n':ident $h_st_program:ident $h_st_prefix:str
-          (try clear $h_st_pc:ident $h_st_program:ident $h_st_err:ident $h_st_sp_aligned:ident)
-          -- intro_change_hyps $h_step_n':ident $h_st_prefix:str
-          -- (try clear $h_step_n':ident)
-      )))
-
--- sym_n tactic symbolically simulates n instructions.
-elab "sym_n" n:num : tactic => do
-  for i in List.range n.getNat do
-    sym_one i
-
--- sym_n tactic symbolically simulates n instructions from
--- state number i.
-elab "sym_i_n" i:num n:num : tactic => do
-  for j in List.range n.getNat do
-    sym_one (i.getNat + j)
-
 section stepiTac
 
-open Lean Elab Tactic Expr Meta
-
 /-- Apply the relevant pre-generated stepi lemma to replace a local hypothesis
   `h_step : ?s' = stepi ?s`
 with an hypothesis in terms of `w` and `write_mem`
@@ -142,36 +96,14 @@ def sym1 (c : SymContext) : TacticM SymContext :=
     return c.next
 
 
-open Lean (Name) in
-/-- `sym1_i_n i n h_program` will symbolically evaluate a program for `n` steps,
-starting from state `i`, where `h_program` is an assumption of the form:
-`s{i}.program = someConcreteProgam`.
-
-The context is assumed to contain hypotheses
-```
-h_s{i}_err : r StateField.ERR s{i} = .None
-h_s{i}_pc  : r StateField.PC  s{i} = $PC
-h_run      : sf = run $STEPS s0
-```
-Where $PC and $STEPS are concrete constants.
-Note that the tactic will search for assumption of *exactly* these names,
-it won't search by def-eq -/
-@[deprecated "Use `sym1_n` instead"]
-elab "sym1_i_n" i:num n:num _program:(ident)? : tactic => do
-  Lean.Elab.Tactic.evalTactic (← `(tactic|
-    simp (config := {failIfUnchanged := false}) only [state_simp_rules] at *
-  ))
-  let mut c := SymContext.default i.getNat
-  for _ in List.range n.getNat do
-    c ← sym1 c
-
-/- used in `sym1_n` tactic -/
+/- used in `sym_n` tactic -/
 syntax sym_at := "at" ident
 
+open Elab.Term (elabTerm) in
 /--
-`sym1_n n` will symbolically evaluate a program for `n` steps.
+`sym_n n` will symbolically evaluate a program for `n` steps.
 Alternatively,
-  `sym1_n n at s` does the same, with `s` as initial state
+  `sym_n n at s` does the same, with `s` as initial state
 
 If `s` is not passed, the initial state is inferred from the local context
 
@@ -191,18 +123,16 @@ Hypotheses `h_err` and `h_sp` may be missing,
 in which case a new goal of the appropriate type will be added.
 The other hypotheses *must* be present,
 since we infer required information from their types. -/
-elab "sym1_n" n:num s:(sym_at)? : tactic =>
+elab "sym_n" n:num s:(sym_at)? : tactic =>
   let s := s.map fun
     | `(sym_at|at $s:ident) => s.getId
     | _ => panic! "Unexpected syntax: {s}"
   Lean.Elab.Tactic.withMainContext <| do
-    Lean.Elab.Tactic.evalTactic (← `(tactic|
-      simp (config := {failIfUnchanged := false}) only [state_simp_rules] at *
-    ))
-
     let mut c ← SymContext.fromLocalContext s
     c ← c.addGoalsForMissingHypotheses
+    c.canonicalizeHypothesisTypes
 
+    -- Check that we are not asked to simulate more steps than available
     let n ←
       if n.getNat ≤ c.runSteps then
         pure n.getNat
@@ -211,6 +141,18 @@ elab "sym1_n" n:num s:(sym_at)? : tactic =>
         logWarning m!"Symbolic simulation using {h_run} is limited to at most {c.runSteps} steps"
         pure c.runSteps
 
+    -- Check that step theorems have been pre-generated
+    try
+      let pc := c.pc.toHexWithoutLeadingZeroes
+      let step_thm := Name.str c.program ("stepi_eq_0x" ++ pc)
+      let _ ← getConstInfo step_thm
+    catch err =>
+      throwErrorAt err.getRef "{err.toMessageData}\n
+Did you remember to generate step theorems with:
+  #generateStepEqTheorems {c.program}"
+-- TODO: can we make this error ^^ into a `Try this:` suggestion that
+--       automatically adds the right command just before the theorem?
+
     -- The main loop
     for _ in List.range n do
       c ← sym1 c