Goal sequents #1689
Merged
Goal sequents #1689
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
|
CI failure looks like out-of-memory again |
robdockins
force-pushed
the
rwd/goal-sequents
branch
2 times, most recently
from
f328f68 to
dfdcbf7
Compare
|
CI problem on AWS-LC still appears to be out-of-memory. Lazy LLVM loading seems like it doesn't help for this workload. Perhaps #1697 will make a difference. |
robdockins
force-pushed
the
rwd/goal-sequents
branch
2 times, most recently
from
d3597dc to
c8760a0
Compare
robdockins
force-pushed
the
rwd/goal-sequents
branch
from
c8760a0 to
4a60360
Compare
robdockins
force-pushed
the
rwd/goal-sequents
branch
2 times, most recently
from
3dbcd8f to
3b14346
Compare
to use sequents.
joint count of the size of terms appearing in sequents.
proper pretty-printing support for sequents.
Perhaps this will plug some space leaks.
These prevent the rewriter from continuting to rewrite in the result.
Notably, add the ability to perform rewrites using local sequent assumptions.
This is useful to save on resident memory for verification conditions, which are never directly used to prove later theorems.
This avoids entering the statements of verification conditions into the "theorem database", and tracks data about their proofs separately. This is primarily to avoid retaining the terms representing these conditions throughout the run of a proof, as the VCs can get quite large, and are never directly used in the proof of another theorem.
to the old `goal_assume` tactic. It was never much used, and the use-cases it aimed to serve are better handled by sequents.
Reimplement `goal_insert` based on cut. This tactic was removed in an earlier phase, but here we can add it back fairly easily. Add the ability to apply local hypotheses in addition to theorems, via `goal_apply_hyp`. Add the ability to specialize a local hypothesis via `goal_specialize_hyp`. This is especially useful for specializing an inductive hypothesis in the (unfortunatly common) case where solvers cannot figure out the correct instantiations. The `split_goal` tactic now works on hypotheses that represent SAWCore implications (i.e., nondependent functions between Props), which provides the standard modus ponens rule.
robdockins
force-pushed
the
rwd/goal-sequents
branch
from
3b14346 to
b66cca9
Compare
induction principle for natural numbers, and for bitvectors. This adds no additional axioms over those alreay present in the system.
by induction on bitvector values.
robdockins
commented
Aug 23, 2022
robdockins
commented
Aug 23, 2022
robdockins
commented
Aug 23, 2022
RyanGlScott
reviewed
Aug 24, 2022
RyanGlScott
reviewed
Aug 24, 2022
proof would force a sequent normalization. This was to account for the case where the "enable_sequent_goals" option was set, which requires a little additional work to match up the statement of a lemma with the initial sequent that was proved. However, in some cases, this normalization step can be quite expensive, so now we only insert this additional normalization step when the sequent goals option is active.
Minor other docuemenation tweaks.
Co-authored-by: Ryan Scott <[email protected]>
Also! Fix a bug in the tactic for applying local hypotheses. Previously it would only generate a single subgoal, even if the applied hypotheses generated more than that. This would lead to prematurely-finished proofs and evidence checking failures.
in the external API of the Proof module. We still need to correct the terminology within the module itself.
right-hand side of a sequent, reserving the term "goal" for an entire sequent.
robdockins
force-pushed
the
rwd/goal-sequents
branch
from
c8eb404 to
58c477d
Compare
|
With the exception of opening tickets regarding some of the things mentioned above, I think this PR is ready to go. |
RyanGlScott
approved these changes
Aug 26, 2022
robdockins
added
the
PR: ready to merge
This was referenced Aug 26, 2022
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.
CF #1685