summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_values.v
AgeCommit message (Collapse)Author
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.
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-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-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-02Coq: add properly checked subrange update, reduce importsBrian Campbell
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-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
2019-06-06Coq: tweak bool to Z to use less memoryBrian Campbell
2019-06-05Coq: exploit arithmetic solver for some mixed integer/bool problems.Brian Campbell
2019-06-05Coq: generalize proof terms before main solverBrian Campbell
Ensures that dependencies in proofs don't affect rewriting.
2019-06-04Coq: more constraint solvingBrian Campbell
- make the exists, iff solver handle more cases - avoid exposing omega to goals with local definitions involving proofs
2019-06-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-29Coq: more solver improvementsBrian Campbell
- don't clear boolean local definitions - we need those now - some boolean disjunction fixes
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-28Coq: more constraint solvingBrian Campbell
- add division lemma - deal with some awkward \/ constraints from asl_parser - try simple integer comparison proofs before omega (which can blow up on trivial properties in large contexts)
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-23Coq: solve some division constraintsBrian Campbell
2019-05-22Coq: tweak disjunctions tactic with subst to support more constraintsBrian Campbell
2019-05-21Coq: remove premature unfolding of local definitionsBrian Campbell
2019-05-20Coq: fix property extraction bug, solve some constraints involving setsBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
That is, undefined_bitvector, undefined_unit, internal_pick.
2019-05-15Coq: constraint solving for aarch64Brian Campbell
Also split out main solver tactic to make debugging a little easier.
2019-04-19Coq: more robust handling of unknown constraintsBrian Campbell
2019-04-16Coq: make bools_of_int (and hence get_slice_int) compute wellBrian Campbell
2019-04-16Coq: add specialised shiftsBrian Campbell
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
NB: requires minor changes in the models
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-03-27Coq: add a little knowledge about ZEuclid.divBrian Campbell
2019-03-27Coq: replace firstorder with less expensive tacticsBrian Campbell
2019-03-19Coq: more work on testsBrian Campbell
- skip a few more that aren't supported yet - produce better debugging information (in particular, in the right order) - avoid some autocasts that aren't supported yet and are usually unnecessary - Handle more constraints like `8 * n = 8 * ?Goal`
2019-03-15Coq: some progress on the test suiteBrian Campbell
Rewrite <> true/false in goals. Correct implicits in record and variant types. Use expanded valspecs from the type checker in axioms. Allow list notations in type definitions. Skip some not-yet-supported tests.
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
Fixes bad precedence issues, removes an out-of-date special case that's not necessary, and solves more goals.
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 07:34:54 +0000