Fix a missing ERR definition

Make use of utilsLib.adjoin_thms.

Update RISC-V model for latest version of L3.

Update RISC-V model and tools.

The source specification has been modified to avoid writing to the c_update and log components when exporting to HOL4.

Update for the latest version of L3.

Changes have been made when exporting operations of the form:

`f : args -> state -> value * state`

If the state is not changed then this is now exported as

`f : args -> state -> value`

If the state is changed but the `value` type is `unit` then it this is now exported as

`f : args -> state -> state`.

Update the RISC-V model and add decompilation support.

The model itself supports multiple cores (with a shared memory) and the state assertions reflect this, e.g.

riscv_c_gpr core reg value
riscv_MEM8 address value

However, for decompilation we fix on core 0, i.e. we use

riscv_REG reg value .

The model also supports virtual memory, but we assume that this is turned off when generating step and spec theorems.