summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Collapse)Author
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
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
It now includes updating the effects so that morally pure recursive functions can be turned into this impure termination-by-assertion form.
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
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.
2018-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-20Minor coq updatesBrian Campbell
2018-10-22Update Coq patch for RISC-V, add string_take to Coq libraryBrian Campbell
2018-09-19Coq: track changes elsewhereBrian Campbell
- more hex_bits functions, add decimal_string_of_bits - extra tuple unfolding in constructors - note that variables can be redundant wildcard clauses - update RISC-V patch
2018-09-19Coq: more fixes for AArch64Brian Campbell
- implement set_slice and set_slice_int - lemmas for more constraints - make real sqrt visible - unfolding list membership needs andb and orb to be handled first
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
- hints for dotp - handle exists separately when trying eauto to keep search depth low - more uniform existential handling (i.e., we now handle all existentials in the way we used to only handle existentials around atoms)
2018-09-17Coq: make generic_neq work on realBrian Campbell
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian Campbell
The omega tactic doesn't like them
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-06Coq: more string handlingBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
otherwise some other parts don't work properly. Also update RISC-V patch.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:45:23 +0000