| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
The state monad currently assumes that tags are written to and read from
properly aligned addresses (since it does not know the capability size used in
the Sail model). This change allows the Sail model to pass in the aligned
address(es) even if data is written to an unaligned address. There might be
better ways to model tag writing, but this approach seems rather general.
|
|
Currently ignored in the state monad
|
|
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.
|
|
The suffix _lemmas is more descriptive than _extras.
|
