| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-15 | Get RISC-V on Coq into reasonable state to show | Brian 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-14 | Coq: attempt a quick proof before an indepth one | Brian Campbell | |
| 2018-08-13 | Coq: drop irrelevant definitions before constraint solving | Brian Campbell | |
| (which were slowing down RISCV unacceptably because dealing with the xlen max/min values is surprisingly expensive) | |||
| 2018-08-09 | Coq: a bit more handling of unknown constraints | Brian Campbell | |
| 2018-08-03 | Coq: use a dummy constraint when the real one is unknown | Brian Campbell | |
| Not really what we want, but a useful placeholder because of the widespread use of ex_int. | |||
| 2018-08-03 | Coq: generalise dependent pair handling a little | Brian Campbell | |
| 1. for monadic values (not in a terribly useful way, though) 2. for more types | |||
| 2018-08-02 | Coq: limit eauto to ensure termination in reasonable time | Brian Campbell | |
| 2018-08-02 | Fill in more Coq builtins for aarch64 | Brian Campbell | |
| 2018-08-01 | Coq: implicit range conversions for function arguments, debug tracing | Brian Campbell | |
| The new option -dcoq_debug_on takes a list of functions to output tracing on. | |||
| 2018-07-18 | Coq: constraint solving improvements | Brian 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-17 | Coq: integer shifts | Brian Campbell | |
| 2018-07-17 | Coq: add printing stubs | Brian Campbell | |
| 2018-07-17 | Coq: handle E_constraint properly | Brian Campbell | |
| Adds missing constraints for aarch64 | |||
| 2018-07-16 | Coq: add support for more complex atom types | Brian Campbell | |
| As a result, add proof to pow2. | |||
| 2018-07-12 | Coq: handle all bool conjunctions/disjunctions | Brian Campbell | |
| 2018-07-12 | Coq: remove unnecessary constraint on foreach loops | Brian Campbell | |
| 2018-07-09 | Bits for bits of aarch64 in coq | Brian Campbell | |
| 2018-07-07 | Coq: precise generic vectors | Brian Campbell | |
| (probably still some pattern matching to do, but I don't think the models use that) | |||
| 2018-07-07 | Coq: eq_range should take proofs | Brian Campbell | |
| 2018-07-06 | Coq: use List.In predicates in constraint solving; make other bits robust | Brian Campbell | |
| 2018-07-05 | Coq: get index_list right | Brian Campbell | |
| 2018-07-02 | Coq: add some string functions | Brian Campbell | |
| 2018-07-02 | Coq: replace simpl in a tactic with a more precise "change" | Brian Campbell | |
| Prevents partial unfolding of Z.pow. | |||
| 2018-06-25 | Coq: add typeclass based comparison, and instantiate for enums | Brian Campbell | |
| 2018-06-22 | Add coq builtins for MIPS | Brian Campbell | |
| 2018-06-22 | Coq: library updates, esp extending bitvector multiplies, Undefined | Brian Campbell | |
| 2018-06-22 | Coq: project away range types in comparisons | Brian Campbell | |
| 2018-06-20 | Coq: reverse_endianness | Brian Campbell | |
| 2018-06-20 | Coq: Tidy up libraries, export String | Brian Campbell | |
| 2018-06-19 | Coq: library name update (as we did for Lem) | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |