From a52babad87c773baee21acd54028e12684709c89 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 4 Sep 2024 14:58:45 -0500 Subject: [PATCH] feat: efficient axiomatization of effects (#129) ### Description: We've built a new datastructure `AxEffects`, which stores a map from `StateField` to two `Expr`s: the current value of that field, and a proof that `r = `, together with other assorted proofs related to axiomatic effects. We then incorporate this `AxEffects` into `sym_n`, replacing and superseding `intro_fetch_decode`. This has two benefits: `AxEffects` is more complete, and it is *much* faster. Fully simulating `gcm_gmult_v8_program` (assuming step theorems have been pre-generated) used to take around 3.5 seconds, with this PR it takes only 0.5 seconds: a 7x speedup! - In the process, we've proven that `Abs` correctly implements its spec - No longer is a `CheckSPAlignment` goal added by default. Instead, we only add `CheckSPAlignment` goals if the initial state was known to be aligned, and there is some write to the SP of which alignment could not be automatically proven. For now, this goal is added eagerly, without trying to determine if this fact is actually needed for further simulation. Trying to be smarter about this is left for future PRs. ### Testing: `make all` works locally ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Siddharth Co-authored-by: Shilpi Goel --- Arm/BitVec.lean | 5 + Arm/Insts/Common.lean | 14 + Arm/State.lean | 85 ++++- Proofs/Experiments/Abs/Abs.lean | 34 +- Tactics/Attr.lean | 13 + Tactics/Common.lean | 35 ++ Tactics/Reflect/AxEffects.lean | 624 +++++++++++++++++++++++++++++++ Tactics/Reflect/ProgramInfo.lean | 4 +- Tactics/Sym.lean | 124 +++++- Tactics/SymContext.lean | 56 ++- Tests/Tactics/Sym.lean | 28 +- 11 files changed, 985 insertions(+), 37 deletions(-) create mode 100644 Tactics/Reflect/AxEffects.lean diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index 12a75b1e..1d47a9a9 100644 --- a/Arm/BitVec.lean +++ b/Arm/BitVec.lean @@ -555,6 +555,11 @@ protected theorem extract_lsb_of_zeroExtend (x : BitVec n) (h : j < i) : simp_all omega +@[bitvec_rules, simp] +theorem zero_append {w} (x : BitVec 0) (y : BitVec w) : + x ++ y = y.cast (by simp) := by + apply eq_of_getLsb_eq; simp; omega + @[bitvec_rules] theorem empty_bitvector_append_left (x : BitVec n) (h : 0 + n = n) : diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 2f9431e1..b670f3a2 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -144,6 +144,20 @@ theorem CheckSPAlignment_AddWithCarry_64_4 (st : ArmState) (y : BitVec 64) (carr simp_all only [CheckSPAlignment, read_gpr, zeroExtend_eq, Nat.sub_zero, add_eq, Aligned_AddWithCarry_64_4] +@[state_simp_rules] +theorem CheckSPAlignment_of_r_sp_eq {s s' : ArmState} + (h_eq : r (StateField.GPR 31#5) s' = r (StateField.GPR 31#5) s) + (h_sp : CheckSPAlignment s) : + CheckSPAlignment s' := by + simpa only [CheckSPAlignment, read_gpr, h_eq] using h_sp + +@[state_simp_rules] +theorem CheckSPAlignment_of_r_sp_aligned {s : ArmState} {value} + (h_eq : r (StateField.GPR 31#5) s = value) + (h_aligned : Aligned value 4) : + CheckSPAlignment s := by + simp only [CheckSPAlignment, read_gpr, h_eq, zeroExtend_eq, h_aligned] + ---------------------------------------------------------------------- inductive ShiftType where diff --git a/Arm/State.lean b/Arm/State.lean index 6cb26b97..eaf7347c 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -98,7 +98,7 @@ inductive PFlag where | Z : PFlag | C : PFlag | V : PFlag -deriving DecidableEq, Repr +deriving DecidableEq, Repr, Hashable instance : ToString PFlag := ⟨fun p => match p with @@ -255,7 +255,50 @@ inductive StateField where | PC : StateField | FLAG : PFlag → StateField | ERR : StateField -deriving DecidableEq, Repr +deriving DecidableEq, Repr, Hashable + +namespace StateField + +/-- general purpose register `x31` is used as stack pointer -/ +@[state_simp_rules] +abbrev SP := GPR 31#5 + +/- Might eventually be used to maintain a `O(1)` access `StateField` map, +by using `StateField.toFin` to index into a sparse array. -/ +/-- `StateField` is equivalent to `Fin (32 + 32 + 1 + 4 + 1)` -/ +def toFin : StateField → Fin 70 + | .GPR x => x.toFin.castAdd 38 + | .SFP x => (x.toFin.addNat 32).castAdd 6 + | .PC => 64 + | .FLAG .N => 65 + | .FLAG .Z => 66 + | .FLAG .C => 67 + | .FLAG .V => 68 + | .ERR => 69 + +section ToExpr +open Lean PFlag + +instance : ToExpr PFlag where + toTypeExpr := mkConst ``PFlag + toExpr := fun + | N => mkConst ``N + | V => mkConst ``V + | C => mkConst ``C + | Z => mkConst ``Z + +instance : ToExpr StateField where + toTypeExpr := mkConst ``StateField + toExpr := fun + | GPR x => mkApp (mkConst ``GPR) (toExpr x) + | SFP x => mkApp (mkConst ``SFP) (toExpr x) + | PC => mkConst ``PC + | FLAG fl => mkApp (mkConst ``FLAG) (toExpr fl) + | ERR => mkConst ``ERR + +end ToExpr + +end StateField instance : ToString StateField := ⟨fun s => match s with @@ -645,6 +688,14 @@ theorem read_mem_bytes_of_w : rw [n_ih] done +@[state_simp_rules] +theorem read_mem_bytes_w_of_read_mem_eq + (h : ∀ n addr, read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂) + (fld val n₁ addr₁) : + read_mem_bytes n₁ addr₁ (w fld val s₁) + = read_mem_bytes n₁ addr₁ s₂ := by + simp only [read_mem_bytes_of_w, h] + @[state_simp_rules] theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n * 8)): (write_mem_bytes n addr bytes s).program = s.program := by @@ -1022,3 +1073,33 @@ by_cases h : ix < base · simp only [h₂, ↓reduceIte, BitVec.getLsb_extractLsByte] end Memory + +/-! ## Helper lemma for `AxEffects` -/ + +@[state_simp_rules] +theorem Memory.eq_of_read_mem_bytes_eq {m₁ m₂ : Memory} + (h : ∀ n addr, m₁.read_bytes n addr = m₂.read_bytes n addr) : + m₁ = m₂ := by + funext i + specialize (h 1 i) + simp only [Nat.reduceMul, read_bytes, Nat.reduceAdd, read, read_store, + BitVec.cast_eq] at h + rw [BitVec.zero_append, BitVec.zero_append] at h + simpa only [Nat.reduceAdd, BitVec.cast_eq] using h + +theorem mem_eq_iff_read_mem_bytes_eq {s₁ s₂ : ArmState} : + s₁.mem = s₂.mem + ↔ ∀ n addr, read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂ := by + simp only [memory_rules] + constructor + · intro h _ _; rw[h] + · exact Memory.eq_of_read_mem_bytes_eq + +theorem read_mem_bytes_write_mem_bytes_of_read_mem_eq + (h : ∀ n addr, read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂) + (n₂ addr₂ val n₁ addr₁) : + read_mem_bytes n₁ addr₁ (write_mem_bytes n₂ addr₂ val s₁) + = read_mem_bytes n₁ addr₁ (write_mem_bytes n₂ addr₂ val s₂) := by + revert n₁ addr₁ + simp only [← mem_eq_iff_read_mem_bytes_eq] at h ⊢ + simp only [memory_rules, h] diff --git a/Proofs/Experiments/Abs/Abs.lean b/Proofs/Experiments/Abs/Abs.lean index a088e397..f15c95e8 100644 --- a/Proofs/Experiments/Abs/Abs.lean +++ b/Proofs/Experiments/Abs/Abs.lean @@ -8,7 +8,7 @@ The goal is to prove that this program implements absolute value correctly. import Arm import Tactics.StepThms import Tactics.Sym - +import Tactics.CSE namespace Abs def program : Program := @@ -19,7 +19,16 @@ def program : Program := (0x4005dc#64, 0x4a000020#32), -- eor w0, w1, w0 (0x4005e0#64, 0xd65f03c0#32)] -- ret -def spec (x : BitVec 32) : BitVec 32 := BitVec.ofNat 32 x.toInt.natAbs +def spec (x : BitVec 32) : BitVec 32 := + -- We prefer the current definition as opposed to: + -- BitVec.ofNat 32 x.toInt.natAbs + -- because the above has functions like `toInt` that do not play well with + -- bitblasting/LeanSAT. + let msb := BitVec.extractLsb 31 31 x + if msb == 0#1 then + x + else + (0#32 - x) #genStepEqTheorems program @@ -29,15 +38,30 @@ theorem correct (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) : + (h_run : sf = run (program.length) s0) : read_gpr 32 0 sf = spec (read_gpr 32 0 s0) ∧ read_err sf = StateError.None := by simp (config := {ground := true}) at h_run sym_n 5 - sorry + simp only [run] at h_run + subst sf + apply And.intro + · simp only [read_gpr, BitVec.ofNat_eq_ofNat] + simp (config := {decide := true}) only [ + h_s5_non_effects, + h_s4_x0, + h_s3_x1, h_s3_non_effects, + h_s2_x0, h_s2_non_effects, + h_s1_x1, h_s1_non_effects] + generalize r (StateField.GPR 0#5) s0 = x + simp only [spec, AddWithCarry] + split <;> bv_decide + · assumption -/-- info: 'Abs.correct' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] -/ +/-- +info: 'Abs.correct' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] +-/ #guard_msgs in #print axioms correct end Abs diff --git a/Tactics/Attr.lean b/Tactics/Attr.lean index e6d3d9d9..574e0211 100644 --- a/Tactics/Attr.lean +++ b/Tactics/Attr.lean @@ -8,3 +8,16 @@ initialize -- enable tracing for `sym_n` tactic and related components registerTraceClass `Tactic.sym + + -- enable extra checks for debugging `sym_n`, + -- see `AxEffects.validate` for more detail on what is being type-checked + registerOption `Tactic.sym.debug { + defValue := true + descr := "enable/disable type-checking of internal state during execution \ + of the `sym_n` tactic, throwing an error if mal-formed expressions were \ + created, indicating a bug in the implementation of `sym_n`. + + This is an internal option for debugging purposes, end users should \ + generally not set this option, unless they are reporting a bug with \ + `sym_n`" + } diff --git a/Tactics/Common.lean b/Tactics/Common.lean index ed269ccf..22b4c290 100644 --- a/Tactics/Common.lean +++ b/Tactics/Common.lean @@ -138,6 +138,28 @@ def reflectBitVecLiteral (w : Nat) (e : Expr) : MetaM (BitVec w) := do else throwError "Expected a bitvector of width {w}, but\n\t{e}\nhas width {n}" +def reflectPFLag (e : Expr) : MetaM PFlag := + match_expr e with + | PFlag.N => pure .N + | PFlag.Z => pure .Z + | PFlag.C => pure .C + | PFlag.V => pure .V + | _ => + let pflag := mkConst ``PFlag + throwError "Expected a `{pflag}` constructor, found:\n {e}" + +/-- Reflect a concrete `StateField` -/ +def reflectStateField (e : Expr) : MetaM StateField := + match_expr e with + | StateField.GPR x => StateField.GPR <$> reflectBitVecLiteral _ x + | StateField.SFP x => StateField.SFP <$> reflectBitVecLiteral _ x + | StateField.PC => pure StateField.PC + | StateField.FLAG f => StateField.FLAG <$> reflectPFLag f + | StateField.ERR => pure StateField.ERR + | _ => + let sf := mkConst ``StateField + throwError "Expected a `{sf}` constructor, found:\n {e}" + /-! ## Hypothesis types -/ namespace SymContext @@ -224,3 +246,16 @@ def findProgramHyp (state : Expr) : MetaM (LocalDecl × Name) := do throwError "Expected a constant, found:\n\t{program}" return ⟨h_program, program⟩ + +/-! ## Expr Builders -/ + +/-- Return the expression for `ArmState` -/ +def mkArmState : Expr := mkConst ``ArmState + +/-- Return `x = y`, given expressions `x` and `y` of type `ArmState` -/ +def mkEqArmState (x y : Expr) : Expr := + mkApp3 (.const ``Eq [1]) mkArmState x y + +/-- Return a proof of type `x = x`, where `x : ArmState` -/ +def mkEqReflArmState (x : Expr) : Expr := + mkApp2 (.const ``Eq.refl [1]) mkArmState x diff --git a/Tactics/Reflect/AxEffects.lean b/Tactics/Reflect/AxEffects.lean new file mode 100644 index 00000000..2621b29a --- /dev/null +++ b/Tactics/Reflect/AxEffects.lean @@ -0,0 +1,624 @@ +/- +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): Alex Keizer +-/ + +import Arm.State +import Tactics.Common +import Tactics.Attr +import Std.Data.HashMap + +open Lean Meta + +/-- A reflected `ArmState` field, see `AxEffects.fields` for more context -/ +structure AxEffects.FieldEffect where + value : Expr + /-- A proof that `r = ` -/ + proof : Expr + deriving Repr +open AxEffects.FieldEffect + +/-- `AxEffects` is an axiomatic representation of effects, +i.e., `AxEffects` transforms a description of an `ArmState` written as +a sequence of `w` and `write_mem`s to some initial state +into a set of hypotheses that relates reading fields from the final state +to the initial state. +Note that as soon as an unsupported expression (e.g., an `if`) is encountered, +the whole expression is taken to be the initial state, +even if there might be more `w`/`write_mem`s in sub-expressions. + +`AxEffects` contains a hashmap from `StateField` to an expression, +in terms of the fixed initial state, +that describes the value of the given field *after* the writes. +Additionally, each field carries a proof that it is indeed the right value. + +Furthermore, we maintain a few other invariants, +see the docstrings on each field for more detail -/ +structure AxEffects where + /-- The initial state -/ + initialState : Expr + /-- The current state, which may be expressed in either the "exploded form" + (a sequence of `w`/`write_mem` to the initial state), or as just a variable + which is (propositionally) equal to that exploded form -/ + currentState : Expr + + /-- A map from each statefield to the corresponding `FieldEffect`. + If a field has no entry in this map, it has not been changed, and thus, + its value can be retrieved from the `nonEffectProof` -/ + fields : Std.HashMap StateField AxEffects.FieldEffect + /-- An expression that contains the proof of: + ```lean + ∀ (f : StateField), f ≠ → ⋯ → f ≠ → + r f = r f ` + ``` + where `f₁, ⋯, fₙ` are the keys of `fields` + -/ + nonEffectProof : Expr + /-- An expression of a (potentially empty) sequence of `write_mem`s + to the initial state, which describes the effects on memory. + See `memoryEffectProof` for more detail -/ + memoryEffect : Expr + /-- An expression that contains the proof of: + ```lean + ∀ n addr, + read_mem_bytes n addr + = read_mem_bytes n addr + ``` -/ + memoryEffectProof : Expr + /-- A proof that `.program = .program` -/ + programProof : Expr + /-- An optional proof of `CheckSPAlignment `. + + This proof is preserved on a best-effort basis. + That is, if we update the state with a write to memory, or a register that is + not SP, we maintain the proof. + However, if SP is written to, no effort is made to prove alignment of the + new value; the field will be set to `none` -/ + stackAlignmentProof? : Option Expr + deriving Repr + +namespace AxEffects + +/-! ## Initial Reflected State -/ + +/-- An initial `AxEffects` state which has no writes. +That is, the given `state` is assigned to be both the initial and the current +state -/ +def initial (state : Expr) : AxEffects where + initialState := state + currentState := state + fields := .empty + nonEffectProof := + -- `fun f => rfl` + mkLambda `f .default (mkConst ``StateField) <| + mkEqReflArmState <| mkApp2 (mkConst ``r) (.bvar 0) state + memoryEffect := state + memoryEffectProof := + -- `fun n addr => rfl` + mkLambda `n .default (mkConst ``Nat) <| + let bv64 := mkApp (mkConst ``BitVec) (toExpr 64) + mkLambda `addr .default bv64 <| + mkApp2 (.const ``Eq.refl [1]) + (mkApp (mkConst ``BitVec) <| mkNatMul (.bvar 1) (toExpr 8)) + (mkApp3 (mkConst ``read_mem_bytes) (.bvar 1) (.bvar 0) state) + programProof := + -- `rfl` + mkAppN (.const ``Eq.refl [1]) #[ + mkConst ``Program, + mkApp (mkConst ``ArmState.program) state] + stackAlignmentProof? := none + +/-! ## ToMessageData -/ + +instance : ToMessageData FieldEffect where + toMessageData := fun {value, proof} => + m!"\{ value := {value},\n proof := {proof} }" + +instance : ToMessageData (Std.HashMap StateField FieldEffect) where + toMessageData map := + toMessageData map.toList + +instance : ToMessageData AxEffects where + toMessageData eff := + m!"\ + \{ initialState := {eff.initialState}, + currentState := {eff.currentState}, + fields := {eff.fields}, + nonEffectProof := {eff.nonEffectProof}, + memoryEffect := {eff.memoryEffect}, + memoryEffectProof := {eff.memoryEffectProof}, + programProof := {eff.programProof} + }" + +private def traceCurrentState (eff : AxEffects) + (header : MessageData := "current state") : + MetaM Unit := + withTraceNode `Tactic.sym (fun _ => pure header) do + trace[Tactic.sym] "{eff}" + +/-! ## Helpers -/ + +/-- +Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`. + +Rewrites with a fresh metavariable as the ambient goal. +Fails if the rewrite produces any subgoals. +-/ +-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +private def rewrite (e eq : Expr) : MetaM Expr := do + let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq + | throwError "Expr.rewrite may not produce subgoals." + return eq' + +/-- +Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`. + +Rewrites with a fresh metavariable as the ambient goal. +Fails if the rewrite produces any subgoals. +-/ +-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +private def rewriteType (e eq : Expr) : MetaM Expr := do + mkEqMP (← rewrite (← inferType e) eq) e + +/-- Given a `field` such that `fields ∉ eff.fields`, return a proof of + `r field = r field ` +by constructing an application of `eff.nonEffectProof` -/ +partial def mkAppNonEffect (eff : AxEffects) (field : Expr) : MetaM Expr := do + let msg := m!"constructing application of non-effects proof" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + trace[Tactic.sym] "nonEffectProof: {eff.nonEffectProof}" + + let nonEffectProof := mkApp eff.nonEffectProof field + let typeOfNonEffects ← inferType nonEffectProof + forallTelescope typeOfNonEffects <| fun fvars _ => do + trace[Tactic.sym] "hypotheses of nonEffectProof: {fvars}" + let lctx ← getLCtx + let pre ← fvars.mapM fun expr => do + let ty := lctx.get! expr.fvarId! |>.type + mkDecideProof ty + + let nonEffectProof := mkAppN nonEffectProof pre + trace[Tactic.sym] "constructed: {nonEffectProof}" + return nonEffectProof + +/-- Get the value for a field, if one is stored in `eff.fields`, +or assemble an instantiation of the non-effects proof -/ +def getField (eff : AxEffects) (fld : StateField) : MetaM FieldEffect := + let msg := m!"getField {fld}" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + eff.traceCurrentState + + if let some val := eff.fields.get? fld then + trace[Tactic.sym] "returning stored value {val}" + return val + else + trace[Tactic.sym] "found no stored value" + let value := mkApp2 (mkConst ``r) (toExpr fld) eff.initialState + let proof ← eff.mkAppNonEffect (toExpr fld) + pure { value, proof } + +/-! ## Update a Reflected State -/ + +/-- Execute `write_mem ` against the state stored in `eff` +That is, `currentState` of the returned struct will be + `write_mem ` +and all other fields are updated accordingly. +Note that no effort is made to preserve `currentStateEq`; it is set to `none`! +-/ +private def update_write_mem (eff : AxEffects) (n addr val : Expr) : + MetaM AxEffects := do + trace[Tactic.sym] "adding write of {n} bytes of value {val} \ + to memory address {addr}" + + -- Update each field + let fields ← eff.fields.toList.mapM fun ⟨fld, {value, proof}⟩ => do + let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes) + (toExpr fld) n addr val eff.currentState + let proof ← mkEqTrans r_of_w proof + return ⟨fld, {value, proof}⟩ + + -- Update the non-effects proof + let nonEffectProof ← lambdaTelescope eff.nonEffectProof fun args proof => do + let f := args[0]! + let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes) + f n addr val eff.currentState + let proof ← mkEqTrans r_of_w proof + mkLambdaFVars args proof + -- ^^ `fun f ... => Eq.trans (@r_of_write_mem_bytes f ...) ` + + -- Update the memory effects proof + let memoryEffectProof := + -- `read_mem_bytes_write_mem_bytes_of_read_mem_eq ...` + mkAppN (mkConst ``read_mem_bytes_write_mem_bytes_of_read_mem_eq) + #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, n, addr, val] + + -- Update the program proof + let programProof ← + -- `Eq.trans (@write_mem_bytes_program ...) ` + mkEqTrans + (mkAppN (mkConst ``write_mem_bytes_program) + #[eff.currentState, n, addr, val]) + eff.programProof + + -- Assemble the result + let addWrite (e : Expr) := + -- `@write_mem_bytes ` + mkApp4 (mkConst ``write_mem_bytes) n addr val e + let eff := { eff with + currentState := addWrite eff.currentState + fields := .ofList fields + nonEffectProof + memoryEffect := addWrite eff.memoryEffect + memoryEffectProof + programProof + } + withTraceNode `Tactic.sym (fun _ => pure "new state") <| do + trace[Tactic.sym] "{eff}" + return eff + +/-- Execute `w ` against the state stored in `eff` +That is, `currentState` of the returned struct will be + `w ` +and all other fields are updated accordingly. +Note that no effort is made to preserve `currentStateEq`; it is set to `none`! +-/ +private def update_w (eff : AxEffects) (fld val : Expr) : + MetaM AxEffects := do + let rField ← reflectStateField fld + trace[Tactic.sym] "adding write of value {val} to register {rField}" + + -- Update all other fields + let fields ← + eff.fields.toList.filterMapM fun ⟨fld', {value, proof}⟩ => do + if fld' ≠ rField then + let proof : Expr ← do + let fld' := toExpr fld' + let h_neq : Expr ← -- h_neq : fld' ≠ fld + mkDecideProof (mkApp3 (.const ``Ne [1]) + (mkConst ``StateField) fld' fld) + let newProof := mkApp5 (mkConst ``r_of_w_different) + fld' fld val eff.currentState h_neq + mkEqTrans newProof proof + return some (fld', {value, proof}) + else + return none + + -- Update the main field + let newField : FieldEffect := { + value := val + proof := + -- `r_of_w_same ` + mkApp3 (mkConst ``r_of_w_same) fld val eff.currentState + } + let fields := (rField, newField) :: fields + + -- Update the non-effects proof + let nonEffectProof ← lambdaTelescope eff.nonEffectProof fun args proof => do + let f := args[0]! + + /- First, assume we have a proof `h_neq : ≠ `, and use that + to compute the new `nonEffectProof` -/ + let k := fun args h_neq => do + let r_of_w := mkApp5 (mkConst ``r_of_w_different) + f fld val eff.currentState h_neq + let proof ← mkEqTrans r_of_w proof + mkLambdaFVars args proof + -- ^^ `fun f ... => Eq.trans (r_of_w_different ... ) ` + + /- Then, determine `h_neq` so that we can pass it to `k`. + Notice how we have to modify the environment, to add `h_neq` as a new local + hypothesis if it wan't present yet, but only in some branches. + This is why we had to define `k` as a monadic continuation, + so we can nest `k` under a `withLocalDeclD` -/ + let h_neq_type := mkApp3 (.const ``Ne [1]) (mkConst ``StateField) f fld + let h_neq? ← args.findM? fun h => do + let hTy ← inferType h + return hTy == h_neq_type + match h_neq? with + | some h_neq => k args h_neq + | none => + let name := Name.mkSimple s!"h_neq_{rField}" + withLocalDeclD name h_neq_type fun h_neq => + k (args.push h_neq) h_neq + + -- Update the memory effect proof + let memoryEffectProof := + -- `read_mem_bytes_w_of_read_mem_eq ...` + mkAppN (mkConst ``read_mem_bytes_w_of_read_mem_eq) + #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, fld, val] + + -- Update the program proof + let programProof ← + -- `Eq.trans (w_program ...) ` + mkEqTrans + (mkAppN (mkConst ``w_program) #[fld, val, eff.currentState]) + eff.programProof + + -- Assemble the result + let eff := { eff with + currentState := mkApp3 (mkConst ``w) fld val eff.currentState + fields := Std.HashMap.ofList fields + nonEffectProof + -- memory effects are unchanged + memoryEffectProof + programProof + } + eff.traceCurrentState "new state" + return eff + +/-- Throw an error if `e` is not of type `expectedType` -/ +private def assertHasType (e expectedType : Expr) : MetaM Unit := do + let eType ← inferType e + if !(←isDefEq eType expectedType) then + throwError "{e} {← mkHasTypeButIsExpectedMsg eType expectedType}" + +private def assertIsDefEq (e expected : Expr) : MetaM Unit := do + if !(←isDefEq e expected) then + throwError "expected:\n {expected}\nbut found:\n {e}" + +/-- Given an expression `e : ArmState`, +which is a sequence of `w`/`write_mem`s to the some state `s`, +return an `AxEffects` where `s` is the intial state, and `e` is `currentState`. + +Note that as soon as an unsupported expression (e.g., an `if`) is encountered, +the whole expression is taken to be the initial state, +even if there might be more `w`/`write_mem`s in sub-expressions. -/ +partial def fromExpr (e : Expr) : MetaM AxEffects := do + let msg := m!"Building effects with writes from: {e}" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do match_expr e with + | write_mem_bytes n addr val e => + let eff ← fromExpr e + eff.update_write_mem n addr val + + | w field value e => + let eff ← fromExpr e + eff.update_w field value + + | _ => + return initial e + +/-- Given a proof `eq : s = `, +set `s` to be the new `currentState`, and update all proofs accordingly -/ +def adjustCurrentStateWithEq (eff : AxEffects) (s eq : Expr) : + MetaM AxEffects := do + withTraceNode `Tactic.sym (fun _ => pure "adjusting `currenstState`") do + eff.traceCurrentState + trace[Tactic.sym] "rewriting along {eq}" + assertHasType eq <| mkEqArmState s eff.currentState + let eq ← mkEqSymm eq + + let currentState := s + + let fields ← eff.fields.toList.mapM fun (field, fieldEff) => do + withTraceNode `Tactic.sym (fun _ => pure m!"rewriting field {field}") do + trace[Tactic.sym] "original proof: {fieldEff.proof}" + let proof ← rewriteType fieldEff.proof eq + trace[Tactic.sym] "new proof: {proof}" + pure (field, {fieldEff with proof}) + let fields := .ofList fields + + let nonEffectProof ← rewriteType eff.nonEffectProof eq + let memoryEffectProof ← rewriteType eff.memoryEffectProof eq + -- ^^ TODO: what happens if `memoryEffect` is the same as `currentState`? + -- Presumably, we would *not* want to encapsulate `memoryEffect` here + let programProof ← rewriteType eff.programProof eq + + return { eff with + currentState, fields, nonEffectProof, memoryEffectProof, programProof + } + +/-- Given a proof `eq : ?s = `, +where `?s` and `?s0` are arbitrary `ArmState`s, +return an `AxEffect` with `?s0` as the initial state, +the rhs of the equality as the current state, and +`eq` stored as `currentStateEq`, +so that `?s` is the public-facing current state -/ +def fromEq (eq : Expr) : MetaM AxEffects := + let msg := m!"Building effects with equality: {eq}" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + let s ← mkFreshExprMVar mkArmState + let rhs ← mkFreshExprMVar mkArmState + assertHasType eq <| mkEqArmState s rhs + + let eff ← fromExpr (← instantiateMVars rhs) + let eff ← eff.adjustCurrentStateWithEq s eq + withTraceNode `Tactic.sym (fun _ => pure "new state") do + trace[Tactic.sym] "{eff}" + return eff + +/-- Given an equality `eq : ?currentProgram = ?newProgram`, +where `currentProgram` is the rhs of `eff.programProof`, +apply transitivity to make `newProgram` the rhs of `programProof` +in the return value. + +Generally used with `?currentProgram = .program`, which is the +default rhs created by `initial`, +and `?newProgram` the constant of the concrete program. -/ +def withProgramEq (eff : AxEffects) (eq : Expr) : MetaM AxEffects := do + let programProof ← mkEqTrans eff.programProof eq + return {eff with programProof} + +/-- Given an equality `eq : r ?field = ?value`, +record `value` in the `AxEffect`s struct as the effect for `field`, +assuming that `field` did not have an effect stored yet. + +Otherwise, if there *is* an effect stored for the field, try to rewrite it +along the given equality. +If this rewrite fails, return the original effects unchanged. + +Note: throws an error when `initialState = currentState` *and* +the field already has a value stored, as the rewrite might produce expressions +of unexpected types. -/ +def withField (eff : AxEffects) (eq : Expr) : MetaM AxEffects := do + let msg := m!"withField {eq}" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + eff.traceCurrentState + let fieldE ← mkFreshExprMVar (mkConst ``StateField) + let value ← mkFreshExprMVar none + let expectedType ← mkEq (mkApp2 (mkConst ``r) fieldE eff.initialState) value + assertHasType eq expectedType + + let field ← reflectStateField (← instantiateMVars fieldE) + let fieldEff ← eff.getField field + trace[Tactic.sym] "current field effect: {fieldEff}" + + if field ∉ eff.fields then + let proof ← mkEqTrans fieldEff.proof eq + let fields := eff.fields.insert field { value, proof } + return { eff with fields } + else + if eff.currentState == eff.initialState then + throwError "error: {field} already has an effect associated with it, \ + and the current state + {eff.currentState} + is equal to the initial state + {eff.initialState}" + + let valEq ← try rewrite fieldEff.value eq + catch _ => return eff + + let_expr Eq _ _ value := ← inferType valEq + | throwError "internal error: expected an equality, found {valEq}" + let proof ← mkEqMP valEq fieldEff.proof + let fields := eff.fields.insert field { value, proof } + return { eff with fields } + +/-- Given a proof of `CheckSPAlignment `, +attempt to transport it to a proof of `CheckSPAlignment ` +and store that proof in `stackAlignmentProof?`. + +Returns `none` if the proof failed to be transported, +i.e., if SP was written to. -/ +def withStackAlignment? (eff : AxEffects) (spAlignment : Expr) : + MetaM (Option AxEffects) := do + let msg := m!"withInitialStackAlignment? {spAlignment}" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + eff.traceCurrentState + + let { value, proof } ← eff.getField StateField.SP + let expected := + mkApp2 (mkConst ``r) (toExpr <| StateField.SP) eff.initialState + trace[Tactic.sym] "checking whether value:\n {value}\n\ + is syntactically equal to expected value\n {expected}" + if value != expected then + trace[Tactic.sym] "failed to transport proof: + expected value to be {expected}, but found {value}" + return none + + let stackAlignmentProof? := some <| + mkAppN (mkConst ``CheckSPAlignment_of_r_sp_eq) + #[eff.initialState, eff.currentState, proof, spAlignment] + trace[Tactic.sym] "constructed stackAlignmentProof: {stackAlignmentProof?}" + return some { eff with stackAlignmentProof? } + +/-! ## Composition -/ + +/- TODO: write a function that combines two effects `left` and `right`, +where `left.initialState = right.currentState`. +That is, compose the effect of "`left` after `right`" -/ + +/-! ## Validation -/ + +/-- type check all expressions stored in `eff`, +throwing an error if one is not type-correct. + +In principle, the various `AxEffects` definitions should return only well-formed +expressions, making `validate` a no-op. +In practice, however, running `validate` is helpful for catching bugs in those +definitions. Do note that typechecking might be a bit expensive, so we generally +only call `validate` while debugging, not during normal execution. +See also the `Tactic.sym.debug` option, which controls whether `validate` is +called for each step of the `sym_n` tactic. + +NOTE: does not necessarily validate *which* type an expression has, +validation will still pass if types are different to those we claim in the +docstrings -/ +def validate (eff : AxEffects) : MetaM Unit := do + let msg := "validating that the axiomatic effects are well-formed" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + eff.traceCurrentState + + assertHasType eff.initialState mkArmState + assertHasType eff.currentState mkArmState + + for ⟨_field, fieldEff⟩ in eff.fields do + check fieldEff.value + check fieldEff.proof + + check eff.nonEffectProof + check eff.memoryEffect + check eff.memoryEffectProof + check eff.programProof + if let some h := eff.stackAlignmentProof? then + check h + +/-! ## Tactic Environment -/ +section Tactic +open Elab.Tactic + +/-- Add new hypotheses to the local context of a given mvar (or the main goal, +by default): +- one for every field in `eff.fields` +- `eff.nonEffectProof`, +- `eff.memoryEffectProof`, +- `eff.programProof`, and +- `eff.stackAlignmentProof?` (if the field is not `none`) -/ +def addHypothesesToLContext (eff : AxEffects) (hypPrefix : String := "h_") + (mvar : Option MVarId := none): + TacticM Unit := + let msg := m!"adding hypotheses to local context" + withTraceNode `Tactic.sym (fun _ => pure msg) do + eff.traceCurrentState + let mut goal ← mvar.getDM getMainGoal + + for ⟨field, {proof, ..}⟩ in eff.fields do + let msg := m!"adding field {field}" + goal ← withTraceNode `Tactic.sym (fun _ => pure msg) <| goal.withContext do + trace[Tactic.sym] "raw proof: {proof}" + let name := Name.mkSimple (s!"{hypPrefix}{field}") + replaceOrNote goal name proof + + trace[Tactic.sym] "adding non-effects with {eff.nonEffectProof}" + goal ← goal.withContext do + let name := .mkSimple s!"{hypPrefix}non_effects" + let proof := eff.nonEffectProof + replaceOrNote goal name proof + + trace[Tactic.sym] "adding memory effects with {eff.memoryEffectProof}" + goal ← goal.withContext do + let name := .mkSimple s!"{hypPrefix}memory_effects" + let proof := eff.memoryEffectProof + replaceOrNote goal name proof + + trace[Tactic.sym] "adding program hypothesis with {eff.programProof}" + goal ← goal.withContext do + let name := .mkSimple s!"{hypPrefix}program" + let proof := eff.programProof + replaceOrNote goal name proof + + trace[Tactic.sym] "stackAlignmentProof? is {eff.stackAlignmentProof?}" + if let some stackAlignmentProof := eff.stackAlignmentProof? then + trace[Tactic.sym] "adding stackAlignment hypothesis" + goal ← goal.withContext do + let name := .mkSimple s!"{hypPrefix}sp_aligned" + replaceOrNote goal name stackAlignmentProof + else + trace[Tactic.sym] "skipping stackAlignment hypothesis" + + replaceMainGoal [goal] +where + replaceOrNote (goal : MVarId) (h : Name) (v : Expr) + (t? : Option Expr := none) : + MetaM MVarId := + let msg := m!"adding {h} to the local context" + withTraceNode `Tactic.sym (fun _ => pure msg) <| do + trace[Tactic.sym] "with value {v} and type {t?}" + if let some decl := (← getLCtx).findFromUserName? h then + let ⟨_, goal, _⟩ ← goal.replace decl.fvarId v t? + return goal + else + let ⟨_, goal⟩ ← goal.note h v t? + return goal + +end Tactic diff --git a/Tactics/Reflect/ProgramInfo.lean b/Tactics/Reflect/ProgramInfo.lean index 897ec2a3..99e3cc71 100644 --- a/Tactics/Reflect/ProgramInfo.lean +++ b/Tactics/Reflect/ProgramInfo.lean @@ -179,7 +179,9 @@ initialize programInfoExt : PersistentEnvExtension (ProgramInfo) (ProgramInfo) ( registerPersistentEnvExtension { name := `programInfo mkInitial := pure {} - addImportedFn := fun _ _ => pure {} + addImportedFn := fun pis => + pis.flatten.foldlM (init := ∅) fun map p => + return map.insert p.name p addEntryFn := fun s p => s.insert p.name p exportEntriesFn := fun m => let r : Array (ProgramInfo) := diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean index 5b52edf0..0e51334f 100644 --- a/Tactics/Sym.lean +++ b/Tactics/Sym.lean @@ -179,6 +179,91 @@ def withoutHyp (hyp : Name) (k : TacticM Unit) : TacticM (Option FVarId) := replaceMainGoal [newGoal] return newHyp +/-- Given an equality `h_step : s{i+1} = w ... (... (w ... s{i})...)`, +add hypotheses that axiomatically describe the effects in terms of +reads from `s{i+1}` -/ +def explodeStep (c : SymContext) (hStep : Expr) : TacticM Unit := + withMainContext do + let mut eff ← AxEffects.fromEq hStep + + let stateExpr ← c.stateExpr + /- Assert that the initial state of the obtained `AxEffects` is equal to + the state tracked by `c`. + This will catch and throw an error if the semantics of the current + instruction still contains unsupported constructs (e.g., an `if`) -/ + if !(← isDefEq eff.initialState stateExpr) then + throwError "[explodeStep] expected initial state {stateExpr}, but found:\n \ + {eff.initialState}\nin\n\n{eff}" + + let hProgram ← SymContext.findFromUserName c.h_program + eff ← eff.withProgramEq hProgram.toExpr + + let hErr ← SymContext.findFromUserName c.h_err + eff ← eff.withField hErr.toExpr + + if let some h_sp := c.h_sp? then + let hSp ← SymContext.findFromUserName h_sp + -- let effWithSp? + eff ← match ← eff.withStackAlignment? hSp.toExpr with + | some newEff => pure newEff + | none => do + trace[Tactic.sym] "failed to show stack alignment" + -- FIXME: in future, we'd like to detect when the `sp_aligned` + -- hypothesis is actually necessary, and add the proof obligation + -- on-demand. For now, however, we over-approximate, and say that + -- if the original state was known to be aligned, and something + -- writes to the SP, then we eagerly add the obligation to proof + -- that the result is aligned as well. + -- If you don't want this obligation, simply remove the hypothesis + -- that the original state is aligned + let spEff ← eff.getField .SP + let subGoal ← mkFreshMVarId + -- subGoal.setTag <| + let hAligned ← do + let name := Name.mkSimple s!"h_{c.next_state}_sp_aligned" + mkFreshExprMVarWithId subGoal (userName := name) <| + mkAppN (mkConst ``Aligned) #[toExpr 64, spEff.value, toExpr 4] + + trace[Tactic.sym] "created subgoal to show alignment:\n{subGoal}" + + let subGoal? ← do + let (ctx, simprocs) ← + LNSymSimpContext + (config := {failIfUnchanged := false, decide := true}) + (decls := #[hSp]) + LNSymSimp subGoal ctx simprocs + + if let some subGoal := subGoal? then + trace[Tactic.sym] "subgoal got simplified to:\n{subGoal}" + appendGoals [subGoal] + else + trace[Tactic.sym] "subgoal got closed by simplification" + + let stackAlignmentProof? := some <| + mkAppN (mkConst ``CheckSPAlignment_of_r_sp_aligned) + #[eff.currentState, spEff.value, spEff.proof, hAligned] + pure { eff with stackAlignmentProof? } + + withMainContext <| do + if ←(getBoolOption `Tactic.sym.debug) then + eff.validate + + eff.addHypothesesToLContext s!"h_{c.next_state}_" + +/-- A tactic wrapper around `explodeStep`. +Note the use of `SymContext.fromLocalContext`, +so the local context is assumed to be of the same shape as for `sym_n` -/ +elab "explode_step" h_step:term " at " state:term : tactic => withMainContext do + let hStep ← elabTerm h_step none + let state ← elabTerm state mkArmState + let .fvar stateFVar := state + | throwError "Expected fvar, found {state}" + let stateDecl := (← getLCtx).get! stateFVar + let c ← SymContext.fromLocalContext (some stateDecl.userName) + + explodeStep c hStep + + /-- Symbolically simulate a single step, according the the symbolic simulation context `c`, returning the context for the next step in simulation. -/ @@ -191,7 +276,6 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext := let stepi_eq := Lean.mkIdent (.mkSimple s!"stepi_{c.state}") let h_step := Lean.mkIdent (.mkSimple s!"h_step_{c.curr_state_number + 1}") - -- let stepi_eq := h_step unfoldRun c (fun _ => evalTacticAndTrace whileTac) -- Add new state to local context @@ -202,15 +286,39 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext := -- Apply relevant pre-generated `stepi` lemma stepiTac stepi_eq h_step c + -- WORKAROUND: eventually we'd like to eagerly simp away `if`s in the + -- pre-generation of instruction semantics. For now, though, we keep a + -- `simp` here + withMainContext <| do + let hStep ← SymContext.findFromUserName h_step.getId + let lctx ← getLCtx + let decls := (c.h_sp?.bind lctx.findFromUserName?).toArray + -- If we know SP is aligned, `simp` with that fact + + if !decls.isEmpty then + trace[Tactic.sym] "simplifying {hStep.toExpr} \ + with {decls.map (·.toExpr)}" + -- If `decls` is empty, we have no more knowledge than before, so + -- everything that could've been `simp`ed, already should have been + let some goal ← do + let (ctx, simprocs) ← LNSymSimpContext + (config := {decide := false}) (decls := decls) + let goal ← getMainGoal + LNSymSimp goal ctx simprocs hStep.fvarId + | throwError "internal error: simp closed goal unexpectedly" + replaceMainGoal [goal] + else + trace[Tactic.sym] "we have no relevant local hypotheses, \ + skipping simplification step" + -- Prepare `h_program`,`h_err`,`h_pc`, etc. for next state - let h_st_prefix := Lean.Syntax.mkStrLit s!"h_{c.state}" - -- Ensure we run `intro_fetch_decode_lemmas` without `stepi_eq` - let _ ← withoutHyp stepi_eq.getId <| evalTacticAndTrace <|← `(tactic| - intro_fetch_decode_lemmas - $h_step:ident $c.h_program_ident:ident $h_st_prefix:str - ) - return c.next + withMainContext <| do + let hStep ← SymContext.findFromUserName h_step.getId + -- ^^ we can't reuse `hStep` from before, since its fvarId might've been + -- changed by `simp` + explodeStep c hStep.toExpr + return c.next /- used in `sym_n` tactic to specify an initial state -/ syntax sym_at := "at" ident diff --git a/Tactics/SymContext.lean b/Tactics/SymContext.lean index db6998d5..ca4072bf 100644 --- a/Tactics/SymContext.lean +++ b/Tactics/SymContext.lean @@ -9,6 +9,8 @@ import Lean.Meta import Arm.Exec import Tactics.Common import Tactics.Attr +import Tactics.Reflect.ProgramInfo +import Tactics.Reflect.AxEffects /-! This files defines the `SymContext` structure, @@ -55,6 +57,9 @@ structure SymContext where program : Name /-- `h_program` is a local hypothesis of the form `state.program = program` -/ h_program : Name + /-- `programInfo` is the relevant cached `ProgramInfo` -/ + programInfo : ProgramInfo + /-- `pc` is the *concrete* value of the program counter Note that for now we only support symbolic evaluation of programs @@ -84,7 +89,6 @@ structure SymContext where and used together with `curr_state_number` to determine the name of the next state variable that is added by `sym` -/ curr_state_number : Nat := 0 - deriving Repr namespace SymContext @@ -113,7 +117,7 @@ def h_sp_ident : Ident := mkIdent c.h_sp /-- Find the local declaration that corresponds to a given name, or throw an error if no local variable of that name exists -/ -private def findFromUserName (name : Name) : MetaM LocalDecl := do +def findFromUserName (name : Name) : MetaM LocalDecl := do let some decl := (← getLCtx).findFromUserName? name | throwError "Unknown local variable `{name}`" return decl @@ -256,9 +260,15 @@ def fromLocalContext (state? : Option Name) : MetaM SymContext := do if h_sp?.isNone then trace[Sym] "Could not find local hypothesis of type {h_sp_type stateExpr}" + -- Finally, retrieve the programInfo from the environment + let some programInfo ← ProgramInfo.lookup? program + | throwError "Could not find program info for `{program}`. + Did you remember to generate step theorems with: + #generateStepEqTheorems {program}" + return inferStatePrefixAndNumber { state, finalState, h_run, runSteps?, program, h_program, pc, h_pc, - h_err?, h_sp? + h_err?, h_sp?, programInfo } where findLocalDeclUsernameOfType? (expectedType : Expr) : MetaM (Option Name) := do @@ -281,7 +291,8 @@ where /-- If `h_sp` or `h_err` are missing from the `SymContext`, add new goals of the expected types, and use these to add `h_sp` and `h_err` to the main goal context -/ -def addGoalsForMissingHypotheses (ctx : SymContext) : TacticM SymContext := +def addGoalsForMissingHypotheses (ctx : SymContext) (addHSp : Bool := false) : + TacticM SymContext := let msg := "Adding goals for missing hypotheses" withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext do let mut ctx := ctx @@ -314,20 +325,24 @@ def addGoalsForMissingHypotheses (ctx : SymContext) : TacticM SymContext := match ctx.h_sp? with | none => - trace[Tactic.sym] "h_sp? is none, adding a new goal" - - let h_sp? := Name.mkSimple s!"h_{ctx.state}_sp" - let newGoal ← mkFreshMVarId - - goal := ← do - let h_sp_type := h_sp_type stateExpr - let newGoalExpr ← mkFreshExprMVarWithId newGoal h_sp_type - let goal' ← goal.assert h_sp? h_sp_type newGoalExpr - let ⟨_, goal'⟩ ← goal'.intro1P - return goal' - - newGoals := newGoal :: newGoals - ctx := { ctx with h_sp? } + if addHSp then + trace[Tactic.sym] "h_sp? is none, adding a new goal" + + let h_sp? := Name.mkSimple s!"h_{ctx.state}_sp" + let newGoal ← mkFreshMVarId + + goal := ← do + let h_sp_type := h_sp_type stateExpr + let newGoalExpr ← mkFreshExprMVarWithId newGoal h_sp_type + let goal' ← goal.assert h_sp? h_sp_type newGoalExpr + let ⟨_, goal'⟩ ← goal'.intro1P + return goal' + + newGoals := newGoal :: newGoals + ctx := { ctx with h_sp? } + else + trace[Tactic.sym] "h_sp? is none, but addHSp is false, \ + so no new goal is added" | some h_sp => let h_sp ← userNameToMessageData h_sp trace[Tactic.sym] "h_sp? is {h_sp}, no new goal needed" @@ -380,10 +395,11 @@ def next (c : SymContext) (nextPc? : Option (BitVec 64) := none) : h_run := c.h_run h_program := .mkSimple s!"h_{s}_program" h_pc := .mkSimple s!"h_{s}_pc" - h_err? := some <| .mkSimple s!"h_{s}_err" - h_sp? := some <| .mkSimple s!"h_{s}_sp" + h_err? := c.h_err?.map (fun _ => .mkSimple s!"h_{s}_err") + h_sp? := c.h_sp?.map (fun _ => .mkSimple s!"h_{s}_sp_aligned") runSteps? := (· - 1) <$> c.runSteps? program := c.program + programInfo := c.programInfo pc := nextPc?.getD (c.pc + 4#64) curr_state_number state_prefix := c.state_prefix diff --git a/Tests/Tactics/Sym.lean b/Tests/Tactics/Sym.lean index d83de45d..65f13205 100644 --- a/Tests/Tactics/Sym.lean +++ b/Tests/Tactics/Sym.lean @@ -5,6 +5,9 @@ Author(s): Alex Keizer -/ import Proofs.«AES-GCM».GCMGmultV8Sym +-- Enable extra validations +set_option Tactic.sym.debug true + namespace GCMGmultV8Program -- Test the behaviour of `sym_n` when `h_err` and `h_sp` are not present @@ -17,6 +20,29 @@ namespace GCMGmultV8Program simp (config := {ground := true}) only [Option.some.injEq] at h_s0_pc h_run sym_n 1 · sorry - · exact (sorry : CheckSPAlignment s0) · exact (sorry : read_err s0 = .None) done + + +namespace SimpleMemory + +def program := def_program [ + (0x4005b8#64 , 0xb9000fe0#32), -- str w0, [sp, #12] + ] + +#genStepEqTheorems program + +example + (sf s0 : ArmState) + (h_program : s0.program = program) + (h_run : sf = run 1 s0) + (h_err : read_err s0 = .None) + (h_pc : read_pc s0 = 0x4005b8#64) + (h_sp : CheckSPAlignment s0) + (h_s0_x0 : r (.GPR 0#5) s0 = x) + (h_s0_x31 : r (.GPR 31#5) s0 = y) : + read_mem_bytes 4 (y + 12#64) s0 = (x.zeroExtend 32) := by + sym_n 1 + sorry + +end SimpleMemory