summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_values.v
AgeCommit message (Expand)Author
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
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: some work on bool simplificationBrian Campbell
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2018-12-27Coq: make solver try hints before stripping away existentialsBrian 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
2018-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-09-19Coq: more fixes for AArch64Brian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian Campbell
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-30Coq: correct endianness reversal bugBrian Campbell
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:40:54 +0000