blob: 8348eea0e2ed5df8b69d1a2f2a2e4894960bf2b7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
# Snapshot of HOL4 output for Sail CHERI and RISC-V models
These theories are a snapshot of the generated files for the Sail
MIPS, CHERI, RISC-V, and Aarch64 models, translated to HOL4 via Lem.
They only require HOL4; the necessary Lem library files are included.
A recent checkout of HOL4 from the repository at
<https://github.com/HOL-Theorem-Prover/HOL/> is required. This snapshot was
successfully built with commit `7ed3f12`, for example. Some older versions
will fail with a Holdep error due to a lexer bug in HOL that has now been
fixed.
Note that HOL4 takes a substantial amount of time to process the definition of
the `regstate` record. In particular, allow over an hour for the MIPS model.
|
