summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Collapse)Author
2020-09-30Tweak Coq proof to avoid incompatibility with IrisBrian Campbell
(in the previous proof script the intuition tactic found a strange proof involving a type-level dependent pair that imposed an unnecessary universe constraint, this doesn't)
2020-09-12Merge some of the gitignore filesColumbus240
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq. This commit removes /lib/coq/.gitignore and moves all ignore-statements to /.gitignore . This should simplify the maintenance of gitignore files. The situation with /test/mono/.gitignore is analogous.
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
Also remove omega workaround that lia doesn't need.
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
Helps with Coq 8.11. Also fix BBVDIR default in test script.
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
- 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
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
Also be more careful to avoid pattern bindings with identifiers to avoid parsing clashes, eg `let 'bytes := ...` which is confused with the notation for binary literals.
2020-01-17Coq: add hex_strBrian Campbell
Now used in RISC-V model.
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
- add liftRS support to tactics - define uint and sint in terms of functions without proof terms - eq_vec correctness - lemma that rounding up integers using reals is the obvious integer calculation - another proof irrelevance tactic - try lemmas in the sail hintdb both before and after goal processing
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
- break up goals more in unbool - remove intuition from guess_ex_solver because it can be too expensive - flip goals around because the side that evars appears on has changed - generalise the and/or tactics - make a couple of tactics more specific/robust
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
Includes removing an explicit use of a lemma generated by abstract, which was causing problems with different versions of Coq because the names change.
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
Mostly from making the aarch64 model compile again - switch order some arithmetic lemmas - move list membership rewrites alongside other comparisons to enable more rewriting - copy hypotheses used in other types/definitions so that they can be rewritten - lift boolean existentials out of implications in hypotheses so they can be used as witnesses without proving the condition - add negation to solve_bool_with_Z - add some new bool solving for goals from and_boolMP/or_boolMP
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
- 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
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-13Coq: more proof supportBrian Campbell
- add state versions of foreach combinators - support dependent sumbool pattern matching (i.e., those where the property is actually used) - add rewriting congruence rules, state monad lifting rules, and invariant proof rules for these
2019-11-04Coq: compatiblity with 8.10 as well as 8.9Brian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
- 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
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
It only produces them when necessary (because some types do not have decidable equality due to embedded proofs). Also add trivial instance for the unit type.
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
- in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates)
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
In particular, shift state lambdas outside of if/match/let which avoids unnecessary abstraction/applications. Add more rules to the tactic.
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
Also tweak the informative and/or boolean definitions so that they use the same proofs in both monads.
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Coq library work for proofs:Brian Campbell
* rename state fields to avoid clash with regstate type * use rewriting to automate some proofs
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
Add count_leading_zeros, and correct a precedence error in min/max.
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
Mostly in the Coq backend, plus a few testcases that use bitvector builtins on poly-vectors (which works on some backends, but not Coq). Also handle some additional list inclusion proofs in Coq.
2019-07-31Coq: Update barrier definitionsBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
Loops measures are now abstracted over the variables so that they can be used in proofs. Add total Hoare logic rules for until.
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
Move the tactic forward so that preprocessing can't try silly things, simpl to get rid of embedded proofs.
2019-06-20Coq: avoid some unnecessary reduction in the constraint solverBrian Campbell
2019-06-13Coq: add eq_bit built-inBrian Campbell
2019-06-11Coq: add concatenation operator for polymorphic vectorsBrian Campbell
2019-06-06Coq: more aggressive rewriting before solvingBrian Campbell
Solves some ARM model constraints much more quickly
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:53:29 +0000