| Age | Commit message (Collapse) | Author |
|---|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
|
|
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
|
|
|
|
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
|
|
|
|
That is, undefined_bitvector, undefined_unit, internal_pick.
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
|
|
Now generates something vaguely sensible for RISC-V, although the solver
needs a little work.
Adds type annotations around effectful, rich and/or expressions.
|
|
Make internal_plet produce annotations (with code to replace unusable
type variables)
Add mappings for bool kids at bindings
Add version of and_bool that proves a property
|
|
This introduces some simplification of informative booleans, but tries
too hard to eliminate all of the existentials resulting in difficulties
in and/or trees.
|
|
|
|
It now includes updating the effects so that morally pure recursive
functions can be turned into this impure termination-by-assertion form.
|
|
This only applies to recursive functions and uses the termination measure
merely as a limit to the recursive call depth, rather than proving the
measure correct.
|
|
|
|
|
|
|
|
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
|
|
1. for monadic values (not in a terribly useful way, though)
2. for more types
|
|
|
|
|
|
|
|
|
