summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Collapse)Author
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-23Coq: define the names from the Sail real libraryBrian 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: add signed bitvector to integer function that doesn't need >0 constraintBrian 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-25Update coq read_mem/write_mem.Prashanth Mundkur
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: set_slice typoBrian Campbell
2019-04-16Coq: add specialised shiftsBrian Campbell
2019-04-15Basic loop termination measures for CoqBrian Campbell
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).
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-05Coq: termination measures for mutually recursive functionsBrian Campbell
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 test workBrian Campbell
- add dummy print_bits function - support int(1) like types in axioms
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
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
Just enough for RISC-V to go through
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions.
2019-02-28Coq: more for informative booleansBrian Campbell
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
2019-02-28Coq: some work on bool simplificationBrian Campbell
This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees.
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-01Coq: update instr_kinds from LemBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-27Coq: make solver try hints before stripping away existentialsBrian Campbell
(which allows us to avoid a Coq bug where the proof isn't recorded correctly)
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
Also output termination measures in Sail printer
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:44:33 +0000