saw-core-coq: Rudimentary lia support for bitvectors
#1776
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
RyanGlScott
added
the
subsystem: saw-core-coq
RyanGlScott
commented
Dec 7, 2022
Comment on lines
+69
to
+72
| Lemma bvToInt_inj w a b : | ||
| bvToInt w a = bvToInt w b -> | ||
| a = b. | ||
| Proof. holds_for_bits_up_to_3. Qed. |
There was a problem hiding this comment.
This adds a handful of bitvector-related proofs that are proved via holds_for_bits_up_to_3. I'm not sure if this is the best home for them, or if they would be better placed alongside the existing holds_for_bits_up_to_3 proofs in SAWCoreBitvectors.v.
RyanGlScott
force-pushed
the
saw-core-coq/lia-support-take-two
branch
2 times, most recently
from
ceb03e3 to
8985af1
Compare
eddywestbrook
approved these changes
Dec 8, 2022
RyanGlScott
added
the
PR: ready to merge
We were previously defining the following in the Coq support library: ```coq Definition true := Datatypes.true. Definition false := Datatypes.false. ``` This is rather silly, as we could just as well use `Datatypes.true` and `Datatypes.false` directly. What's more, redefining `true` causes issues in a subsequent commit that adds `lia` support for `bitvector`s, so it is especially important to remove `true` for that reason. This removes the redefined versions of `true` and `false`, and it also tweaks `SpecialTreatment.hs` to translate SAWCore's `True`/`False` into `Datatypes.true`/`Datatypes.false`. Although this is technically a breaking change, it is a change that is very unlikely to break existing proofs (unless your proofs directly mention `SAWCoreScaffolding.true` or `SAWCoreScaffolding.false`). Co-authored-by: Eddy Westbrook <[email protected]>
For historical reasons, the Coq support library has several wrapper functions like the following: ```coq Definition Bool := bool. ``` These are extremely silly, however, given that `bool` is already widely used in the Coq world, and providing our own version of `bool` with different capitalization causes a proliferation of names that refer to the same thing. It would be nice to rip out these wrapper functions, but unfortunately, doing so would induce a fair bit of breakage in downstream code. For now, we simply record the fact that these functions are deprecated, and we will revisit whether we want to remove them at a later date.
This adds `SAWCoreBitvectorsZifyU64.v`, a file containing all of the necessary `Zify`-related instances for `bitvector 64` values needed to allow solving a large class of `bitvector`-related theorems using Coq's `lia` tactic. This also includes a small set of examples to ensure that `lia` works as expected. Although this is far from complete (see the documentation near the top of the file for a list of limitations), it should be enough to handle the common use case of `bitvector 64`, which is better than nothing.
Changed the Coq translator to directly translate a number of constructs to their corresponding Coq constructs, rather than having additional named definitions in SAWCoreScaffolding.v for those constructs; these included the Bool, Eq, String, and Nat types, along with their constructors, the Boolean operations and, or, xor, and not, the fst and snd operators, and the id function. Co-authored-by: Eddy Westbrook <[email protected]>
RyanGlScott
force-pushed
the
saw-core-coq/lia-support-take-two
branch
from
8985af1 to
44e0a4f
Compare
These cause issues with the automation due to confusion with the standard Coq functions of the same name. Trying to make both versions of each function coexist is a maintenance nightmare, so let's just remove SAWCoreScaffolding's versions.
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 adds
SAWCoreBitvectorsZifyU64.v, a file containing all of the necessaryZify-related instances forbitvector 64values needed to allow solving a large class ofbitvector-related theorems using Coq'sliatactic. This also includes a small set of examples to ensure thatliaworks as expected. Although this is far from complete (see the documentation near the top of the file for a list of limitations), it should be enough to handle the common use case ofbitvector 64, which is better than nothing.