diff --git a/Arm/Memory/Common.lean b/Arm/Memory/Common.lean index 428d1d28..77564952 100644 --- a/Arm/Memory/Common.lean +++ b/Arm/Memory/Common.lean @@ -783,6 +783,7 @@ An example is `mem_lega'.of_omega n a`, which has type: a way to convert `e : α` into the `omegaToDesiredFactFnVal`. -/ def proveWithOmega? {α : Type} [ToMessageData α] [OmegaReducible α] (e : α) + (extraOmegaAssumptions : Array Expr) (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) (hyps : Array Memory.Hypothesis) : MetaM (Option (Proof α e)) := do -- TODO: refactor to use mkProofGoalForOmega @@ -800,9 +801,9 @@ def proveWithOmega? {α : Type} [ToMessageData α] [OmegaReducible α] (e : α) let g := omegaObligationVal.mvarId! g.withContext do try - let (_, g) ← Hypothesis.addOmegaFactsOfHyps g hyps.toList #[] + let (omegaAssumptions, g) ← Hypothesis.addOmegaFactsOfHyps g hyps.toList #[] trace[simp_mem.info] m!"Executing `omega` to close {e}" - omega g (← getLocalHyps) bvToNatSimpCtx bvToNatSimprocs + omega g (omegaAssumptions ++ extraOmegaAssumptions) bvToNatSimpCtx bvToNatSimprocs trace[simp_mem.info] "{checkEmoji} `omega` succeeded." return (.some <| Proof.mk (← instantiateMVars factProof)) catch e => @@ -811,6 +812,10 @@ def proveWithOmega? {α : Type} [ToMessageData α] [OmegaReducible α] (e : α) end ReductionToOmega +/-- Collect nondependent hypotheses that are propositions. -/ +def _root_.Lean.MVarId.getNondepPropExprs (g : MVarId) : MetaM (Array Expr) := do + return ((← g.getNondepPropHyps).map Expr.fvar) + /-- simplify the goal state, closing legality, subset, and separation goals, and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise. @@ -818,20 +823,21 @@ and simplifying all other expressions. return `true` if goal has been closed, an partial def closeMemSideCondition (g : MVarId) (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) (hyps : Array Memory.Hypothesis) : MetaM Bool := do + -- TODO: take user selected hyps. g.withContext do trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}" let gt ← g.getType if let .some e := MemLegalProp.ofExpr? gt then TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do - if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then + if let .some proof ← proveWithOmega? e (← g.getNondepPropExprs) bvToNatSimpCtx bvToNatSimprocs hyps then g.assign proof.h if let .some e := MemSubsetProp.ofExpr? gt then TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do - if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then + if let .some proof ← proveWithOmega? e (← g.getNondepPropExprs) bvToNatSimpCtx bvToNatSimprocs hyps then g.assign proof.h if let .some e := MemSeparateProp.ofExpr? gt then TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do - if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then + if let .some proof ← proveWithOmega? e (← g.getNondepPropExprs) bvToNatSimpCtx bvToNatSimprocs hyps then g.assign proof.h return ← g.isAssigned diff --git a/Arm/Memory/MemOmega.lean b/Arm/Memory/MemOmega.lean index be4966d0..2c1eec75 100644 --- a/Arm/Memory/MemOmega.lean +++ b/Arm/Memory/MemOmega.lean @@ -104,33 +104,31 @@ def mkKeepHypsOfUserHyp (g : MVarId) (set : Std.HashSet FVarId) (hyp : UserHyp) | .expr _e => return set /-- -Given the user hypotheses, build a more focusedd MVarId that contains only those hypotheses. -This makes `omega` focus only on those hypotheses, since omega by default crawls the entire goal state. +Fold over the array of `UserHyps`, build tracking `FVarId`s for the ones that we use. +if the array is `.none`, then we keep everything. +-/ +def mkKeepHypsOfUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| Std.HashSet FVarId := + (userHyps?.getD #[]).foldlM (init := ∅) (MemOmega.mkKeepHypsOfUserHyp g) -This is arguably a workaround to having to plumb the hypotheses through the full layers of code, but it works, -and should be a cheap solution. +/-- Fold over the array of `UserHyps`, build tracking `FVarId`s for the ones that we use. +if the array is `.none`, then we keep everything. -/ -def mkGoalWithOnlyUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| MVarId := - match userHyps? with - | none => pure g - | some userHyps => do - g.withContext do - let mut keepHyps : Std.HashSet FVarId ← userHyps.foldlM - (init := ∅) - (mkKeepHypsOfUserHyp g) - let hyps ← g.getNondepPropHyps - let mut g := g - for h in hyps do - if !keepHyps.contains h then - try - g ← g.withContext <| g.clear h - catch e => - let hname := (← getLCtx).get! h |>.userName - throwTacticEx `simp_mem g <| .some m!"unable to clear hypothesis '{hname}' when trying to focus on hypotheses.{Format.line}Consider adding '{hname}' to the set of retained hypotheses.{Format.line}Error from `clear` is: {indentD e.toMessageData}" - return g +def mkMemoryAndKeepHypsOfUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| Array Memory.Hypothesis × Array FVarId := do + let keepHyps : Std.HashSet FVarId ← mkKeepHypsOfUserHyps g userHyps? + g.withContext do + let mut foundHyps : Array Memory.Hypothesis := #[] + let mut nonmem := #[] + for h in keepHyps do + let sz := foundHyps.size + foundHyps ← hypothesisOfExpr (Expr.fvar h) foundHyps + if foundHyps.size == sz then + -- size did not change, so that was a non memory hyp. + nonmem := nonmem.push h + return (foundHyps, nonmem) + + def memOmega (g : MVarId) : MemOmegaM Unit := do - let g ← mkGoalWithOnlyUserHyps g (← readThe Context).userHyps? g.withContext do let rawHyps ← getLocalHyps let mut hyps := #[] @@ -159,7 +157,6 @@ def memOmega (g : MVarId) : MemOmegaM Unit := do throw e def memOmegaWithHyps (g : MVarId) (rawHyps : Array FVarId) : MemOmegaM Unit := do - let g ← mkGoalWithOnlyUserHyps g (← readThe Context).userHyps? g.withContext do let mut hyps := #[] -- extract out structed values for all hyps. diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 259a594a..72fdb69c 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -211,21 +211,21 @@ def getConfig : SimpMemM SimpMemConfig := do #guard_msgs in #check state_value -def SimpMemM.findOverlappingReadHypAux (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) (hReadEq : ReadBytesEqProof) : +def SimpMemM.findOverlappingReadHypAux (extraOmegaHyps : Array Expr) (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) (hReadEq : ReadBytesEqProof) : SimpMemM <| Option (MemSubsetProof { sa := er.span, sb := hReadEq.read.span }) := do withTraceNode m!"{processingEmoji} ... ⊆ {hReadEq.read.span} ? " do -- the read we are analyzing should be a subset of the hypothesis let subset := (MemSubsetProp.mk er.span hReadEq.read.span) - let some hSubsetProof ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps + let some hSubsetProof ← proveWithOmega? subset extraOmegaHyps (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps | return none return some (hSubsetProof) -def SimpMemM.findOverlappingReadHyp (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) : +def SimpMemM.findOverlappingReadHyp (extraOmegaHyps : Array Expr) (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) : SimpMemM <| Option (Σ (hread : ReadBytesEqProof), MemSubsetProof { sa := er.span, sb := hread.read.span }) := do for hyp in hyps do let Hypothesis.read_eq hReadEq := hyp | continue - let some subsetProof ← SimpMemM.findOverlappingReadHypAux hyps er hReadEq + let some subsetProof ← SimpMemM.findOverlappingReadHypAux extraOmegaHyps hyps er hReadEq | continue return some ⟨hReadEq, subsetProof⟩ return none @@ -274,12 +274,12 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) : let separate := MemSeparateProp.mk er.span ew.span let subset := MemSubsetProp.mk er.span ew.span - if let .some separateProof ← proveWithOmega? separate (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do + if let .some separateProof ← proveWithOmega? separate (← (← getMainGoal).getNondepPropExprs) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do trace[simp_mem.info] "{checkEmoji} {separate}" let result ← MemSeparateProof.rewriteReadOfSeparatedWrite er ew separateProof e setChanged return result - else if let .some subsetProof ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do + else if let .some subsetProof ← proveWithOmega? subset (← (← getMainGoal).getNondepPropExprs) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do trace[simp_mem.info] "{checkEmoji} {subset}" let result ← MemSubsetProof.rewriteReadOfSubsetWrite er ew subsetProof e setChanged @@ -294,7 +294,7 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) : -- we can add the theorem that `(write region).read = write val`. -- Then this generic theory will take care of it. withTraceNode m!"Searching for overlapping read {er.span}." do - let some ⟨hReadEq, hSubsetProof⟩ ← findOverlappingReadHyp hyps er + let some ⟨hReadEq, hSubsetProof⟩ ← findOverlappingReadHyp (← (← getMainGoal).getNondepPropExprs) hyps er | SimpMemM.walkExpr e hyps let out ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq hSubsetProof e setChanged @@ -345,9 +345,8 @@ partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Memory.Hypothesis) replaceMainGoal [newGoal] end -def SimpMemM.findMemoryHyps (g : MVarId) : SimpMemM <| Array Memory.Hypothesis := do +def SimpMemM.mkMemoryHypsFrom (g : MVarId) (hyps : (Array Expr)) : SimpMemM <| Array Memory.Hypothesis := do g.withContext do - let hyps := (← getLocalHyps) withTraceNode m!"Searching for Hypotheses" do let mut foundHyps : Array Memory.Hypothesis := #[] for h in hyps do @@ -411,35 +410,35 @@ def SimpMemM.simplifySupervisedCore (g : MVarId) (e : Expr) (guidance : Guidance let .some ew := WriteBytesExpr.ofExpr? er.mem | throwError "{crossEmoji} expected to find read of write based on '⊂' guidance, but found read of '{er.mem}'" let subset := MemSubsetProp.mk er.span ew.span - let g ← withContext g <| MemOmega.mkGoalWithOnlyUserHyps g guidance.userHyps? + /- TODO: replace the use of throwError with telling the user to prove the goals if enabled. -/ + let keepHyps : Std.HashSet FVarId ← (guidance.userHyps?.getD #[]).foldlM (init := ∅) (fun s uh => MemOmega.mkKeepHypsOfUserHyp g s uh) + let keepHyps := (keepHyps.toArray.map Expr.fvar) + let hyps ← SimpMemM.mkMemoryHypsFrom g keepHyps withContext g do - let hyps ← SimpMemM.findMemoryHyps g - /- TODO: replace the use of throwError with telling the user to prove the goals if enabled. -/ - let (subsetProof, gs) ← do - match ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with - | .some p => pure (p, #[]) - | .none => do - Meta.logWarning m!"simp_mem: Unable to prove subset {subset}, creating user obligation." - let (p, g') ← mkProofGoalForOmega subset - pure (p, #[g']) - return (← MemSubsetProof.rewriteReadOfSubsetWrite er ew subsetProof e, gs) + match ← proveWithOmega? subset keepHyps (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with + | .some p => + return (← MemSubsetProof.rewriteReadOfSubsetWrite er ew p e, #[]) + | .none => do + Meta.logWarning m!"simp_mem: Unable to prove subset {subset}, creating user obligation." + let (p, g') ← mkProofGoalForOmega subset + return (← MemSubsetProof.rewriteReadOfSubsetWrite er ew p e, #[g']) | .separateWrite => -- TODO: unify code with other branch. let .some ew := WriteBytesExpr.ofExpr? er.mem | throwError "{crossEmoji} expected to find read of write based on '⟂' guidance, but found read of '{er.mem}'" - let g ← withContext g <| MemOmega.mkGoalWithOnlyUserHyps g guidance.userHyps? - withContext g do - let hyps ← SimpMemM.findMemoryHyps g - let separate := MemSeparateProp.mk er.span ew.span + let separate := MemSeparateProp.mk er.span ew.span + let keepHyps : Std.HashSet FVarId ← (guidance.userHyps?.getD #[]).foldlM (init := ∅) (fun s uh => MemOmega.mkKeepHypsOfUserHyp g s uh) + let keepHyps := (keepHyps.toArray.map Expr.fvar) + let hyps ← SimpMemM.mkMemoryHypsFrom g keepHyps /- TODO: replace the use of throwError with telling the user to prove the goals if enabled. -/ - let (separateProof, gs) ← do - match ← proveWithOmega? separate (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with - | .some p => pure (p, #[]) + withContext g do + match ← proveWithOmega? separate keepHyps (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with + | .some p => + return (← MemSeparateProof.rewriteReadOfSeparatedWrite er ew p e, #[]) | .none => do Meta.logWarning m!"simp_mem: Unable to prove separate {separate}, creating user obligation." let (p, g') ← mkProofGoalForOmega separate - pure (p, #[g']) - pure (← MemSeparateProof.rewriteReadOfSeparatedWrite er ew separateProof e, gs) + return (← MemSeparateProof.rewriteReadOfSeparatedWrite er ew p e, #[g']) | .subsetRead hread? => do -- If the user has provided guidance hypotheses, add the user hypothesis to this list. -- If the user has not provided guidance hypotheses, then we don't filter the list, so @@ -451,34 +450,36 @@ def SimpMemM.simplifySupervisedCore (g : MVarId) (e : Expr) (guidance : Guidance -- -- User wants filtering, and wants this read hypothesis to be used. -- -- Add it into the set of user provided hypotheses. | (.some userHyps, .some readHyp) => .some <| userHyps.push (MemOmega.UserHyp.ofExpr readHyp) - let g ← withContext g <| MemOmega.mkGoalWithOnlyUserHyps g userHyps? - let hyps ← SimpMemM.findMemoryHyps g - match hread? with - | .none => do - /- - User hasn't given us a read, so find a read. No recovery possible, - Because the expression we want to rewrite into depends on knowing what the read was. - -/ - let .some ⟨hreadEq, proof⟩ ← findOverlappingReadHyp hyps er - | throwError "{crossEmoji} unable to find overlapping read for {er}" - return (← MemSubsetProof.rewriteReadOfSubsetRead er hreadEq proof e, #[]) - | .some hyp => do - /- - User has given us a read, prove that it works. - TODO: replace the use of throwError with telling the user to prove the goals if enabled. - -/ - let .some hReadEq := (← ReadBytesEqProof.ofExpr? hyp (← inferType hyp)).get? 0 - | throwError "{crossEmoji} expected user provided read hypohesis {hyp} to be a read" - let subset := (MemSubsetProp.mk er.span hReadEq.read.span) - match ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with - | .some p => do - let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e - return (result, #[]) - | .none => do - Meta.logWarning m!"simp_mem: Unable to prove read subset {subset}, creating user obligation." - let (p, g') ← mkProofGoalForOmega subset - let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e - return (result, #[g']) + let keepHyps : Std.HashSet FVarId ← (userHyps?.getD #[]).foldlM (init := ∅) (fun s uh => MemOmega.mkKeepHypsOfUserHyp g s uh) + let keepHyps := (keepHyps.toArray.map Expr.fvar) + -- TODO: build keepHyps from Hypothesis. + let hyps ← SimpMemM.mkMemoryHypsFrom g keepHyps + match hread? with + | .none => do + /- + User hasn't given us a read, so find a read. No recovery possible, + Because the expression we want to rewrite into depends on knowing what the read was. + -/ + let .some ⟨hreadEq, proof⟩ ← findOverlappingReadHyp keepHyps hyps er + | throwError "{crossEmoji} unable to find overlapping read for {er}" + return (← MemSubsetProof.rewriteReadOfSubsetRead er hreadEq proof e, #[]) + | .some hyp => do + /- + User has given us a read, prove that it works. + TODO: replace the use of throwError with telling the user to prove the goals if enabled. + -/ + let .some hReadEq := (← ReadBytesEqProof.ofExpr? hyp (← inferType hyp)).get? 0 + | throwError "{crossEmoji} expected user provided read hypohesis {hyp} to be a read" + let subset := (MemSubsetProp.mk er.span hReadEq.read.span) + match ← proveWithOmega? subset keepHyps (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with + | .some p => do + let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e + return (result, #[]) + | .none => do + Meta.logWarning m!"simp_mem: Unable to prove read subset {subset}, creating user obligation." + let (p, g') ← mkProofGoalForOmega subset + let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e + return (result, #[g']) partial def SimpMemM.simplifySupervised (g : MVarId) (guidances : Array Guidance) : SimpMemM Unit := do diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 16412299..1c8cc16f 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -227,12 +227,14 @@ info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat' /-- info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat' +[simp_mem.info] ⚙️ Processing 'h'' : 'a ≤ 100' [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1' [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1 [simp_mem.info] Adding omega facts from hypotheses [simp_mem.info] Reducion to omega [simp_mem.info] goal (Note: can be large) (NOTE: can be large) [simp_mem.info] a : Nat + h' : a ≤ 100 hab : a ≤ a + 1 ⊢ a ≤ a + 1 [simp_mem.info] ✅️ `omega` succeeded. @@ -248,17 +250,19 @@ warning: unused variable `hab` note: this linter can be disabled with `set_option linter.unusedVariables false` --- info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat' +[simp_mem.info] ⚙️ Processing 'h'' : 'a ≤ 100' [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1' [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1 [simp_mem.info] Adding omega facts from hypotheses [simp_mem.info] Reducion to omega [simp_mem.info] goal (Note: can be large) (NOTE: can be large) [simp_mem.info] a : Nat + h' : a ≤ 100 hab : a ≤ a + 1 ⊢ a ≤ a + 1 [simp_mem.info] ✅️ `omega` succeeded. -/ -#guard_msgs in +#guard_msgs in -- TODO: fix this, we shouldn't process h! set_option trace.simp_mem.info true in example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by mem_omega with [*, -h'] -- correctly exclude h' and include hab, so processing should not mention h'. @@ -284,7 +288,7 @@ theorem mem_automation_test_1_conv_all_hyps simp only [memory_rules] conv => lhs - simp_mem sep + simp_mem sep with [*] #time theorem mem_automation_test_1_conv_focused_hyp @@ -327,7 +331,7 @@ theorem mem_automation_test_2_conv simp only [memory_rules] conv => lhs - simp_mem sep + simp_mem sep with [*] theorem mem_automation_test_2_conv_focus (h_n0 : n0 ≠ 0) @@ -410,7 +414,7 @@ theorem mem_automation_test_4_conv simp only [memory_rules] conv => lhs - simp_mem sep, sub + simp_mem sep with [*], sub with [*] congr 1 bv_omega_bench -- TODO: address normalization. @@ -431,7 +435,7 @@ theorem mem_automation_test_4_conv_focused simp only [memory_rules] conv => lhs - simp_mem sep with [h_no_wrap_src_region, h_s0_src_ignore_disjoint], sub + simp_mem sep with [h_no_wrap_src_region, h_s0_src_ignore_disjoint], sub with [*] congr 1 bv_omega_bench -- TODO: address normalization. @@ -458,7 +462,7 @@ theorem overlapping_read_test_1_conv {out : BitVec (16 * 8)} simp only [memory_rules] at h ⊢ conv => lhs - simp_mem ⊆r at h + simp_mem ⊆r at h with [*] simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq] /-- A read overlapping with another read. -/ @@ -469,7 +473,7 @@ theorem overlapping_read_test_1_conv_search_read {out : BitVec (16 * 8)} simp only [memory_rules] at h ⊢ conv => lhs - simp_mem ⊆r + simp_mem ⊆r with [*] simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq] /-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/ @@ -500,7 +504,7 @@ theorem overlapping_read_test_2_conv {out : BitVec (16 * 8)} simp only [memory_rules] at h ⊢ conv => lhs - simp_mem ⊆r at h + simp_mem ⊆r at h with [*] · congr -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6 bv_omega_bench @@ -649,7 +653,7 @@ theorem irrelvant_hyps simp only [memory_rules] conv => lhs - simp_mem sep with [h_s0_src_dest_separate, h_irrelevant] + simp_mem sep with [h_s0_src_dest_separate] -- rfl end SimpMemConv