sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-09-21	Remove cheri and mips specs -- they now have their own repository.	Robert Norton

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-02	Coq mips: fix deprecation warning	Brian Campbell

2018-08-02	Coq: remove type removal holdover from Lem backend, add MIPS lemma	Brian Campbell

2018-07-23	Coq: faster MIPS extras without confusing message	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-03	Fill in a few Coq functions for CHERI from the MIPS prelude	Brian Campbell

2018-07-02	Coq modulus operation that fits the type	Brian Campbell

2018-06-22	Add current state of mips_extras.v	Brian Campbell