From 2cb5579cd3ad745581cf0fef6917775e978663c5 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 14 Oct 2024 14:46:15 -0500 Subject: [PATCH] refactor: replace `rewrite` with `mkEqNDRec` --- Tactics/Common.lean | 21 +++++++++++++++++++ Tactics/Sym/AxEffects.lean | 37 ++++++++++++++++++++++++++++------ Tactics/Sym/Context.lean | 4 +++- Tactics/Sym/MemoryEffects.lean | 18 +++++++++-------- 4 files changed, 65 insertions(+), 15 deletions(-) diff --git a/Tactics/Common.lean b/Tactics/Common.lean index 9763af33..6b302996 100644 --- a/Tactics/Common.lean +++ b/Tactics/Common.lean @@ -280,6 +280,27 @@ def Lean.Expr.eqReadField? (e : Expr) : Option (Expr × Expr × Expr) := do /-- Return the expression for `Memory` -/ def mkMemory : Expr := mkConst ``Memory +/-- Return `ArmState.program = ` -/ +def mkEqProgram (state program : Expr) : Expr := + mkApp3 (.const ``Eq [1]) (mkConst ``Program) + (mkApp (mkConst ``ArmState.program) state) + program + +/-- Return `x = y`, given expressions `x, y : BitVec ` -/ +def mkEqBitVec (n x y : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) n + mkApp3 (.const ``Eq [1]) ty x y + +/-- Return `read_mem_bytes ` -/ +def mkReadMemBytes (n addr state : Expr) : Expr := + mkApp3 (mkConst ``read_mem_bytes) n addr state + +/-- Return `read_mem_bytes = `, given expressions +`n : Nat`, `addr : BitVec 64`, `state : ArmState` and `value : BitVec (n*8)` -/ +def mkEqReadMemBytes (n addr state value : Expr) : Expr := + let n8 := mkNatMul n (toExpr 8) + mkEqBitVec n8 (mkReadMemBytes n addr state) value + /-! ## Expr Helpers -/ /-- Throw an error if `e` is not of type `expectedType` -/ diff --git a/Tactics/Sym/AxEffects.lean b/Tactics/Sym/AxEffects.lean index 275a0cb5..69e9eade 100644 --- a/Tactics/Sym/AxEffects.lean +++ b/Tactics/Sym/AxEffects.lean @@ -62,7 +62,9 @@ structure AxEffects where nonEffectProof : Expr /-- The memory effects -/ memoryEffects : MemoryEffects - /-- A proof that `.program = .program` -/ + /-- The program of the current state, see `programProof` -/ + program : Expr + /-- A proof that `.program = ` -/ programProof : Expr /-- An optional proof of `CheckSPAlignment `. @@ -129,6 +131,8 @@ def initial (state : Expr) : AxEffects where mkLambda `f .default (mkConst ``StateField) <| mkEqReflArmState <| mkApp2 (mkConst ``r) (.bvar 0) state memoryEffects := .initial state + program := -- `ArmState.program ` + mkApp (mkConst ``ArmState.program) state programProof := -- `rfl` mkAppN (.const ``Eq.refl [1]) #[ @@ -486,17 +490,38 @@ def adjustCurrentStateWithEq (eff : AxEffects) (s eq : Expr) : let fields ← eff.fields.toList.mapM fun (field, fieldEff) => do withTraceNode m!"rewriting field {field}" (tag := "rewriteField") do trace[Tactic.sym] "original proof: {fieldEff.proof}" - let proof ← rewriteType fieldEff.proof eq + let motive : Expr ← withLocalDeclD `s mkArmState <| fun s => do + let eq := mkEqReadField (toExpr field) s fieldEff.value + mkLambdaFVars #[s] eq + let proof ← mkEqNDRec motive fieldEff.proof eq trace[Tactic.sym] "new proof: {proof}" pure (field, {fieldEff with proof}) let fields := .ofList fields Sym.withTraceNode m!"rewriting other proofs" (tag := "rewriteMisc") <| do - let nonEffectProof ← rewriteType eff.nonEffectProof eq + let nonEffectProof ← lambdaTelescope eff.nonEffectProof fun args proof => do + let f := args[0]! + let motive ← -- `fun s => r f s = r f ` + -- TODO: ` + withLocalDeclD `s mkArmState <| fun s => + let eq := mkEqStateValue f + (mkApp2 (mkConst ``r) f s) + (mkApp2 (mkConst ``r) f eff.initialState) + mkLambdaFVars #[s] eq + mkLambdaFVars args <|← mkEqNDRec motive proof eq + let memoryEffects ← eff.memoryEffects.adjustCurrentStateWithEq eq - let programProof ← rewriteType eff.programProof eq - let stackAlignmentProof? ← eff.stackAlignmentProof?.mapM - (rewriteType · eq) + + let programMotive : Expr ← + withLocalDeclD `s mkArmState <| fun s => + let eq := mkEqProgram s eff.program + mkLambdaFVars #[s] eq + let programProof ← mkEqNDRec programMotive eff.programProof eq + + let stackAlignmentProof? ← eff.stackAlignmentProof?.mapM fun proof => do + let motive ← withLocalDeclD `s mkArmState <| fun s => + mkLambdaFVars #[s] <| mkApp (mkConst ``CheckSPAlignment) s + mkEqNDRec motive proof eq return { eff with currentState, fields, nonEffectProof, memoryEffects, programProof, diff --git a/Tactics/Sym/Context.lean b/Tactics/Sym/Context.lean index 44d981e0..944b4889 100644 --- a/Tactics/Sym/Context.lean +++ b/Tactics/Sym/Context.lean @@ -333,12 +333,14 @@ protected def searchFor : SearchLCtxForM SymM Unit := do searchLCtxForOnce (h_program_type currentState program) (whenNotFound := throwNotFound) (whenFound := fun decl _ => do + let program ← instantiateMVars program -- Register the program proof modifyThe AxEffects ({· with + program programProof := decl.toExpr }) -- Assert that `program` is a(n application of a) constant - let program := (← instantiateMVars program).getAppFn + let program := program.getAppFn let .const program _ := program | throwError "Expected a constant, found:\n\t{program}" -- Retrieve the programInfo from the environment diff --git a/Tactics/Sym/MemoryEffects.lean b/Tactics/Sym/MemoryEffects.lean index 45cb7eec..4dfb0802 100644 --- a/Tactics/Sym/MemoryEffects.lean +++ b/Tactics/Sym/MemoryEffects.lean @@ -79,14 +79,16 @@ def updateWrite (eff : MemoryEffects) (currentState : Expr) so that `s` is the new `currentState` -/ def adjustCurrentStateWithEq (eff : MemoryEffects) (eq : Expr) : MetaM MemoryEffects := do - let proof ← rewriteType eff.proof eq - /- ^^ This looks scary, since it can rewrite the left-hand-side of the proof - if `memoryEffect` is the same as `currentState` (which would be bad!). - However, this cannot ever happen in LNSym: every instruction has to modify - either the PC or the error field, neither of which is incorporated into - the `memoryEffect` and thus, `memoryEffect` never coincides with - `currentState` (assuming we're dealing with instruction semantics, as we - currently do!). -/ + let memoryMotive : Expr ← + withLocalDeclD `s mkArmState <| fun s => + withLocalDeclD `n (mkConst ``Nat) <| fun n => + withLocalDeclD `addr (mkApp (mkConst ``BitVec) (toExpr 64)) <| fun addr => do + let lhs := mkReadMemBytes n addr s + let rhs := mkReadMemBytes n addr eff.effects + let eq := mkEqBitVec (mkNatMul n (toExpr 8)) lhs rhs + let eq ← mkForallFVars #[n, addr] eq + mkLambdaFVars #[s] eq + let proof ← mkEqNDRec memoryMotive eff.proof eq return { eff with proof } /-- Convert a `MemoryEffects` into a `MessageData` for logging. -/