summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_values.v
AgeCommit message (Expand)Author
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
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
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
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
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
2019-06-04Coq: more constraint solvingBrian Campbell
2019-06-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-29Coq: more solver improvementsBrian Campbell
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-28Coq: more constraint solvingBrian Campbell
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
2019-05-15Coq: constraint solving for aarch64Brian Campbell
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
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
2019-03-15Coq: some progress on the test suiteBrian Campbell
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
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:20:08 +0000