Merge branch 'main' into add_loop_vcg

Arm/BitVec.lean

@@ -339,6 +339,14 @@ example : split 0xabcd1234#32 8 (by omega) = [0xab#8, 0xcd#8, 0x12#8, 0x34#8] :=
 /-- Get the width of a bitvector. -/
 protected def width (_ : BitVec n) : Nat := n
 
+/-- Convert a bitvector into its hex representation, without leading zeroes.
+
+See `BitVec.toHex` if you do want the leading zeroes.
+
+NOTE: returns only the digits, without a `0x` prefix -/
+def toHexWithoutLeadingZeroes {w} (x : BitVec w) : String :=
+  (Nat.toDigits 16 x.toNat).asString
+
 ----------------------------------------------------------------------
 
 attribute [ext] BitVec

Arm/Exec.lean

@@ -166,3 +166,13 @@ theorem run_onestep (s s': ArmState) (n : Nat) (h_nonneg : 0 < n):
   · cases h_nonneg
   · rename_i n
     simp [run]
+
+/-- helper lemma for automation -/
+theorem stepi_eq_of_fetch_inst_of_decode_raw_inst
+    (s : ArmState) (addr : BitVec 64) (rawInst : BitVec 32) (inst : ArmInst)
+    (h_err    : r .ERR s = .None)
+    (h_pc     : r .PC s = addr)
+    (h_fetch  : fetch_inst addr s = some rawInst)
+    (h_decode : decode_raw_inst rawInst = some inst) :
+    stepi s = exec_inst inst s := by
+  simp only [stepi, h_err, h_pc, h_fetch, h_decode, read_err, read_pc]

Arm/State.lean

@@ -521,6 +521,14 @@ theorem fetch_inst_from_program
     unfold fetch_inst
     simp only
 
+theorem fetch_inst_eq_of_prgram_eq_of_map_find
+    {state : ArmState} {program : Program}
+    {addr : BitVec 64} {inst? : Option (BitVec 32)}
+    (h_program : state.program = program)
+    (h_map : program.find? addr = inst?) :
+    fetch_inst addr state = inst? := by
+  rw [fetch_inst, h_program, h_map]
+
 end Load_program_and_fetch_inst
 
 ----------------------------------------------------------------------

Proofs/AES-GCM/GCMGmultV8Sym.lean

@@ -4,9 +4,7 @@ import Tactics.StepThms
 
 namespace GCMGmultV8Program
 
-#genStepTheorems gcm_gmult_v8_program thmType:="fetch" `state_simp_rules
-#genStepTheorems gcm_gmult_v8_program thmType:="decodeExec" `state_simp_rules
-#genStepTheorems gcm_gmult_v8_program thmType:="step" `state_simp_rules
+#genStepEqTheorems gcm_gmult_v8_program
 
 theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     (h_s0_program : s0.program = gcm_gmult_v8_program)

Proofs/Experiments/Abs.lean

@@ -6,6 +6,8 @@ Author(s): Shilpi Goel, Siddharth Bhat
 The goal is to prove that this program implements absolute value correctly.
 -/
 import Arm
+import Tactics.StepThms
+import Tactics.Sym
 
 namespace Abs
 
@@ -19,14 +21,21 @@ def program : Program :=
 
 def spec (x : BitVec 32) : BitVec 32 := BitVec.ofNat 32 x.toInt.natAbs
 
+#genStepEqTheorems program
+
 theorem correct
   {s0 sf : ArmState}
   (h_s0_pc : read_pc s0 = 0x4005d0#64)
   (h_s0_program : s0.program = program)
   (h_s0_err : read_err s0 = StateError.None)
+  (h_s0_sp : CheckSPAlignment s0)
   (h_run : sf = run program.length s0) :
   read_gpr 32 0 sf = spec (read_gpr 32 0 s0) ∧
-  read_err sf = StateError.None := by sorry
+  read_err sf = StateError.None := by
+  simp (config := {ground := true}) at h_run
+
+  sym1_n 5
+  sorry
 
 /-- info: 'Abs.correct' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms correct

Proofs/Popcount32.lean

@@ -66,14 +66,7 @@ def popcount32_program : Program :=
    (0x40061c#64 , 0xd65f03c0#32)] -- ret
 
 
-#genStepTheorems popcount32_program thmType:="fetch"
-
--- #guard_msgs in
--- #check popcount32_fetch_0x4005b4
-
-#genStepTheorems popcount32_program thmType:="decodeExec"
-
-#genStepTheorems popcount32_program thmType:="step" `state_simp_rules
+#genStepEqTheorems popcount32_program
 
 theorem popcount32_sym_no_error (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x4005b4#64)
@@ -130,16 +123,15 @@ theorem popcount32_sym_no_error (s0 s_final : ArmState)
 section Tests
 
 /--
-info: popcount32_program.stepi_0x4005c0 (s sn : ArmState) (h_program : s.program = popcount32_program)
+info: popcount32_program.stepi_eq_0x4005c0 {s : ArmState} (h_program : s.program = popcount32_program)
   (h_pc : r StateField.PC s = 4195776#64) (h_err : r StateField.ERR s = StateError.None) :
-  (sn = stepi s) =
-    (sn =
-      w StateField.PC (4195780#64)
-        (w (StateField.GPR 0#5)
-          (zeroExtend 64 ((zeroExtend 32 (r (StateField.GPR 0#5) s)).rotateRight 1) &&& 4294967295#64 &&& 2147483647#64)
-          s))
+  stepi s =
+    w StateField.PC (4195780#64)
+      (w (StateField.GPR 0#5)
+        (zeroExtend 64 ((zeroExtend 32 (r (StateField.GPR 0#5) s)).rotateRight 1) &&& 4294967295#64 &&& 2147483647#64)
+        s)
 -/
-#guard_msgs in #check popcount32_program.stepi_0x4005c0
+#guard_msgs in #check popcount32_program.stepi_eq_0x4005c0
 
 end Tests
 

Proofs/SHA512/Sha512StepLemmas.lean

@@ -1,17 +1,15 @@
-import Proofs.SHA512.Sha512FetchLemmas
-import Proofs.SHA512.Sha512DecodeExecLemmas
 import Proofs.SHA512.Sha512Program
--- import Tests.SHA2.SHA512ProgramTest
+import Tactics.StepThms
 
 -- set_option trace.gen_step.debug.heartBeats true in
 -- set_option trace.gen_step.print_names true in
 set_option maxHeartbeats 2000000 in
-#genStepTheorems sha512_program thmType:="step" `state_simp_rules
+#genStepEqTheorems sha512_program
 
 /--
-info: sha512_program.stepi_0x126c90 (s sn : ArmState) (h_program : s.program = sha512_program)
+info: sha512_program.stepi_eq_0x126c90 {s : ArmState} (h_program : s.program = sha512_program)
   (h_pc : r StateField.PC s = 1207440#64) (h_err : r StateField.ERR s = StateError.None) :
-  (sn = stepi s) = (sn = w StateField.PC (if ¬r (StateField.GPR 2#5) s = 0#64 then 1205504#64 else 1207444#64) s)
+  stepi s = w StateField.PC (if ¬r (StateField.GPR 2#5) s = 0#64 then 1205504#64 else 1207444#64) s
 -/
 #guard_msgs in
-#check sha512_program.stepi_0x126c90
+#check sha512_program.stepi_eq_0x126c90

Tactics/Common.lean

@@ -55,7 +55,7 @@ def getBitVecString? (e : Expr) (hex : Bool := false): MetaM (Option String) :=
   | some ⟨_, value⟩ =>
     if hex then
       -- We don't want leading zeroes here.
-      return some (Nat.toDigits 16 value.toNat).asString
+      return some value.toHexWithoutLeadingZeroes
     else
       return some (ToString.toString value.toNat)
   | none => return none
@@ -88,13 +88,13 @@ that additionally recognizes:
 -- TODO: should this be upstreamed to core?
 def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) :=
   match_expr e with
-    | BitVec.ofFin _ i => OptionT.run do
-      let ⟨n, i⟩ ← getFinValue? i
-      let n' := Nat.log2 n
-      if h : n = 2^n' then
-        return ⟨n', .ofFin (Fin.cast h i)⟩
-      else
-        failure
+    | BitVec.ofFin w i => OptionT.run do
+      let w ← getNatValue? w
+      let v ← do
+        match_expr i with
+          | Fin.mk _n v _h  => getNatValue? v
+          | _               => pure (← getFinValue? i).2.val
+      return ⟨w, BitVec.ofNat w v⟩
     | _ => Lean.Meta.getBitVecValue? e
 
 /-- Given a ground term `e` of type `Nat`, fully reduce it,
@@ -115,21 +115,53 @@ which was obtained by reducing:\n\t{e}"
 reduce an expression `e` (of type `BitVec w`) to be of the form `?n#w`,
 and then reflect `?n` to build the meta-level bitvector -/
 def reflectBitVecLiteral (w : Nat) (e : Expr) : MetaM (BitVec w) := do
-  if e.hasFVar then
+  if e.hasFVar || e.hasMVar then
     throwError "Expected a ground term, but {e} has free variables"
 
-  if let some ⟨n, x⟩ ← _root_.getBitVecValue? e then
-    if h : n = w then
-      return x.cast h
-    else
-      throwError "Expected a bitvector of width {w}, but\n\t{e}\nhas width {n}"
+  let some ⟨n, x⟩ ← _root_.getBitVecValue? e
+    | throwError "Failed to reflect:\n\t{e}\ninto a BitVec"
 
-  let x ← mkFreshExprMVar (Expr.const ``Nat [])
-  let e' ← mkAppM ``BitVec.ofNat #[toExpr w, x]
-  if (←isDefEq e e') then
-    return BitVec.ofNat w (← reflectNatLiteral x)
+  if h : n = w then
+    return x.cast h
   else
-    throwError "Failed to unify, expected:\n\t{e'}\nbut found:\n\t{e'}"
+    throwError "Expected a bitvector of width {w}, but\n\t{e}\nhas width {n}"
+
+/-! ## Hypothesis types -/
+namespace SymContext
+
+/-- `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 :=
+  mkAppN (mkConst ``Eq [1]) #[
+    mkConst ``StateError,
+    mkApp2 (.const ``r []) (.const ``StateField.ERR []) state,
+    .const ``StateError.None []
+  ]
+
+/-- `h_sp_type state` returns an Expr for `CheckSPAlignment <state>`,
+the expected type of `h_sp` -/
+def h_sp_type (state : Expr) : Expr :=
+  mkApp (.const ``CheckSPAlignment []) state
+
+/-- `h_sp_type state` returns an Expr for `<state>.program = <program>`,
+the expected type of `h_program` -/
+def h_program_type (state program : Expr) : Expr :=
+  mkAppN (mkConst ``Eq [1]) #[
+    mkConst ``Program,
+    mkApp (mkConst ``ArmState.program) state,
+    program
+  ]
+
+/-- `h_pc_type state` returns an Expr for `r .PC <state> = <address>`,
+the expected type of `h_pc` -/
+def h_pc_type (state address : Expr) : Expr :=
+  mkAppN (mkConst ``Eq [1]) #[
+    mkApp (mkConst ``BitVec) (toExpr 64),
+    mkApp2 (mkConst ``r) (mkConst ``StateField.PC) state,
+    address
+  ]
+
+end SymContext
 
 /-! ## Local Context Search -/
 
@@ -162,7 +194,7 @@ Throws an error if no such hypothesis could. -/
 def findProgramHyp (state : Expr) : MetaM (LocalDecl × Name) := do
   -- Try to find `h_program`, and infer `program` from it
   let program ← mkFreshExprMVar none
-  let h_program_type ← mkEq (← mkAppM ``ArmState.program #[state]) program
+  let h_program_type := SymContext.h_program_type state program
   let h_program ← findLocalDeclOfTypeOrError h_program_type
 
   -- Assert that `program` is a(n application of a) constant, and find its name

Tactics/Reflect/FetchAndDecode.lean

@@ -13,24 +13,15 @@ open Elab.Tactic Elab.Term
 initialize
   Lean.registerTraceClass `Sym.reduceFetchInst
 
-theorem fetch_inst_eq_of_prgram_eq_of_map_find
-    {state : ArmState} {program : Program}
-    {addr : BitVec 64} {inst? : Option (BitVec 32)}
-    (h_program : state.program = program)
-    (h_map : program.find? addr = inst?) :
-    fetch_inst addr state = inst? := by
-  rw [fetch_inst, h_program, h_map]
-
-def reduceFetchInst? (addr : Expr) (s : Expr) :
+def reduceFetchInst? (addr : BitVec 64) (s : Expr) :
     MetaM (BitVec 32 × Expr) := do
-  let addr ← reflectBitVecLiteral 64 addr
   let ⟨programHyp, program⟩ ← findProgramHyp s
   let programInfo ← try ProgramInfo.lookupOrGenerate program catch err =>
     throwErrorAt
       err.getRef
       "Could not generate ProgramInfo for {program}:\n\n{err.toMessageData}"
 
-  let some rawInst := programInfo.getRawInstrAt? addr
+  let some rawInst := programInfo.getRawInstAt? addr
     | throwError "No instruction found at address {addr}"
 
   trace[Sym.reduceFetchInst] "{Lean.checkEmoji} reduced to: {rawInst}"
@@ -54,6 +45,7 @@ simproc reduceFetchInst (fetch_inst _ _) := fun e => do
   trace[Sym.reduceFetchInst] "⚙️ simplifying {e}"
   let_expr fetch_inst addr s := e
     | return .continue
+  let addr ← reflectBitVecLiteral 64 addr
 
   try
     let ⟨x, proof?⟩ ← reduceFetchInst? addr s