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

Jump to bottom

Use itree SpecM monad instead of CompM in Heapster #1778

Merged
merged 93 commits into from
Dec 10, 2022
Merged

Use itree SpecM monad instead of CompM in Heapster #1778

merged 93 commits into from
Dec 10, 2022

Conversation

m-yac
Copy link
Contributor

@m-yac m-yac commented Dec 9, 2022

This PR updates the Heapster translation of saw-core to use the SpecM monad and its proof automation from GaloisInc/entree-specs, which is based on interaction trees (itrees).

Note that not all of the heapster-saw/examples have been updated to use the new translation and/or the new automation.

  • Most rust examples do not current work with the new translation, so any individual calls to hepaster the don't work in these files are commented out
  • All _proofs.v files but mbox_proofs.v and linked_list_proofs.v have not been updated to use the new automation, so are commented out in the _CoqProject
  • MRSolver has yet to be updated to use the new translation, so all _mr_solver.saw files are commented out in the Makefile

lag47 and others added 30 commits July 12, 2022 11:26
@lag47
began defining SpecM in Prelude.sawcore
661c442
@lag47
added some SpecM definitions
f852a35
@lag47
wrote new interface for SpecM
cba7658
@lag47
fixed haddock syntax errors
7f1b785
@lag47
further refactored SpecM
b501146
partially rewrote saw translation
6e783f7
new draft of multiFixS function signature
92fb1f9
@lag47
refactored MultiFixSBodiesS
1e8e7b3
@lag47
implementing SAW functions
211fac9
@lag47
updated documentation
bed9ee8
Merge branch 'master' into heapster-itree
f0a4895
updated the SAW core prelude with the new versions of the SpecM opera…
0e5bd0e 
…tions
Added VoidEvRetType for defining the evRetType of a Void to the SAW c…
be309ca 
…ore prelude
renamed CallS to callS
8b6a93c
added the more general identOpenTerm
f195a8f
partially finished changing the translation to generate SpecM computa…
4ecf85d 
…tions instead of CompM
almost done changing the translation to generate SpecM computations i…
3eea089 
…nstead of CompM
got the new translation to SpecM to compile, yay!
b5eb9f1
fixed some small bugs in the SAW core translation
c434a4c
changed more of the CompM operations in the translation to use the co…
a074cbc 
…rresponding SpecM operations instead
fixed the type of errorS
3d90681
added translations for the SpecM operations
fbbc4c3
updated sawLet to use sort 1 instead of sort 0
4e0c3f9
whoops, updated the SAW translation to use retS instead of returnS
0b2d854
fixed up references to EnTree specs
c5d8962
Merge branch 'master' into heapster-itree
9a596bb
changed the SpecM monad to be a sort 0 instead of a sort 1
f355421
Merge branch 'master' into heapster-itree
bebfce2
removed the old LetRecType1 type, and updated LetRecType to reference…
48f53a5 
… the version from the SpecM module
changed some uses of errorM to errorS; added a workaround for issue #…
13d26b9 
…1748; changed uses of LetRecTypes to use List1 LetRecType, to be consistent with the SpecM module
RyanGlScott and others added 14 commits November 29, 2022 11:32
@RyanGlScott
mbox_split_at_spec_ref is proven!
aba8237
@RyanGlScott
More progress on mbox_copy_chain
4759cd2
@m-yac
use eithers instead of either, update proofs
ab0e39c
added heapster_set_event_type command, along with the io example to u…
26f44ac 
…se it
Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into…
0e9eed5 
… heapster-itree
@RyanGlScott
Complete proof of mbox_copy_chain
290db7e
@RyanGlScott
mbox_detach_from_end proofs
e4a40b3
@m-yac
prove mbox_randomize_spec_ref
fac87aa
small tweaks to the hello world example
ac18311
Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into…
1a077f4 
… heapster-itree
@RyanGlScott
translateCurryLocalPermImpl: Don't force the use of an EmptyFunStack
c862d47 
This caused typechecking errors in practice in some downstream code.
@m-yac
clean up + update mbox_proofs, linked_list_proofs
c2385cc
@m-yac
get make passing (rust typechecking fails)
2f1d08b
@m-yac
Merge branch 'master' into heapster-itree
bbac0b2
@m-yac m-yac added the subsystem: heapster Issues specifically related to memory verification using Heapster label Dec 9, 2022
RyanGlScott
RyanGlScott reviewed Dec 9, 2022
View reviewed changes
heapster-saw/examples/_CoqProject Show resolved Hide resolved
heapster-saw/examples/Makefile Outdated Show resolved Hide resolved
heapster-saw/src/Verifier/SAW/Heapster/HintExtract.hs Outdated Show resolved Hide resolved
saw-core/src/Verifier/SAW/Module.hs Outdated Show resolved Hide resolved
RyanGlScott and others added 3 commits December 9, 2022 10:07
@RyanGlScott
Merge branch 'master' into heapster-itree
eabdf2d
@RyanGlScott
Install entree-specs as a Coq dependency
d2d9f01 
This updates the CI to build a particular `entree-specs` commit before building
the Coq support libraries. This also updates the instructions in the
`saw-core-coq` `README` accordingly.

Note that this requires limiting the Coq support window to 8.15 for now, as
`entree-specs` requires 8.15 as the minimum. In particular, `entree-specs`
does not yet support 8.16 (see GaloisInc/entree-specs#1), so we now require
Coq 8.15 exactly.
@m-yac
update proofs with latest changes to saw-core-coq
b91d94e
This was referenced Dec 9, 2022
Open
Open
Open
eddywestbrook
eddywestbrook approved these changes Dec 9, 2022
View reviewed changes
Copy link
Contributor

@eddywestbrook eddywestbrook left a comment

Choose a reason for hiding this comment

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

LGTM!

@m-yac m-yac added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Dec 9, 2022
@RyanGlScott
Copy link
Contributor

The blst job appears to be failing because of some odd out-of-space-related issues with Docker. Given that this PR only changes Heapster (and shouldn't affect anything else in SAW that would impact the BLST proofs), I'm going to go ahead and merge this.

@RyanGlScott RyanGlScott merged commit 8f72532 into master Dec 10, 2022
@RyanGlScott RyanGlScott deleted the heapster-itree branch December 10, 2022 13:20
@RyanGlScott RyanGlScott mentioned this pull request Feb 14, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@RyanGlScott RyanGlScott RyanGlScott left review comments

@eddywestbrook eddywestbrook eddywestbrook approved these changes

Assignees
No one assigned
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@m-yac @RyanGlScott @eddywestbrook @lag47