sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-04-18	Add some lemmas about bitvectors	Thomas Bauereiss
	Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors.
2018-03-14	Make partiality more explicit in library functions of Lem shallow embedding	Thomas Bauereiss
	Some functions are partial, e.g. converting a bitvector to an integer, which might fail for the bit list representation due to undefined bits. Undefined cases can be handled in different ways: - call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the default so far), - return an option type, - raise a failure in the monad, or - use a bitstream oracle to resolve undefined bits. This patch adds different versions of partial functions corresponding to those options. The desired behaviour can be selected by choosing a binding in the Sail prelude. The naming scheme is that the failwith version is the default, while the other versions have the suffixes _maybe, _fail, and _oracle, respectively.
2018-03-14	Use sets instead of lists for Lem nondeterminism monad	Thomas Bauereiss
	This simplifies reasoning in Isabelle.
2018-03-05	Add support for undefined bit oracle to Lem shallow embedding	Thomas Bauereiss
	Add an Undefined outcome to the prompt monad that asks the environment for a Boolean value. For the state monad, add fields for a random generator and a seed (currently of type nat) to the state.
2018-02-26	Rename some Isabelle theories	Thomas Bauereiss
	The suffix _lemmas is more descriptive than _extras.