cvlr-spec: basic primitives for specifications #37
Conversation
This file contains hidden or 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
1arie1
force-pushed
the
cvlr-spec-rewrite
branch
from
e08c901 to
7976000
Compare
also includes various cleanups in cvlr-spec and exposure of cvlr-spec in cvlr.
Converts a rust function int a CvlrBoolExpr predicate
cvlr_assert series of macros introduce local variables to avoid evaulating their arguments multiple times. The variable names should be unique to avoid shadowing. We are using `__cvlr_` prefix since it is unique enough.
We have cvlr_spec crate that is re-exported in cvlr as cvlr::spec We expect most users to use cvlr rather than sub-crates individually.
re-exporting as cvlr::predicate
Useful for converting state predicates to post-conditions
An alternative design in which associated types are used to represent that context over which a BoolExpr operates. This design allow programatic access to the context form the BoolExpr. Also replace StatePair with a tuple of contexts.
Currently, only evaluation over two states (or one state) is supported. Two-state evaluation is used in specification to evaluate over pre- and post-state, together. A predicate that is single state is evaluated on the first state of the two-state pair. For that reason, in CvlrSpec, post-state is given first.
```
cvlr_assert_that!{if guard { flag } else { true }}
```
expands to
```
if guard {
::cvlr_asserts::cvlr_assert_checked(flag);
} else {
()
};
```
and `cvlr_assert_that!(true)` expands to `()`
Generated `eval` function exits as soon as one of the expressions is false
CvlrPredicate is a marker trait that all predicates must implement. A CvlrFormula is either a constnat CvlrTrue, a predicate, or a boolean combination of CvlrFormulas.
The case of if-without-else is broken for evaluation. The current eager evaluation scheme is difficult to implement in this case. Let binidngs are also broken because they are collected now separately from the expression statements. Fixing this requires a more serious overhaul.
This is on the way of supporting if-without-else, but in the current variant it still does not work as expected.
Using cvlr::predicate attributed local functions instead of cvlr_def_predicate macro.
Add form 2 of cvlr_lemma macro that allows for pre-built predicates. This form is useful when you already have predicates defined or want to use composed expressions. update tests and documentation to match
1arie1
force-pushed
the
cvlr-spec-rewrite
branch
from
7976000 to
9488476
Compare
1arie1
force-pushed
the
cvlr-spec-rewrite
branch
from
d9d59a6 to
42cb3da
Compare
assert macros log assertion and values. These are enclosed in a scope. The bug was not closing the scope correctly using log_scope_end.
Lemmas are intendend to be used in multiple contexts. Make them public by default. We might add explicit visibility modifier later if needed.
Add support for two-state predicates in cvlr_predicate macro. Two-state predicates are predicates that take two arguments: - The first argument is the post-state context - The second argument is the pre-state context The macro generates a struct that implements CvlrFormula and CvlrPredicate.
CvlrLemma::apply() was essentially same as verify()
Add cvlr_and_pif macro to cvlr-spec. cvlr_and_pif is a macro that composes a list of predicates using cvlr_and.
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.
Introduces basic primitives to write function specification (pre- and post-conditions), invariants, and general Boolean expressions. Expressions can be evaluated, assumed, or asserted. Introduces macros to automatically generate rules from specifications.