summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Collapse)Author
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: more strings for RISC-VBrian 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-10Coq: add some of string libraryBrian Campbell
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.
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
(probably still some pattern matching to do, but I don't think the models use that)
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-05Coq: get index_list rightBrian Campbell
2018-07-02Coq: add some string functionsBrian Campbell
2018-07-02Coq: replace simpl in a tactic with a more precise "change"Brian Campbell
Prevents partial unfolding of Z.pow.
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas.
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-22Coq: project away range types in comparisonsBrian Campbell
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: a few more opsBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
(necessary for backends where they're different) Coq uint/sint and related fixes
2018-06-18Coq: update prompt monad wrt LemBrian Campbell
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
(The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication).
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
- add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving
2018-06-08Coq: some very basic existential supportBrian Campbell
Only single variable in places, only packed at literals and variables, no unpacking
2018-05-25Coq: fill in some built-insBrian Campbell
vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:45:22 +0000