tweak algorithm so we can build mem_omega state correctly

leanprover · Oct 10, 2024 · d7ebfc2 · d7ebfc2
1 parent 78e4d64
commit d7ebfc2
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/Arm/Memory/Common.lean b/Arm/Memory/Common.lean
@@ -227,6 +227,9 @@ inductive Hypothesis
 | pairwiseSeparate (proof : MemPairwiseSeparateProof e)
 | read_eq (proof : ReadBytesEqProof)
 
+def Hypothesis.isPairwiseSeparate : Hypothesis → Bool
+| .pairwiseSeparate _ => true
+| _ => false
 
 def Hypothesis.proof : Hypothesis → Expr
 | .pairwiseSeparate proof  => proof.h

diff --git a/Arm/Memory/MemOmega.lean b/Arm/Memory/MemOmega.lean
@@ -80,10 +80,17 @@ def memOmegaTac : MemOmegaM Unit := do
     for h in rawHyps do
       hyps ← hypothesisOfExpr h hyps
 
+    -- used specialized procedure that doesn't unfold everything for the easy case.
     if ← closeMemSideCondition (← getMainGoal) (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then
       return ()
     else
-      let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
+      let pairwise? := (← readThe Context).cfg.explodePairwiseSeparate
+      -- in the bad case, just rip through everything.
+      -- let _ ← Hypothesis.addOmegaFactsOfHyps (hyps.toList.filter (fun h => h.isPairwiseSeparate)) #[]
+      let _ ← Hypothesis.addOmegaFactsOfHyps
+          (hyps.toList.filter (!pairwise? || ·.isPairwiseSeparate))
+          #[]
+
       TacticM.withTraceNode' m!"Reducion to omega" do
         try
           TacticM.traceLargeMsg m!"goal (Note: can be large)"  m!"{← getMainGoal}"