SyGuS, find SMT array write of a fixed size #2037
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Ryan Scott <rscott@galois.com>
This bumps: * The `crucible` submodule to bring in the changes from GaloisInc/crucible#1178 * The `what4` submodule to bring in the changes from GaloisInc/what4#256
SAW creates a variety of different ExprBuilders in the course of a typical SAW script, but we were only applying the pushMuxOps option to some of them. This patch makes the treatment a bit more comprehensive. Unfortunately, doing so requires a rather uncomfortable amount of extra plumbing in `SAWScript.Proof`, but I'm not sure how to do better without refactoring all of `SAWScript.Proof` to use `TopLevel` instead of `IO` (and it's unclear if that is desirable).
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 23, 2024
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 23, 2024
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 23, 2024
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 23, 2024
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 24, 2024
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 24, 2024
This proves unbounded AES-GCM functions, building on top of the cryptol-specs work in GaloisInc/cryptol-specs#72 and the saw-script work in GaloisInc/saw-script#2037. This requires a newer version of SAW to work than what aws-lc-verification's CI currently uses, so I isolated these proofs into their own SAW scripts, Cryptol specs, shell scripts, Docker image, and CI action. Moreover, some of the AES-GCM proofs use Z3's Constrained Horn Clause (CHC) feature, which is buggy on Z3-4.8.8. aws-lc-verification's other CI jobs are currently using Z3-4.8.8, so I specifically chose a newer version (Z3-4.8.14) for the new, AES-GCM–specific CI job. Co-authored-by: Robert Dockins <rdockins@galois.com> Co-authored-by: Samuel Breese <samuel@chame.co> Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
RyanGlScott
added a commit
to RyanGlScott/aws-lc-verification
that referenced
this pull request
Apr 24, 2024
This proves unbounded AES-GCM functions, building on top of the cryptol-specs work in GaloisInc/cryptol-specs#72 and the saw-script work in GaloisInc/saw-script#2037. This requires a newer version of SAW to work than what aws-lc-verification's CI currently uses, so I isolated these proofs into their own SAW scripts, Cryptol specs, shell scripts, Docker image, and CI action. Moreover, some of the AES-GCM proofs use Z3's Constrained Horn Clause (CHC) feature, which is buggy on Z3-4.8.8. aws-lc-verification's other CI jobs are currently using Z3-4.8.8, so I specifically chose a newer version (Z3-4.8.14) for the new, AES-GCM–specific CI job. Co-authored-by: Robert Dockins <rdockins@galois.com> Co-authored-by: Samuel Breese <samuel@chame.co> Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
kquick
approved these changes
May 14, 2024
| IO (C.ExecutionFeature p sym ext rtp, IORef (Crucible.LLVM.FixpointCHC.ExecutionFeatureContext sym 64 ext)) | ||
|
|
||
| setupSimpleLoopFixpointCHCFeature sym sc sawst cfg mvar func = do | ||
| let ?ptrWidth = knownNat @64 |
There was a problem hiding this comment.
I'm not very comfortable with hard-coding this here (which could deviate from similar settings in src/SAWScript/X86Spec.hs), but there's nothing here that looks immediately available for inheriting/determining this value.
There was a problem hiding this comment.
Indeed. While uncomfortable, this is an assumption which is currently baked into several parts of the code, not just SAW. See GaloisInc/crucible#1028 for where this restriction ultimately arises in crucible-llvm. It would be nice to generalize this code to work over any pointer width, but it would likely require addressing GaloisInc/crucible#1028 first.
This was referenced May 15, 2024
Closed
Closed
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is an amalgamation of:
This bumps:
cruciblesubmodule to bring in the changes from SyGuS, match concrete size array crucible#1178what4submodule to bring in the changes from Guard mux-pushing simplifications behind option what4#256