-
Notifications
You must be signed in to change notification settings - Fork 18
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.
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
Conversation
@bollu Conflicts here. |
@shigoel conflicts addressed! |
Left some comments, looks good in general. We need more tests for the new pairwise construct (in a PR in the very near future is okay!) -- let's start with changing theorems in the SHA512 example to use |
Co-authored-by: Shilpi Goel <shigoel@gmail.com>
@shigoel all comments addressed. |
@bollu I see that a couple comments weren't addressed. Tagged you there. |
@shigoel All comments (hopefully) addressed. |
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) | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
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).
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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. 😉
There was a problem hiding this comment.
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.
@shigoel happy to have this merged, as I prefer keeping the current around to build the |
This is stacked on top of #123 , since we want to state this, for a given
ms : List MemoryRegion
,ms.pairwise MemoryRegion.Separate
. This, of course, needs us to have theMemoryRegion
abstraction in the first place.