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.

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

Conversation

bollu
Copy link
Collaborator

@bollu bollu commented Aug 27, 2024

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 the MemoryRegion abstraction in the first place.

@bollu bollu marked this pull request as ready for review August 27, 2024 19:47
@bollu bollu requested a review from shigoel as a code owner August 27, 2024 19:47
@shigoel
Copy link
Collaborator

shigoel commented Aug 28, 2024

@bollu Conflicts here.

@shigoel shigoel marked this pull request as draft September 3, 2024 16:17
@bollu bollu marked this pull request as ready for review September 3, 2024 21:53
@bollu
Copy link
Collaborator Author

bollu commented Sep 3, 2024

@shigoel conflicts addressed!

@shigoel
Copy link
Collaborator

shigoel commented Sep 3, 2024

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 pairwise, and then we'll go from there?

@bollu
Copy link
Collaborator Author

bollu commented Sep 4, 2024

@shigoel all comments addressed.

@shigoel
Copy link
Collaborator

shigoel commented Sep 4, 2024

@bollu I see that a couple comments weren't addressed. Tagged you there.

@bollu
Copy link
Collaborator Author

bollu commented Sep 4, 2024

@shigoel All comments (hopefully) addressed.

Comment on lines +391 to +403
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)
}
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.

@bollu
Copy link
Collaborator Author

bollu commented Sep 5, 2024

@shigoel happy to have this merged, as I prefer keeping the current around to build the SimpContext around.

@shigoel shigoel merged commit c6c48a0 into main Sep 6, 2024
4 checks passed
@shigoel shigoel deleted the mem-pairwise branch September 11, 2024 17:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants