diff --git a/Proofs/AES-GCM/AESHWEncryptSym.lean b/Proofs/AES-GCM/AESHWEncryptSym.lean index 57d9a230..2739b007 100644 --- a/Proofs/AES-GCM/AESHWEncryptSym.lean +++ b/Proofs/AES-GCM/AESHWEncryptSym.lean @@ -39,7 +39,8 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState) init_next_step h_run h_step_13 s13 replace h_step_13 := h_step_13.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_13<;> try assumption - simp only [h_s1_x3, h_s2_non_effects, h_s3_non_effects, h_s4_x3, + simp (config := {decide := true}) only + [h_s1_x3, h_s2_non_effects, h_s3_non_effects, h_s4_x3, h_s5_non_effects, h_s6_non_effects, h_s7_non_effects, h_s8_non_effects, h_s9_flagN, h_s9_flagV, h_s9_flagZ, h_s9_flagC, h_s10_non_effects, h_s11_non_effects, @@ -51,7 +52,8 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState) -- Add hypotheses that are needed for next loop iteration -- This is an aggregated result have h_s13_x3 : read_gpr 32 3#5 s13 = 10#32 := by - simp only [h_s1_x3, h_s2_non_effects, h_s3_non_effects, h_s4_x3, + simp (config := { decide := true }) only [ + h_s1_x3, h_s2_non_effects, h_s3_non_effects, h_s4_x3, h_s5_non_effects, h_s6_non_effects, h_s7_non_effects, h_s8_non_effects, h_s9_x3, h_s10_non_effects, h_s11_non_effects, h_s12_non_effects, h_step_13, @@ -63,106 +65,106 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState) replace h_step_21 := h_step_21.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_21<;> try assumption simp only [state_simp_rules] at h_s13_x3 - simp only [h_s20_non_effects, h_s19_non_effects, h_s18_non_effects, + simp (config := { decide := true }) only [ + h_s20_non_effects, h_s19_non_effects, h_s18_non_effects, h_s17_flagN, h_s17_flagV, h_s17_flagZ, h_s17_flagC, h_s16_non_effects, h_s15_non_effects, h_s14_non_effects, state_simp_rules, bitvec_rules, minimal_theory, -- hypothesis that states x3's value h_s13_x3] at h_step_21 - simp (config := {ground := true}) only [minimal_theory] at h_step_21 (intro_fetch_decode_lemmas h_step_21 h_s20_program "h_s20") -- Add hypotheses that are needed for next loop iteration -- This is an aggregated result have h_s21_x3 : read_gpr 32 3#5 s21 = 8#32 := by - simp only [h_s20_non_effects, h_s19_non_effects, h_s18_non_effects, + simp (config := {decide := true}) only [ + h_s20_non_effects, h_s19_non_effects, h_s18_non_effects, h_s17_x3, h_s16_non_effects, h_s15_non_effects, - h_s14_non_effects, h_step_21, + h_s14_non_effects, h_step_21, h_s13_x3, state_simp_rules, bitvec_rules, minimal_theory] - simp (config := {ground := true}) only [h_s13_x3, minimal_theory] -- sym_n 7 at s21 init_next_step h_run h_step_29 s29 replace h_step_29 := h_step_29.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_29<;> try assumption simp only [state_simp_rules] at h_s21_x3 - simp only [h_s28_non_effects, h_s27_non_effects, h_s26_non_effects, + simp (config := { decide := true }) only [ + h_s28_non_effects, h_s27_non_effects, h_s26_non_effects, h_s25_flagN, h_s25_flagV, h_s25_flagZ, h_s25_flagC, h_s24_non_effects, h_s23_non_effects, h_s22_non_effects, state_simp_rules, bitvec_rules, minimal_theory, -- hypothesis that states x3's value h_s21_x3] at h_step_29 - simp (config := {ground := true}) only [minimal_theory] at h_step_29 (intro_fetch_decode_lemmas h_step_29 h_s28_program "h_s28") -- Add hypotheses that are needed for next loop iteration -- This is an aggregated result have h_s29_x3 : read_gpr 32 3#5 s29 = 6#32 := by - simp only [h_s28_non_effects, h_s27_non_effects, h_s26_non_effects, + simp (config := { decide := true }) only [ + h_s28_non_effects, h_s27_non_effects, h_s26_non_effects, h_s25_x3, h_s24_non_effects, h_s23_non_effects, - h_s22_non_effects, h_step_29, + h_s22_non_effects, h_step_29, h_s21_x3, state_simp_rules, bitvec_rules, minimal_theory] - simp (config := {ground := true}) only [h_s21_x3, minimal_theory] -- sym_n 7 at s29 init_next_step h_run h_step_37 s37 replace h_step_37 := h_step_37.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_37<;> try assumption simp only [state_simp_rules] at h_s29_x3 - simp only [h_s36_non_effects, h_s35_non_effects, h_s34_non_effects, + simp (config := { decide := true }) only [ + h_s36_non_effects, h_s35_non_effects, h_s34_non_effects, h_s33_flagN, h_s33_flagV, h_s33_flagZ, h_s33_flagC, h_s32_non_effects, h_s31_non_effects, h_s30_non_effects, state_simp_rules, bitvec_rules, minimal_theory, -- hypothesis that states x3's value h_s29_x3] at h_step_37 - simp (config := {ground := true}) only [minimal_theory] at h_step_37 (intro_fetch_decode_lemmas h_step_37 h_s36_program "h_s36") -- Add hypotheses that are needed for next loop iteration -- This is an aggregated result have h_s37_x3 : read_gpr 32 3#5 s37 = 4#32 := by - simp only [h_s36_non_effects, h_s35_non_effects, h_s34_non_effects, + simp (config := { decide := true }) only [ + h_s36_non_effects, h_s35_non_effects, h_s34_non_effects, h_s33_x3, h_s32_non_effects, h_s31_non_effects, - h_s30_non_effects, h_step_37, + h_s30_non_effects, h_step_37, h_s29_x3, state_simp_rules, bitvec_rules, minimal_theory] - simp (config := {ground := true}) only [h_s29_x3, minimal_theory] -- sym_n 7 at s37 init_next_step h_run h_step_45 s45 replace h_step_45 := h_step_45.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_45<;> try assumption simp only [state_simp_rules] at h_s37_x3 - simp only [h_s44_non_effects, h_s43_non_effects, h_s42_non_effects, + simp (config := { decide := true }) only [ + h_s44_non_effects, h_s43_non_effects, h_s42_non_effects, h_s41_flagN, h_s41_flagV, h_s41_flagZ, h_s41_flagC, h_s40_non_effects, h_s39_non_effects, h_s38_non_effects, state_simp_rules, bitvec_rules, minimal_theory, -- hypothesis that states x3's value h_s37_x3] at h_step_45 - simp (config := {ground := true}) only [minimal_theory] at h_step_45 (intro_fetch_decode_lemmas h_step_45 h_s44_program "h_s44") -- Add hypotheses that are needed for next loop iteration -- This is an aggregated result have h_s45_x3 : read_gpr 32 3#5 s45 = 2#32 := by - simp only [h_s44_non_effects, h_s43_non_effects, h_s42_non_effects, + simp (config := { decide := true }) only [ + h_s44_non_effects, h_s43_non_effects, h_s42_non_effects, h_s41_x3, h_s40_non_effects, h_s39_non_effects, - h_s38_non_effects, h_step_45, + h_s38_non_effects, h_step_45, h_s37_x3, state_simp_rules, bitvec_rules, minimal_theory] - simp (config := {ground := true}) only [h_s37_x3, minimal_theory] -- sym_n 7 at s45 init_next_step h_run h_step_53 s53 replace h_step_53 := h_step_53.symm rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_53<;> try assumption simp only [state_simp_rules] at h_s45_x3 - simp only [h_s52_non_effects, h_s51_non_effects, h_s50_non_effects, + simp (config := { decide := true }) only [ + h_s52_non_effects, h_s51_non_effects, h_s50_non_effects, h_s49_flagN, h_s49_flagV, h_s49_flagZ, h_s49_flagC, h_s48_non_effects, h_s47_non_effects, h_s46_non_effects, state_simp_rules, bitvec_rules, minimal_theory, -- hypothesis that states x3's value h_s45_x3] at h_step_53 - simp (config := {ground := true}) only [minimal_theory] at h_step_53 (intro_fetch_decode_lemmas h_step_53 h_s52_program "h_s52") -- sym_n 7 at s53 diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean index 529d14ca..1c707de3 100644 --- a/Proofs/AES-GCM/GCMGmultV8Sym.lean +++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean @@ -203,7 +203,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState) -- Split conjunction repeat' apply And.intro · simp_mem; rfl - · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp] + · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp] at * sym_aggregate · intro n addr h_separate simp_mem diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean index 732b50dd..6aa983a9 100644 --- a/Proofs/Popcount32.lean +++ b/Proofs/Popcount32.lean @@ -100,7 +100,9 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState) simp only [popcount32_spec, popcount32_spec_rec] bv_decide · -- Register Frame Condition - simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]; sym_aggregate + simp only [List.mem_cons, List.mem_singleton, not_or, and_imp, + List.not_mem_nil, not_false_eq_true, true_implies] at * + sym_aggregate · -- Memory Frame Condition intro n addr h_separate simp only [memory_rules] at * diff --git a/Tactics/Aggregate.lean b/Tactics/Aggregate.lean index f4197f0b..632f7df6 100644 --- a/Tactics/Aggregate.lean +++ b/Tactics/Aggregate.lean @@ -85,7 +85,7 @@ elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMain searchLCtxFor (whenFound := whenFound) /- By matching under binders, this also matches for non-effect hypotheses, which look like: - `∀ f, f ≠ _ → r f ?state = ?rhs` + `∀ f, f ∉ […] → r f ?state = ?rhs` -/ (matchUnderBinders := true) (expectedType := do diff --git a/Tactics/Common.lean b/Tactics/Common.lean index 5d0f78eb..ea115419 100644 --- a/Tactics/Common.lean +++ b/Tactics/Common.lean @@ -284,6 +284,50 @@ def mkMemory : Expr := mkConst ``Memory def mkEqReflMemory (x : Expr) : Expr := mkApp2 (.const ``Eq.refl [1]) mkMemory x +/-- Return ` ∈ `, given expressions `α : Type u`, `x : α` +and `xs : List α` -/ +def mkListMem (u : Level) (α x xs : Expr) : Expr := + let list := mkApp (.const ``List [u]) α + let inst := mkApp (.const ``List.instMembership [u]) α + mkApp5 (.const ``Membership.mem [u,u]) α list inst xs x + +/-- Return ` ∈ `, given expressions `f : StateField` +and `fs : List StateField` -/ +def mkStateFieldListMem (f fs : Expr) : Expr := + mkListMem 0 (mkConst ``StateField) f fs + +/-- Return a proof of type ` ∈ `, given expressions `α : Type u`, `x : α` +and `xs : List α`, assuming that `xs` is of the form `[x₁, x₂, ⋯, xₙ]` and that +`x` is *syntactically* equal to one of the elements `xᵢ`. + +Returns `none` if the proof could not be constructed -/ +partial def mkListMemProof (u : Level) (α x xs : Expr) : Option Expr := do + let_expr List.cons _α hd tl := xs | none + if hd == x then + mkApp3 (.const ``List.Mem.head [u]) α x tl + else + mkApp5 (.const ``List.Mem.tail [u]) α x hd tl (← mkListMemProof u α x tl) + +/-- auxiliary lemma for use in `mkNeProofOfMemAndNotMem` -/ +private theorem mkNeProofOfNotMemAndMem.aux.{u} + {α : Type u} {x y : α} {xs : List α} + (h_not_mem : x ∉ xs) (h_mem : y ∈ xs) : + x ≠ y := by + rintro rfl; contradiction + +/-- Return a proof of type ` ≠ `, given proofs +`nonMemProof : ∉ ` and `memProof : ∈ `, assuming that +`α : Type u`, `x y : α`, and `xs : List α` -/ +@[inline] def mkNeProofOfNotMemAndMem (u : Level) (α x y xs nonMemProof memProof : Expr) : + Expr := + mkApp6 (.const ``mkNeProofOfNotMemAndMem.aux [u]) α x y xs + nonMemProof memProof + +/-- Return a proof of ` ∉ `, given `notMemProof : ∉ :: xs`, +assuming that `α : Type u`, `x y : α`, and `xs : List α` -/ +@[inline] def mkNotMemOfNotMemCons (u : Level) (α x y xs notMemProof : Expr) : Expr := + mkApp5 (.const ``List.not_mem_of_not_mem_cons [u]) α x y xs notMemProof + /-! ## 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..e701ca41 100644 --- a/Tactics/Sym/AxEffects.lean +++ b/Tactics/Sym/AxEffects.lean @@ -54,7 +54,7 @@ structure AxEffects where fields : Std.HashMap StateField AxEffects.FieldEffect /-- An expression that contains the proof of: ```lean - ∀ (f : StateField), f ≠ → ⋯ → f ≠ → + ∀ (f : StateField), f ∉ [f₁, ⋯, fₙ] → r f = r f ` ``` where `f₁, ⋯, fₙ` are the keys of `fields` @@ -125,9 +125,13 @@ def initial (state : Expr) : AxEffects where currentState := state fields := .empty nonEffectProof := - -- `fun f => rfl` - mkLambda `f .default (mkConst ``StateField) <| - mkEqReflArmState <| mkApp2 (mkConst ``r) (.bvar 0) state + -- `fun (f : StateField) (h : f ∉ []) => rfl` + let SF := mkConst ``StateField + mkLambda `f .default SF <| + let f_nin_nil := -- `f ∉ []` + mkNot <| mkStateFieldListMem (.bvar 0) (mkApp (.const ``List.nil [0]) SF) + mkLambda `h .default f_nin_nil <| + mkEqReflArmState <| mkApp2 (mkConst ``r) (.bvar 1) state memoryEffects := .initial state programProof := -- `rfl` @@ -192,21 +196,18 @@ private def rewriteType (e eq : Expr) : MetaM Expr := do 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 msg (tag := "mkAppNonEffect") <| do - trace[Tactic.sym] "nonEffectProof: {eff.nonEffectProof}" + Sym.withTraceNode msg (tag := "mkAppNonEffect") <| do + Sym.traceLargeMsg "nonEffectProof" m!"{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 (Expr.forallE _name binderType _body _) := typeOfNonEffects + | throwError m!"internal error: expected a forall, found:\n {typeOfNonEffects}" + trace[Tactic.sym] "non-effect precondition: {binderType}" - let nonEffectProof := mkAppN nonEffectProof pre - trace[Tactic.sym] "constructed: {nonEffectProof}" - return nonEffectProof + let nonMemProof ← mkDecideProof binderType + Sym.traceLargeMsg "constructed proof of precondition" m!"{nonMemProof}" + return mkApp nonEffectProof nonMemProof /-- Get the value for a field, if one is stored in `eff.fields`, or assemble an instantiation of the non-effects proof otherwise -/ @@ -285,7 +286,6 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) : let memoryEffects ← eff.memoryEffects.updateWriteMem eff.currentState n addr val - -- Update the program proof let programProof ← -- `Eq.trans (@write_mem_bytes_program ...) ` @@ -310,7 +310,7 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) : programProof stackAlignmentProof? } - eff.traceCurrentState + trace[Tactic.sym] "result: {eff}" return eff /-- Execute `w ` against the state stored in `eff` @@ -324,8 +324,8 @@ private def update_w (eff : AxEffects) (fld val : Expr) : Sym.withTraceNode m!"processing: w {fld} {val} …" (tag := "updateWrite") <| do let rField ← reflectStateField fld - -- Update all other fields - let fields ← + -- ### Update all other fields + let otherFields ← eff.fields.toList.filterMapM fun ⟨fld', {value, proof}⟩ => do if fld' ≠ rField then let proof : Expr ← do @@ -340,55 +340,86 @@ private def update_w (eff : AxEffects) (fld val : Expr) : else return none - -- Update the main field + -- ### 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]! + let fields := (rField, newField) :: otherFields + + -- ### Update the non-effects proof + let nonEffectProof ← lambdaBoundedTelescope eff.nonEffectProof 2 fun args proof => do + let [f /- : StateField -/, nonMemHyp /- : f ∉ ?modifiedFields -/] := args.toList + | throwError "internal error: expected exactly two arguments, found:\ + {args}\n\nIn non-effect proof:\n {eff.nonEffectProof}" + + let modifiedFields : Expr /- : List StateField -/ ← do + let ty ← inferType nonMemHyp + let_expr Not ty := ty + | let m ← mkFreshExprMVar none + throwError "interal error: expected f ∉ {m}, found:\n {ty}" + let_expr Membership.mem _α _γ _inst fields _f := ty + | let m ← mkFreshExprMVar none + throwError "interal error: expected f ∈ {m}, found:\n {ty}" + pure fields + trace[Tactic.sym.info] "current precondidition is \ + {nonMemHyp} : {f} ∉ {modifiedFields}" + + let newProofOfNe := fun oldProof neProof /- : ` ≠ ` -/ => do + let r_of_w := + mkApp5 (mkConst ``r_of_w_different) f fld val eff.currentState neProof + mkEqTrans r_of_w oldProof + + let h? := mkListMemProof 0 (mkConst ``StateField) fld modifiedFields + if let some h /- : ` ∈ ` -/ := h? then + -- `fld` was previously modified + + let neProof := -- : ` ≠ ` + mkNeProofOfNotMemAndMem 0 (mkConst ``StateField) f fld modifiedFields h nonMemHyp + -- Adjust the proof + let proof ← newProofOfNe proof neProof + -- And abstract `f` and `nonMemHyp` again, without changing their types + mkLambdaFVars #[f, nonMemHyp] proof - /- 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 effects + else + -- `fld` was *not* previously modified, so we need to change the type of + -- the `nonMemHyp` precondition + + let newModifiedFields := -- ` :: ` + mkApp3 (.const ``List.cons [0]) (mkConst ``StateField) fld modifiedFields + trace[Tactic.sym.info] "{fld} was not previously modified, the new list \ + of modified fields is {newModifiedFields}" + + withLocalDeclD `h (mkNot <| mkStateFieldListMem f newModifiedFields) fun newNonMemHyp => do + let proof := proof.replaceFVar nonMemHyp <| + mkNotMemOfNotMemCons 0 (mkConst ``StateField) f fld + modifiedFields newNonMemHyp + + let h := -- : ` ∈ ` + mkApp3 (.const ``List.Mem.head [0]) (mkConst ``StateField) fld modifiedFields + let neProof := -- : ` ≠ ` + mkNeProofOfNotMemAndMem 0 (mkConst ``StateField) f fld + newModifiedFields + newNonMemHyp h + + -- Adjust the proof + let proof ← newProofOfNe proof neProof + -- And abstract `f` and `newNonMemHyp` + mkLambdaFVars #[f, newNonMemHyp] proof + + -- ### Update the memory effects let memoryEffects ← eff.memoryEffects.updateWrite eff.currentState fld val - -- Update the program proof + -- ### Update the program proof let programProof ← -- `Eq.trans (w_program ...) ` mkEqTrans (mkAppN (mkConst ``w_program) #[fld, val, eff.currentState]) eff.programProof - -- Update the stack alignment proof + -- ### Update the stack alignment proof let mut sideConditions := eff.sideConditions let mut stackAlignmentProof? := eff.stackAlignmentProof? if let some proof := stackAlignmentProof? then @@ -416,7 +447,7 @@ private def update_w (eff : AxEffects) (fld val : Expr) : stackAlignmentProof? sideConditions } - eff.traceCurrentState "new state" + trace[Tactic.sym] "result: {eff}" return eff /-- Throw an error if `e` is not of type `expectedType` -/ @@ -492,7 +523,9 @@ def adjustCurrentStateWithEq (eff : AxEffects) (s eq : Expr) : let fields := .ofList fields Sym.withTraceNode m!"rewriting other proofs" (tag := "rewriteMisc") <| do - let nonEffectProof ← rewriteType eff.nonEffectProof eq + trace[Tactic.sym.info] "type of nonEffectProof: {← inferType eff.nonEffectProof}" + let nonEffectProof ← + rewriteType eff.nonEffectProof eq let memoryEffects ← eff.memoryEffects.adjustCurrentStateWithEq eq let programProof ← rewriteType eff.programProof eq let stackAlignmentProof? ← eff.stackAlignmentProof?.mapM @@ -516,7 +549,7 @@ def updateWithEq (eff : AxEffects) (eq : Expr) : MetaM AxEffects := let eff ← eff.updateWithExpr (← instantiateMVars rhs) let eff ← eff.adjustCurrentStateWithEq s eq - eff.traceCurrentState "new state" + eff.traceCurrentState "result …" return eff /-- Given a proof `eq : ?s = `,