summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_values.v
AgeCommit message (Collapse)Author
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
NB: requires minor changes in the models
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
- 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-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: 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-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
(which allows us to avoid a Coq bug where the proof isn't recorded correctly)
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-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
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-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-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.
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
Also required some solver fixes: - make sure that ArithFacts are always cleared to avoid loops - extract_properties should do the goal first because it might add extra work to do in the hypotheses - unfolding should come before extract_properties
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
constructed when a function call, cast, or binder demands them, removing some ambiguous corner cases. Also - Don't simplify nexps before printing (note that we usually end up needing a (8 * x) / 8 lemma as a result) - More extraction of properties in the goal - Splitting of conditionals/matches in goals (which can occur more often because of the new positions of build_ex in definitions) - Try simple solving first to improve speed / reduce proof sizes / help fill in metavariables (because manipulating the goal can interfere with instantiating them) - Update RISC-V patch
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
- Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
(which were slowing down RISCV unacceptably because dealing with the xlen max/min values is surprisingly expensive)
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
2018-08-03Coq: use a dummy constraint when the real one is unknownBrian Campbell
Not really what we want, but a useful placeholder because of the widespread use of ex_int.
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
1. for monadic values (not in a terribly useful way, though) 2. for more types
2018-08-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
The new option -dcoq_debug_on takes a list of functions to output tracing on.
2018-07-18Coq: constraint solving improvementsBrian Campbell
Use eauto so that user-added hints are more flexible, example with Replicate in aarch64, dropped zbool to prevent slow proof searches (and preprocessing deals with boolean comparisons now). Report failed constraints after preprocessing; Separate preprocessing tactic out.
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
Adds missing constraints for aarch64
2018-07-16Coq: add support for more complex atom typesBrian Campbell
As a result, add proof to pow2.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:10:36 +0000