Refactoring tactics for symbolic simulation

Proofs/MultiInsts.lean

@@ -21,17 +21,16 @@ def test_program : Program :=
 theorem small_asm_snippet_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x12650c#64)
   (h_s0_program : s0.program = test_program)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 4 s0) :
   read_sfp 128 26#5 s_final = read_sfp 128 0#5 s0 ∧
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Wrapping up the result:
   unfold run at h_run
-  subst s_final s4
   simp_all (config := {decide := true}) only [state_simp_rules, minimal_theory, bitvec_rules]
   rw [@zeroExtend_eq 128]
   done

Proofs/Sha512_block_armv8.lean

@@ -26,22 +26,24 @@ def sha512_program_test_1 : Program :=
      ]
 
 -- set_option profiler true in
+-- set_option trace.profiler.output "new_sym.log" in
+-- set_option trace.profiler.output.pp true in
 -- set_option pp.deepTerms true in
 theorem sha512_program_test_1_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x126538#64)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_program : s0.program = sha512_program_test_1)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 4 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Final steps
   unfold run at h_run
-  subst s_final s4
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  subst s_final
+  simp only [h_s4_err]
   done
 
 ----------------------------------------------------------------------
@@ -62,17 +64,16 @@ def sha512_program_test_2 : Program :=
 theorem sha512_program_test_2_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x126538#64)
   (h_s0_program : s0.program = sha512_program_test_2)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 6 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 6 h_s0_program
+  sym_n 6
   -- Final steps
   unfold run at h_run
-  subst s_final s6
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  simp only [h_run, h_s6_err]
   done
 
 ----------------------------------------------------------------------
@@ -91,7 +92,7 @@ def sha512_program_test_3 : Program :=
 set_option pp.deepTerms false in
 set_option pp.deepTerms.threshold 10 in
 theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_pc : read_pc s0 = 0x1264c0#64)
   (h_s0_program : s0.program = sha512_program_test_3)
@@ -100,11 +101,11 @@ theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Final steps
   unfold run at h_run
-  subst s_final s4
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  subst s_final
+  apply h_s4_err
   done
 
 ----------------------------------------------------------------------
@@ -113,73 +114,43 @@ theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
 -- simulation test for the AWS-LC production SHA512 code (the program
 -- we'd like to verify).
 
-example : StateError.None = StateError.None := by decide
-
 -- set_option profiler true in
 -- set_option profiler.threshold 10 in
+-- set_option trace.profiler.output.pp true in
 theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_pc : read_pc s0 = 0x1264c0#64)
   (h_s0_program : s0.program = sha512_program_map)
-  (h_run : s_final = run 32 s0) :
+  (h_run : s_final = run 10 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  -- sym_n 5 h_s0_program
-  -- sym_i_n 0 1 h_s0_program
-  -- init_next_step h_run
-  -- rename_i s1 h_step_1 h_run
-  -- -- fetch_and_decode_inst h_step_1 h_s0_program
-  -- simp only [*, stepi, state_simp_rules, minimal_theory, bitvec_rules] at h_step_1
-  -- rw [fetch_inst_from_program] at h_step_1
-  -- simp only [h_s0_program] at h_step_1
-  -- conv at h_step_1 =>
-  --   pattern Map.find? _ _
-  --   tactic => set_option maxRecDepth 3000 in
-  --             simp (config := {ground := true}) only [reduceMapFind?]
-  -- (try dsimp only at h_step_1)
-  -- conv at h_step_1 =>
-  --   pattern decode_raw_inst _
-  --   tactic =>
-  --     simp (config := {ground := true}) only
-  -- (try dsimp only at h_step_1)
-  -- simp (config := {decide := true}) only
-  --   [exec_inst, state_simp_rules, minimal_theory]
-  --   at h_step_1
-  sym_i_n 0 1 h_s0_program
-  init_next_step h_run
-  rename_i s2 h_step_2 h_run
-  -- project_program_and_error_fields h_step_1
-  -- fetch_and_decode_inst h_step_2 h_s0_program
-  simp only [stepi, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2
-  rw [fetch_inst_from_program] at h_step_2
-  have h_s1_program : s1.program = s0.program := by
-    simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
-  have h_s1_err : r StateField.ERR s1 = StateError.None := by
-    simp only [*, state_simp_rules, minimal_theory, bitvec_rules]
-  have h_s1_pc : r StateField.PC s1 = (1205444#64) := by
-    simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
-  simp only [h_s0_program, h_s1_program, h_s1_err, h_s1_pc] at h_step_2
-  conv at h_step_2 =>
-    pattern Map.find? _ _
-    tactic => set_option maxRecDepth 3000 in
-              simp only [reduceMapFind?]
-  (try dsimp only at h_step_2)
-  conv at h_step_2 =>
-    pattern decode_raw_inst _
-    tactic =>
-      simp (config := {ground := true}) only
-  (try dsimp only at h_step_2)
-  (try clear h_s1_program h_s1_err)
-  -- exec_inst h_step_2
-  explode_step h_step_1
-  have h_s1_gpr31 : r (StateField.GPR 31#5) s1 = (r (StateField.GPR 31#5) s0 + 18446744073709551600#64) := by
-    simp_all only [stepi, state_simp_rules, minimal_theory, bitvec_rules]
-  simp (config := { decide := true }) only [*, -h_step_1, exec_inst, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2
-  (try (repeat simp (config := {ground := true}) only [↓reduceIte, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2))
-
+  -- sym_n 32
+  -- sym_n 10
+  -- -- Final Steps
+  -- unfold run at h_run
+  -- simp only [h_run, h_s10_err]
+  -- done
+  sym_n 10
+  -- sym_i_n 0 1
+  -- sym_i_n 1 1
+  -- sym_i_n 2 1
+  -- sym_i_n 3 1
+  -- sym_i_n 4 1
+  -- sym_i_n 5 1
+  -- sym_i_n 6 1
+  -- sym_i_n 7 1
+  -- sym_i_n 8 1
+  -- sym_i_n 9 1
+  -- Final Steps
+  unfold run at h_run
+  subst s_final
+  -- save
+  -- rw [h_s10_err]
+  -- apply h_s10_err
+  -- done
   sorry
 
 ----------------------------------------------------------------------

Tactics.lean

@@ -7,3 +7,4 @@ Author(s): Shilpi Goel
 -- Import modules here that should be built as part of the library.
 import «Tactics».Sym
 import «Tactics».ExplodeStep
+

Tactics/Common.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
+
+import Lean
+import Arm.Exec
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+
+/- Obtain `Array α` from `Array (Option α)` by discarding any `none`
+elements. -/
+private def optionArraytoArray (array : Array (Option α)) : Array α :=
+  Array.foldl (fun acc val =>
+    match val with
+    | none => acc
+    | some v => acc.append #[v])
+  #[] array
+
+/- Find all declarations in the `LocalContext` whose username begins
+with `pfxUserName`. -/
+def filterDeclsWithPrefix (lctx : LocalContext) (pfxUserName : Name)
+  : (Array LocalDecl) :=
+  optionArraytoArray
+  (PersistentArray.toArray
+    (PersistentArray.filter
+      lctx.decls
+      (fun decl =>
+        match decl with
+          | none      => false
+          | some decl => String.isPrefixOf (toString pfxUserName)
+                                           (toString decl.userName))))

Tactics/ExecInst.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
+import Arm.Exec
+import Tactics.Common
+import Tactics.Simp
+import Lean
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+----------------------------------------------------------------------
+
+def execInst (goal : MVarId) (h_step : Expr) (hyp_prefix : String)
+  : TacticM Bool := goal.withContext do
+  -- Find all the FVars in the local context whose name begins with
+  -- hyp_prefix.
+  let lctx ← getLCtx
+  let matching_decls := filterDeclsWithPrefix lctx hyp_prefix.toName
+  -- logInfo m!"matching_decls: {matching_decls[0]!.userName}"
+  let (ctx, simprocs) ←
+    LNSymSimpContext (config := {decide := true, ground := true})
+                     (simp_attrs := #[`minimal_theory, `bitvec_rules, `state_simp_rules])
+                     (decls_to_unfold := #[``exec_inst])
+                     (thms := #[])
+                     (decls := matching_decls)
+                     (simprocs := #[``reduceIte])
+  let maybe_goal ← LNSymSimp goal ctx simprocs (fvarid := h_step.fvarId!)
+  match maybe_goal with
+  | none =>
+    logInfo m!"[execInst] The goal appears to be solved, but this tactic \
+                  is not a finishing tactic! Something went wrong?"
+    return false
+  | some goal' =>
+    replaceMainGoal [goal']
+    return true
+
+def execInstElab (h_step : Name) (hyp_prefix : String) : TacticM Unit :=
+  withMainContext
+  (do
+    let h_step ← getFVarFromUserName h_step
+    let success ← execInst (← getMainGoal) h_step hyp_prefix
+    if ! success then
+      failure)
+
+elab "exec_inst" h_step:ident hyp_prefix:str : tactic =>
+  execInstElab (h_step.getId) (hyp_prefix.getString)
+
+----------------------------------------------------------------------

Tactics/ExplodeStep.lean

@@ -124,12 +124,6 @@ partial def explodeWriteNest (goal : MVarId)
               match p_simp? with
               | none => []
               | some (_, p_simp_mvarid) => [p_simp_mvarid]
-            -- let new_goals ←
-            --   evalTacticAt
-            --     (← `(tactic|
-            --           (simp (config := {decide := true}) only
-            --                        [state_simp_rules, minimal_theory, bitvec_rules])))
-            --     p
             -- logInfo m!"new_goals: {new_goals}"
             let (_, goal') ← MVarId.intro1P $ ← Lean.MVarId.assert goal name new_prop_type new_prop_val
             explodeWriteNest goal' st_var rest (field_str :: seen_fields) (rest_goals ++ new_goals)
@@ -226,7 +220,7 @@ example (s0 s1 : ArmState)
   (h : s1 = w (StateField.GPR 31#5) 12#64
               (w StateField.PC 1#64
                 (w (StateField.GPR 31#5) 13#64 s0))) :
-  r StateField.PC s1 = 1#64 := by
+  (r StateField.PC s1) + 1#64 = 2#64 := by
   explode_step h
-  assumption
+  simp (config := {decide := true}) [h_s1_pc]
   done