| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
(which might not be present).
|
|
|
|
|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
|
|
Only check for availability of Lem library if actually trying to build
an Isabelle heap image.
|
|
toolchain; use SAIL_RISCV instead to refer to sail-riscv.
|
|
|
|
Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.
|
|
|
|
|
|
The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
|
|
Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
|
|
It is used for nondeterministic choice, so Undefined might be
misleading.
|
|
Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag; this is
useful for formulating predicates on traces.
|
|
|
|
Removes some friction by back-and-forth conversion when handling events
|
|
|
|
|
|
Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
|
|
|
|
On second thought, this change should not really make a difference; the CHERI
test suite still passes without it. Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
|
|
add_vec_int and similar functions in the Lem library used unsigned instead of
signed conversion.
|
|
|
|
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
|
|
|
|
|
|
|
|
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
|
|
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
|
|
|
|
|
|
|
|
|
|
Placed in lib/isabelle/manual/document.pdf
Also fixed a few typos.
|
|
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
This simplifies reasoning in Isabelle.
|
