Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: fix proof building in 'mem.read ... = mem.read ...' #227

Merged
merged 2 commits into from
Oct 10, 2024
Merged

chore: fix proof building in 'mem.read ... = mem.read ...' #227

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
61bd3bc
chore: fix proof building in 'mem.read ... = mem.read ...'
bollu Oct 10, 2024
ce74853
Merge branch 'main' into simp-mem-bugfix-read-of-read
shigoel Oct 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Arm/Memory/SeparateAutomation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -314,7 +314,7 @@ we can have some kind of funny situation where both LHS and RHS are ReadBytes.
For example, `mem1.read base1 n = mem2.read base2 n`.
In such a scenario, we should record both reads.
-/
def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) : Array ReadBytesEqProof := Id.run do
def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) : MetaM (Array ReadBytesEqProof) := do
let mut out := #[]
if let .some ⟨_ty, lhs, rhs⟩ := etype.eq? then do
let lhs := lhs
Expand All @@ -323,7 +323,7 @@ def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) : Array ReadBytesEqPr
out := out.push { val := rhs, read := read, h := eval }

if let .some read := ReadBytesExpr.ofExpr? rhs then
out:= out.push { val := lhs, read := read, h := eval }
out:= out.push { val := lhs, read := read, h := ← mkEqSymm eval }
return out

inductive Hypothesis
Expand Down Expand Up @@ -583,7 +583,7 @@ def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothe
return hyps
else
let mut hyps := hyps
for eqProof in ReadBytesEqProof.ofExpr? h ht do
for eqProof in ← ReadBytesEqProof.ofExpr? h ht do
let proof : Hypothesis := .read_eq eqProof
hyps := hyps.push proof
return hyps
Expand Down
10 changes: 3 additions & 7 deletions Proofs/Experiments/MemoryAliasing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,10 +255,6 @@ info: 'ReadOverlappingRead.overlapping_read_test_3' depends on axioms: [propext,
-/
#guard_msgs in #print axioms overlapping_read_test_3

/- TODO(@bollu): This test case hangs at `bv_omega_bench`. This is to be debugged.
/-- A read in the goal state overlaps with a read in the
right hand side of the hypotheis `h`.
-/
theorem overlapping_read_test_4
(hlegal : mem_legal' src_addr 16)
(h : read_mem_bytes 16 other_addr s = read_mem_bytes 16 src_addr s) :
Expand All @@ -268,11 +264,11 @@ theorem overlapping_read_test_4
simp only [memory_rules] at h ⊢
simp_mem
· congr
-- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
bv_omega_bench -- TODO: Lean gets stuck here?
bv_omega

/-- info: 'ReadOverlappingRead.overlapping_read_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms overlapping_read_test_4
-/

end ReadOverlappingRead

namespace ReadOverlappingWrite
Expand Down
Loading