summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Collapse)Author
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
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 02:46:14 +0000