sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-12-20	RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ↵	Robert Norton
	and tests.
2018-11-20	Minor coq updates	Brian Campbell

2018-10-22	Coq: use function type more carefully in untupling	Brian Campbell
	And update the RISC-V patch accordingly.
2018-10-22	Update Coq patch for RISC-V, add string_take to Coq library	Brian Campbell

2018-10-01	Update Coq RISC-V patch now that the assembler is in good shape	Brian Campbell

2018-09-19	Coq: track changes elsewhere	Brian Campbell
	- more hex_bits functions, add decimal_string_of_bits - extra tuple unfolding in constructors - note that variables can be redundant wildcard clauses - update RISC-V patch
2018-09-12	Coq: update RISC-V patch	Brian Campbell

2018-09-06	Coq: fill in a few more RISC-V axioms	Brian Campbell

2018-09-06	Coq: fix up some barrier/memory definitions for RISC-V	Brian Campbell

2018-09-05	Coq: fill in trivial ranges in constraint solver	Brian Campbell

2018-09-04	Add a rewrite to minimise the number of functions marked as recursive	Brian Campbell
	Particularly useful when execute has been split up (e.g., on RISC-V). Only enabled on Coq for now.
2018-09-03	Coq: solver should split earlier	Brian Campbell
	otherwise some other parts don't work properly. Also update RISC-V patch.
2018-09-03	Coq: update RISC-V patch again	Brian Campbell

2018-09-03	Coq: rework generation of dependent pairs so that they are only	Brian 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-16	Add the type an expression was checked against to tannots, and use for Coq	Brian Campbell
	Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast.
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