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

feat: add automation support for pairwise memory separation #126

Merged
merged 21 commits into from
Sep 6, 2024
Merged

feat: add automation support for pairwise memory separation #126

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
f55ff94
chore: add defn for List.pairwise mem_separate xs
bollu Aug 27, 2024
3e7ba47
chore: completely untested code for separation
bollu Aug 27, 2024
35f5e6c
chore: don't use decideProof in ways that don't work
bollu Aug 27, 2024
80454da
chore: I don't understand this failure
bollu Aug 27, 2024
f2877b9
chore: add separate example
bollu Aug 27, 2024
13e12ef
chore: add examples for pairwise
bollu Aug 27, 2024
16ec26c
chore: show example where better address normalization is needed
bollu Aug 27, 2024
f9d879a
chore: cleanup
bollu Aug 27, 2024
a8a8f64
chore: touchup
bollu Aug 27, 2024
75c3435
metaprogramming nits
bollu Aug 27, 2024
d71b7b4
feat: cleanup
bollu Sep 3, 2024
d1facdd
Merge branch 'main' into mem-pairwise
shigoel Sep 3, 2024
56d5154
Update Proofs/Experiments/MemoryAliasing.lean
bollu Sep 4, 2024
d38e1a5
chore: scope trace enablement
bollu Sep 4, 2024
743c4e3
Merge remote-tracking branch 'origin/mem-pairwise' into mem-pairwise
bollu Sep 4, 2024
34ded47
chore: simp only
bollu Sep 4, 2024
dd24b6d
chore: use custom simp set
bollu Sep 4, 2024
46c2947
Merge branch 'main' into mem-pairwise
shigoel Sep 4, 2024
194b745
Merge branch 'main' into mem-pairwise
shigoel Sep 5, 2024
67618c4
Merge branch 'main' into mem-pairwise
shigoel Sep 5, 2024
2bf5368
Merge branch 'main' into mem-pairwise
shigoel Sep 6, 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
2 changes: 1 addition & 1 deletion Arm/Memory/Separate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,7 @@ theorem Memory.read_bytes_write_bytes_eq_of_mem_subset'
· subst hxn
exfalso
have h := i.isLt
simp at h
simp only [Nat.reduceMul, Nat.zero_mul, Nat.not_lt_zero] at h
· by_cases h₁ : ↑i < xn * 8
· simp only [h₁]
simp only [decide_True, Bool.true_and]
Expand Down
20 changes: 17 additions & 3 deletions Arm/Memory/SeparateAutomation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,6 +373,9 @@ def getConfig : SimpMemM SimpMemConfig := do
let ctx ← read
return ctx.cfg

/-- info: state_value (fld : StateField) : Type -/
#guard_msgs in #check state_value

/-
Introduce a new definition into the local context, simplify it using `simp`,
and return the FVarId of the new definition in the goal.
Expand All @@ -385,9 +388,20 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do
let hdefTy ← inferType hdefVal

/- Simp to gain some more juice out of the defn.. -/
let (simpCtx, simprocs) ← LNSymSimpContext
(config := { decide := false, failIfUnchanged := false })
let (simpResult, _stats) ← simp hdefTy simpCtx simprocs
let mut simpTheorems : Array SimpTheorems := #[]
for a in #[`minimal_theory, `bitvec_rules] do
let some ext ← (getSimpExtension? a)
| throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
simpTheorems := simpTheorems.push (← ext.getTheorems)

-- unfold `state_value.
simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
let simpCtx : Simp.Context := {
simpTheorems,
config := { decide := true, failIfUnchanged := false },
congrTheorems := (← Meta.getSimpCongrTheorems)
}
Comment on lines +391 to +403
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let mut simpTheorems : Array SimpTheorems := #[]
for a in #[`minimal_theory, `bitvec_rules] do
let some ext ← (getSimpExtension? a)
| throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
simpTheorems := simpTheorems.push (← ext.getTheorems)
-- unfold `state_value.
simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
let simpCtx : Simp.Context := {
simpTheorems,
config := { decide := true, failIfUnchanged := false },
congrTheorems := (← Meta.getSimpCongrTheorems)
}
LNSymSimpContext
(config := { decide := false, failIfUnchanged := false })
(simp_attrs := #[`minimal_theory, `bitvec_rules])
(decls_to_unfold := #[state_value])

@bollu I believe LNSymSimpContext can work here. Fair warning: haven't tried out the suggestion, excuse typos, etc.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, open to making LNSymSimpContext nicer (separate issue).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@shigoel I think I would prefer to keep it as-is, because it's hard to see what LNSymSimpContext builds unless one goes and reads its code. Since this code is meant to be performant, I would rather have the building of the simp-set inline, so it's easy to audit.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Weren't you using LNSymSimpContext before though?
dd24b6d

Not a big deal, but I want to make sure I understand what the reasons are.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, I was reusing LNSymSimpContext to make sure that if LNSymSimpContext got more powerful, I would get the same power for free :) But thinking this through, I found your argument for why this should not be expensive to be compelling. Therefore, I'd prefer to build a custom simp-set that's tuned down, and to add power to it as necessary.

From an engineering perspective, I'm advocating for [WET / write everything twice] (https://en.wikipedia.org/wiki/Rule_of_three_(computer_programming)) instead of DRY. 😉

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Gotcha, though I would note that the particular invocation of LNSymSimpContext is equivalent to what you wrote inline.

let (simpResult, _stats) ← simp hdefTy simpCtx (simprocs := #[])
let hdefVal ← simpResult.mkCast hdefVal
let hdefTy ← inferType hdefVal

Expand Down
10 changes: 5 additions & 5 deletions Proofs/Experiments/MemoryAliasing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ theorem mem_automation_test_4
(write_mem_bytes 48 src_addr val s0)) =
val.extractLsBytes 1 10 := by
simp only [memory_rules]
simp_mem -- TODO: repeat on change.
simp_mem
congr 1
bv_omega' -- TODO: address normalization.

Expand Down Expand Up @@ -399,10 +399,8 @@ end PairwiseSeparate

namespace MemOptions

set_option trace.simp_mem true
set_option trace.simp_mem.info true


set_option trace.simp_mem true in
set_option trace.simp_mem.info true in
/--
error: unsolved goals
⊢ False
Expand All @@ -420,6 +418,8 @@ info: ⊢ False
simp_mem (config := { failIfUnchanged := false })
trace_state

set_option trace.simp_mem true in
set_option trace.simp_mem.info true in
/--
error: ❌️ simp_mem failed to make any progress.
---
Expand Down