Merge branch 'sail2' into rmem_interpreter

15 files changed, 875 insertions, 426 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index a1eef9f0..6ddc58aa 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -78,28 +78,22 @@ overload shr_int = {_shr32, _shr_int}
 
 // ***** div and mod *****
 
-val div_int = {
-  smt: "div",
-  ocaml: "quotient",
-  interpreter: "quotient",
-  lem: "integerDiv",
-  c: "tdiv_int",
-  coq: "Z.quot"
+/*! Truncating division (rounds towards zero) */
+val tdiv_int = {
+  ocaml: "tdiv_int",
+  interpreter: "tdiv_int",
+  lem: "integerDiv_t",
+  c: "tdiv_int"
 } : (int, int) -> int
 
-overload operator / = {div_int}
-
-val mod_int = {
-  smt: "mod",
-  ocaml: "modulus",
-  interpreter: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "Z.rem"
+/*! Remainder for truncating division (has sign of dividend) */
+val tmod_int = {
+  ocaml: "tmod_int",
+  interpreter: "tmod_int",
+  lem: "integerMod_t",
+  c: "tmod_int"
 } : (int, int) -> nat
 
-overload operator % = {mod_int}
-
 val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index 6dd962d1..f763db6f 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,6 @@
 BBV_DIR?=../../../bbv
 
-SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_string.v  Sail2_real.v
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_state_lifting.v  Sail2_string.v  Sail2_real.v
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv
 
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index c6fb866b..338bf10b 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -48,14 +48,13 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+Require Import DecidableClass.
 
-(*
-
-class ( EnumerationType 'a )
-  val toNat : 'a -> nat
-end
-
+Class EnumerationType (A : Type) := {
+  toNat : A -> nat
+}.
 
+(*
 val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
 let ~{ocaml} enumeration_typeCompare e1 e2 :=
   compare (toNat e1) (toNat e2)
@@ -89,6 +88,7 @@ Inductive read_kind :=
   (* x86 reads *)
   | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
 .
+Scheme Equality for read_kind.
 (*
 instance (Show read_kind)
   let show := function
@@ -121,6 +121,7 @@ Inductive write_kind :=
   (* x86 writes *)
   | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
 .
+Scheme Equality for write_kind.
 (*
 instance (Show write_kind)
   let show := function
@@ -161,6 +162,7 @@ Inductive barrier_kind :=
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE.
+Scheme Equality for barrier_kind.
 
 (*
 instance (Show barrier_kind)
@@ -196,6 +198,7 @@ end*)
 Inductive trans_kind :=
   (* AArch64 *)
   | Transaction_start | Transaction_commit | Transaction_abort.
+Scheme Equality for trans_kind.
 (*
 instance (Show trans_kind)
   let show := function
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 7e4abe29..ebab269f 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -497,3 +497,4 @@ Definition set_slice_int len n lo (v : mword len) : Z :=
   else n.
 
 Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt.
+Definition print_bits {a} (s : string) (bs : mword a) : unit := tt.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index bae8381e..8efd66f0 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -129,11 +129,11 @@ wfR) y)
  end.
 
 Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
-  match z with
+  Acc_intro _ (fun y H => match z with
   | Zpos p => pos_guard_wf p (Zwf_well_founded _) _
-  | _ => Zwf_well_founded _ _
-  end.
-
+  | Zneg p => pos_guard_wf p (Zwf_well_founded _) _
+  | Z0 => Zwf_well_founded _ _
+  end).
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index 2715b5e7..39567520 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -2,27 +2,28 @@ Require Import String.
 (*Require Import Sail_impl_base*)
 Require Import Sail2_instr_kinds.
 Require Import Sail2_values.
-
-
+Require bbv.Word.
+Import ListNotations.
 
 Definition register_name := string.
 Definition address := list bitU.
 
 Inductive monad regval a e :=
   | Done : a -> monad regval a e
-  (* Read a number : bytes from memory, returned in little endian order *)
-  | Read_mem : read_kind -> address -> nat -> (list memory_byte -> monad regval a e) -> monad regval a e
-  (* Read the tag : a memory address *)
-  | Read_tag : address -> (bitU -> monad regval a e) -> monad regval a e
-  (* Tell the system a write is imminent, at address lifted, : size nat *)
-  | Write_ea : write_kind -> address -> nat -> monad regval a e -> monad regval a e
+  (* Read a number of bytes from memory, returned in little endian order,
+     with or without a tag.  The first nat specifies the address, the second
+     the number of bytes. *)
+  | Read_mem : read_kind -> nat -> nat -> (list memory_byte -> monad regval a e) -> monad regval a e
+  | Read_memt : read_kind -> nat -> nat -> ((list memory_byte * bitU) -> monad regval a e) -> monad regval a e
+  (* Tell the system a write is imminent, at the given address and with the
+     given size. *)
+  | Write_ea : write_kind -> nat -> nat -> monad regval a e -> monad regval a e
   (* Request the result : store-exclusive *)
   | Excl_res : (bool -> monad regval a e) -> monad regval a e
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal, given in little endian order *)
-  | Write_memv : list memory_byte -> (bool -> monad regval a e) -> monad regval a e
-  (* Request to write the tag at last signalled address. *)
-  | Write_tag : address -> bitU -> (bool -> monad regval a e) -> monad regval a e
+  (* Request to write a memory value of the given size at the given address,
+     with or without a tag. *)
+  | Write_mem : write_kind -> nat -> nat -> list memory_byte -> (bool -> monad regval a e) -> monad regval a e
+  | Write_memt : write_kind -> nat -> nat -> list memory_byte -> bitU -> (bool -> monad regval a e) -> monad regval a e
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint : monad regval a e -> monad regval a e
   (* Request a memory barrier *)
@@ -31,50 +32,70 @@ Inductive monad regval a e :=
   | Read_reg : register_name -> (regval -> monad regval a e) -> monad regval a e
   (* Request to write register *)
   | Write_reg : register_name -> regval -> monad regval a e -> monad regval a e
-  | Undefined : (bool -> monad regval a e) -> monad regval a e
-  (*Result : a failed assert with possible error message to report*)
+  (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
+     argument may be used to provide information to the system about what the
+     Boolean is going to be used for. *)
+  | Choose : string -> (bool -> monad regval a e) -> monad regval a e
+  (* Print debugging or tracing information *)
+  | Print : string -> monad regval a e -> monad regval a e
+  (*Result of a failed assert with possible error message to report*)
   | Fail : string -> monad regval a e
-  | Error : string -> monad regval a e
-  (* Exception : type e *)
+  (* Exception of type e *)
   | Exception : e -> monad regval a e.
-  (* TODO: Reading/writing tags *)
 
 Arguments Done [_ _ _].
 Arguments Read_mem [_ _ _].
-Arguments Read_tag [_ _ _].
+Arguments Read_memt [_ _ _].
 Arguments Write_ea [_ _ _].
 Arguments Excl_res [_ _ _].
-Arguments Write_memv [_ _ _].
-Arguments Write_tag [_ _ _].
+Arguments Write_mem [_ _ _].
+Arguments Write_memt [_ _ _].
 Arguments Footprint [_ _ _].
 Arguments Barrier [_ _ _].
 Arguments Read_reg [_ _ _].
 Arguments Write_reg [_ _ _].
-Arguments Undefined [_ _ _].
+Arguments Choose [_ _ _].
+Arguments Print [_ _ _].
 Arguments Fail [_ _ _].
-Arguments Error [_ _ _].
 Arguments Exception [_ _ _].
 
+Inductive event {regval} :=
+  | E_read_mem : read_kind -> nat -> nat -> list memory_byte -> event
+  | E_read_memt : read_kind -> nat -> nat -> (list memory_byte * bitU) -> event
+  | E_write_mem : write_kind -> nat -> nat -> list memory_byte -> bool -> event
+  | E_write_memt : write_kind -> nat -> nat -> list memory_byte -> bitU -> bool -> event
+  | E_write_ea : write_kind -> nat -> nat -> event
+  | E_excl_res : bool -> event
+  | E_barrier : barrier_kind -> event
+  | E_footprint : event
+  | E_read_reg : register_name -> regval -> event
+  | E_write_reg : register_name -> regval -> event
+  | E_choose : string -> bool -> event
+  | E_print : string -> event.
+Arguments event : clear implicits.
+
+Definition trace regval := list (event regval).
+
 (*val return : forall rv a e. a -> monad rv a e*)
 Definition returnm {rv A E} (a : A) : monad rv A E := Done a.
 
 (*val bind : forall rv a b e. monad rv a e -> (a -> monad rv b e) -> monad rv b e*)
 Fixpoint bind {rv A B E} (m : monad rv A E) (f : A -> monad rv B E) := match m with
   | Done a => f a
-  | Read_mem rk a sz k => Read_mem rk a sz (fun v => bind (k v) f)
-  | Read_tag a k =>       Read_tag a       (fun v => bind (k v) f)
-  | Write_memv descr k => Write_memv descr (fun v => bind (k v) f)
-  | Write_tag a t k =>    Write_tag a t    (fun v => bind (k v) f)
-  | Read_reg descr k =>   Read_reg descr   (fun v => bind (k v) f)
-  | Excl_res k =>         Excl_res         (fun v => bind (k v) f)
-  | Undefined k =>        Undefined        (fun v => bind (k v) f)
-  | Write_ea wk a sz k => Write_ea wk a sz (bind k f)
-  | Footprint k =>        Footprint        (bind k f)
-  | Barrier bk k =>       Barrier bk       (bind k f)
-  | Write_reg r v k =>    Write_reg r v    (bind k f)
-  | Fail descr =>         Fail descr
-  | Error descr =>        Error descr
-  | Exception e =>        Exception e
+  | Read_mem rk a sz k =>       Read_mem rk a sz       (fun v => bind (k v) f)
+  | Read_memt rk a sz k =>      Read_memt rk a sz      (fun v => bind (k v) f)
+  | Write_mem wk a sz v k =>    Write_mem wk a sz v    (fun v => bind (k v) f)
+  | Write_memt wk a sz v t k => Write_memt wk a sz v t (fun v => bind (k v) f)
+  | Read_reg descr k =>         Read_reg descr         (fun v => bind (k v) f)
+  | Excl_res k =>               Excl_res               (fun v => bind (k v) f)
+  | Choose descr k =>           Choose descr           (fun v => bind (k v) f)
+  | Write_ea wk a sz k =>       Write_ea wk a sz       (bind k f)
+  | Footprint k =>              Footprint              (bind k f)
+  | Barrier bk k =>             Barrier bk             (bind k f)
+  | Write_reg r v k =>          Write_reg r v          (bind k f)
+  | Print msg k =>              Print msg              (bind k f)
+  | Fail descr =>               Fail descr
+  | Exception e =>              Exception e
 end.
 
 Notation "m >>= f" := (bind m f) (at level 50, left associativity).
@@ -86,8 +107,11 @@ Notation "m >> n" := (bind0 m n) (at level 50, left associativity).
 (*val exit : forall rv a e. unit -> monad rv a e*)
 Definition exit {rv A E} (_ : unit) : monad rv A E := Fail "exit".
 
+(*val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e*)
+Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm.
+
 (*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
-Definition undefined_bool {rv e} (_:unit) : monad rv bool e := Undefined returnm.
+Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool".
 
 (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
 Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
@@ -104,21 +128,21 @@ Definition throw {rv A E} e : monad rv A E := Exception e.
 
 (*val try_catch : forall rv a e1 e2. monad rv a e1 -> (e1 -> monad rv a e2) -> monad rv a e2*)
 Fixpoint try_catch {rv A E1 E2} (m : monad rv A E1) (h : E1 -> monad rv A E2) := match m with
-  | Done a =>             Done a
-  | Read_mem rk a sz k => Read_mem rk a sz (fun v => try_catch (k v) h)
-  | Read_tag a k =>       Read_tag a       (fun v => try_catch (k v) h)
-  | Write_memv descr k => Write_memv descr (fun v => try_catch (k v) h)
-  | Write_tag a t k =>    Write_tag a t     (fun v => try_catch (k v) h)
-  | Read_reg descr k =>   Read_reg descr   (fun v => try_catch (k v) h)
-  | Excl_res k =>         Excl_res         (fun v => try_catch (k v) h)
-  | Undefined k =>        Undefined        (fun v => try_catch (k v) h)
-  | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h)
-  | Footprint k =>        Footprint        (try_catch k h)
-  | Barrier bk k =>       Barrier bk       (try_catch k h)
-  | Write_reg r v k =>    Write_reg r v    (try_catch k h)
-  | Fail descr =>         Fail descr
-  | Error descr =>        Error descr
-  | Exception e =>        h e
+  | Done a =>                   Done a
+  | Read_mem rk a sz k =>       Read_mem rk a sz       (fun v => try_catch (k v) h)
+  | Read_memt rk a sz k =>      Read_memt rk a sz      (fun v => try_catch (k v) h)
+  | Write_mem wk a sz v k =>    Write_mem wk a sz v    (fun v => try_catch (k v) h)
+  | Write_memt wk a sz v t k => Write_memt wk a sz v t (fun v => try_catch (k v) h)
+  | Read_reg descr k =>         Read_reg descr         (fun v => try_catch (k v) h)
+  | Excl_res k =>               Excl_res               (fun v => try_catch (k v) h)
+  | Choose descr k =>           Choose descr           (fun v => try_catch (k v) h)
+  | Write_ea wk a sz k =>       Write_ea wk a sz       (try_catch k h)
+  | Footprint k =>              Footprint              (try_catch k h)
+  | Barrier bk k =>             Barrier bk             (try_catch k h)
+  | Write_reg r v k =>          Write_reg r v          (try_catch k h)
+  | Print msg k =>              Print msg              (try_catch k h)
+  | Fail descr =>               Fail descr
+  | Exception e =>              h e
 end.
 
 (* For early return, we abuse exceptions by throwing and catching
@@ -158,9 +182,23 @@ match x with
   | None => Fail msg
 end.
 
+(*val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e*)
+Definition read_memt_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte * bitU) E :=
+  Read_memt rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
+
+(*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*)
+Definition read_memt {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E :=
+  bind
+    (read_memt_bytes rk addr sz)
+    (fun '(bytes, tag) =>
+       match of_bits (bits_of_mem_bytes bytes) with
+       | Some v => returnm (v, tag)
+       | None => Fail "bits_of_mem_bytes"
+       end).
+
 (*val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e*)
 Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte) E :=
-  Read_mem rk (bits_of addr) (Z.to_nat sz) returnm.
+  Read_mem rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
 
 (*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*)
 Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B) E :=
@@ -169,50 +207,56 @@ Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : mo
     (fun bytes =>
        maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))).
 
-(*val read_tag : forall rv a e. Bitvector a => a -> monad rv bitU e*)
-Definition read_tag {rv a e} `{Bitvector a} (addr : a) : monad rv bitU e :=
- Read_tag (bits_of addr) returnm.
-
 (*val excl_result : forall rv e. unit -> monad rv bool e*)
 Definition excl_result {rv e} (_:unit) : monad rv bool e :=
   let k successful := (returnm successful) in
   Excl_res k.
 
-Definition write_mem_ea {rv a E} `{Bitvector a} wk (addr: a) sz : monad rv unit E :=
- Write_ea wk (bits_of addr) (Z.to_nat sz) (Done tt).
-
-Definition write_mem_val {rv a e} `{Bitvector a} (v : a) : monad rv bool e := match mem_bytes_of_bits v with
-  | Some v => Write_memv v returnm
-  | None => Fail "write_mem_val"
-end.
-
-(*val write_tag : forall rv a e. Bitvector 'a => 'a -> bitU -> monad rv bool e*)
-Definition write_tag {rv a e} (addr : mword a) (b : bitU) : monad rv bool e := Write_tag (bits_of addr) b returnm.
+Definition write_mem_ea {rv a E} wk (addr: mword a) sz : monad rv unit E :=
+ Write_ea wk (Word.wordToNat (get_word addr)) (Z.to_nat sz) (Done tt).
+
+(*val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e*)
+Definition write_mem {rv a b E} wk (addr : mword a) sz (v : mword b) : monad rv bool E :=
+  match (mem_bytes_of_bits v, Word.wordToNat (get_word addr)) with
+    | (Some v, addr) =>
+       Write_mem wk addr (Z.to_nat sz) v returnm
+    | _ => Fail "write_mem"
+  end.
+
+(*val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e*)
+Definition write_memt {rv a b E} wk (addr : mword a) sz (v : mword b) tag : monad rv bool E :=
+  match (mem_bytes_of_bits v, Word.wordToNat (get_word addr)) with
+    | (Some v, addr) =>
+       Write_memt wk addr (Z.to_nat sz) v tag returnm
+    | _ => Fail "write_mem"
+  end.
 
 Definition read_reg {s rv a e} (reg : register_ref s rv a) : monad rv a e :=
   let k v :=
     match reg.(of_regval) v with
       | Some v => Done v
-      | None => Error "read_reg: unrecognised value"
+      | None => Fail "read_reg: unrecognised value"
     end
   in
   Read_reg reg.(name) k.
 
 (* TODO
-val read_reg_range : forall s r rv a e. Bitvector a => register_ref s rv r -> integer -> integer -> monad rv a e
-Definition read_reg_range reg i j :=
-  read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
+val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
+let read_reg_range reg i j =
+  read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))
 
-Definition read_reg_bit reg i :=
-  read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
-  returnm (extract_only_element v)
+let read_reg_bit reg i =
+  read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
+  return (extract_only_element v)
 
-Definition read_reg_field reg regfield :=
+let read_reg_field reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield)
 
-Definition read_reg_bitfield reg regfield :=
+let read_reg_bitfield reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  returnm (extract_only_element v)*)
+  return (extract_only_element v)*)
 
 Definition reg_deref {s rv a e} := @read_reg s rv a e.
 
@@ -221,27 +265,101 @@ Definition write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv u
  Write_reg reg.(name) (reg.(regval_of) v) (Done tt).
 
 (* TODO
-Definition write_reg reg v :=
+let write_reg reg v =
   write_reg_aux (external_reg_whole reg) v
-Definition write_reg_range reg i j v :=
-  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
-Definition write_reg_pos reg i v :=
-  let iN := natFromInteger i in
+let write_reg_range reg i j v =
+  write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v
+let write_reg_pos reg i v =
+  let iN = nat_of_int i in
   write_reg_aux (external_reg_slice reg (iN,iN)) [v]
-Definition write_reg_bit := write_reg_pos
-Definition write_reg_field reg regfield v :=
+let write_reg_bit = write_reg_pos
+let write_reg_field reg regfield v =
   write_reg_aux (external_reg_field_whole reg regfield.field_name) v
-Definition write_reg_field_bit reg regfield bit :=
+let write_reg_field_bit reg regfield bit =
   write_reg_aux (external_reg_field_whole reg regfield.field_name)
                 (Vector [bit] 0 (is_inc_of_reg reg))
-Definition write_reg_field_range reg regfield i j v :=
-  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
-Definition write_reg_field_pos reg regfield i v :=
+let write_reg_field_range reg regfield i j v =
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v
+let write_reg_field_pos reg regfield i v =
   write_reg_field_range reg regfield i i [v]
-Definition write_reg_field_bit := write_reg_field_pos*)
+let write_reg_field_bit = write_reg_field_pos*)
 
 (*val barrier : forall rv e. barrier_kind -> monad rv unit e*)
 Definition barrier {rv e} bk : monad rv unit e := Barrier bk (Done tt).
 
 (*val footprint : forall rv e. unit -> monad rv unit e*)
 Definition footprint {rv e} (_ : unit) : monad rv unit e := Footprint (Done tt).
+
+(* Event traces *)
+
+Local Open Scope bool_scope.
+
+(*val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)*)
+Definition emitEvent {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (m : monad Regval A E) (e : event Regval) : option (monad Regval A E) :=
+ match (e, m) with
+  | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) =>
+     if read_kind_beq rk' rk && Nat.eqb a' a && Nat.eqb sz' sz then Some (k v) else None
+  | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) =>
+     if read_kind_beq rk' rk && Nat.eqb a' a && Nat.eqb sz' sz then Some (k vt) else None
+  | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) =>
+     if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz && generic_eq v' v then Some (k r) else None
+  | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) =>
+     if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz && generic_eq v' v && generic_eq tag' tag then Some (k r) else None
+  | (E_read_reg r v, Read_reg r' k) =>
+     if generic_eq r' r then Some (k v) else None
+  | (E_write_reg r v, Write_reg r' v' k) =>
+     if generic_eq r' r && generic_eq v' v then Some k else None
+  | (E_write_ea wk a sz, Write_ea wk' a' sz' k) =>
+     if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz then Some k else None
+  | (E_barrier bk, Barrier bk' k) =>
+     if barrier_kind_beq bk' bk then Some k else None
+  | (E_print m, Print m' k) =>
+     if generic_eq m' m then Some k else None
+  | (E_excl_res v, Excl_res k) => Some (k v)
+  | (E_choose descr v, Choose descr' k) => if generic_eq descr' descr then Some (k v) else None
+  | (E_footprint, Footprint k) => Some k
+  | _ => None
+end.
+
+Definition option_bind {A B : Type} (a : option A) (f : A -> option B) : option B :=
+match a with
+| Some x => f x
+| None => None
+end.
+
+(*val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)*)
+Fixpoint runTrace {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) : option (monad Regval A E) :=
+match t with
+  | [] => Some m
+  | e :: t' => option_bind (emitEvent m e) (runTrace t')
+end.
+
+(*val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool*)
+Definition final {Regval A E} (m : monad Regval A E) : bool :=
+match m with
+  | Done _ => true
+  | Fail _ => true
+  | Exception _ => true
+  | _ => false
+end.
+
+(*val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasTrace {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) : bool :=
+match runTrace t m with
+  | Some m => final m
+  | None => false
+end.
+
+(*val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasException {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) :=
+match runTrace t m with
+  | Some (Exception _) => true
+  | _ => false
+end.
+
+(*val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasFailure {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) :=
+match runTrace t m with
+  | Some (Fail _) => true
+  | _ => false
+end.
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 1d5cb342..b73d5013 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -3,53 +3,82 @@ Require Import Sail2_values.
 Require Import Sail2_prompt_monad.
 Require Import Sail2_prompt.
 Require Import Sail2_state_monad.
-(*
-(* State monad wrapper around prompt monad *)
-
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
-  | (Done a)             -> returnS a
-  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
-  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
-  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
-  | (Write_tagv t k)     -> bindS (write_tagS t)            (fun v -> liftState ra (k v))
-  | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
-  | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
-  | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
-  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
-  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
-  | (Footprint k)        -> liftState ra k
-  | (Barrier _ k)        -> liftState ra k
-  | (Fail descr)         -> failS descr
-  | (Error descr)        -> failS descr
-  | (Exception e)        -> throwS e
-end
-
-
-val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let rec iterS_aux i f xs = match xs with
-  | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
-  | [] -> returnS ()
-  end
+Import ListNotations.
 
-declare {isabelle} termination_argument iterS_aux = automatic
+(*val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
+Fixpoint iterS_aux {RV A E} i (f : Z -> A -> monadS RV unit E) (xs : list A) :=
+ match xs with
+  | x :: xs => f i x >>$ iterS_aux (i + 1) f xs
+  | [] => returnS tt
+  end.
 
-val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let iteriS f xs = iterS_aux 0 f xs
+(*val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
+Definition iteriS {RV A E} (f : Z -> A -> monadS RV unit E) (xs : list A) : monadS RV unit E :=
+ iterS_aux 0 f xs.
 
-val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let iterS f xs = iteriS (fun _ x -> f x) xs
+(*val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
+Definition iterS {RV A E} (f : A -> monadS RV unit E) (xs : list A) : monadS RV unit E :=
+ iteriS (fun _ x => f x) xs.
 
-val foreachS : forall 'a 'rv 'vars 'e.
-  list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
-let rec foreachS xs vars body = match xs with
-  | [] -> returnS vars
-  | x :: xs ->
-     body x vars >>$= fun vars ->
+(*val foreachS : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e*)
+Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> monadS RV Vars E) : monadS RV Vars E :=
+ match xs with
+  | [] => returnS vars
+  | x :: xs =>
+     body x vars >>$= fun vars =>
      foreachS xs vars body
-end
+end.
+
+(*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*)
+Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E :=
+  let indices := genlist (fun n => n) n in
+  foreachS indices [] (fun n xs => (f n >>$= (fun x => returnS (xs ++ [x])))).
+
+(*val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*)
+Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
+ l >>$= (fun l => if l then r else returnS false).
+
+(*val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*)
+Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
+ l >>$= (fun l => if l then returnS true else r).
+
+(*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*)
+Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E :=
+match b with
+  | B0 => returnS false
+  | B1 => returnS true
+  | BU => failS "bool_of_bitU"
+end.
+
+(*val bool_of_bitU_nondetS : forall 'rv 'e. bitU -> monadS 'rv bool 'e*)
+Definition bool_of_bitU_nondetS {RV E} (b : bitU) : monadS RV bool E :=
+match b with
+  | B0 => returnS false
+  | B1 => returnS true
+  | BU => undefined_boolS tt
+end.
+
+(*val bools_of_bits_nondetS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e*)
+Definition bools_of_bits_nondetS {RV E} bits : monadS RV (list bool) E :=
+  foreachS bits []
+    (fun b bools =>
+      bool_of_bitU_nondetS b >>$= (fun b =>
+      returnS (bools ++ [b]))).
 
-declare {isabelle} termination_argument foreachS = automatic
+(*val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
+Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
+  bools_of_bits_nondetS bits >>$= (fun bs =>
+  returnS (of_bools bs)).
+
+(*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
+Definition of_bits_failS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
+ maybe_failS "of_bits" (of_bits bits).
+
+(*val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_nondetS () =
+  bools_of_bits_nondetS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+  returnS (wordFromBitlist bs))
 
 
 val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
@@ -67,3 +96,21 @@ let rec untilS vars cond body s =
   (cond vars >>$= (fun cond_val s'' ->
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
 *)
+(*val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e*)
+Definition choose_boolsS {RV E} n : monadS RV (list bool) E :=
+ genlistS (fun _ => choose_boolS tt) n.
+
+(* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
+(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
+let internal_pickS xs =
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_boolsS (List.length xs) >>$= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> returnS x
+    | Nothing -> failS "choose internal_pick"
+  end
+
+
+*)
diff --git a/lib/coq/Sail2_state_lifting.v b/lib/coq/Sail2_state_lifting.v
new file mode 100644
index 00000000..633c0ef7
--- /dev/null
+++ b/lib/coq/Sail2_state_lifting.v
@@ -0,0 +1,61 @@
+Require Import Sail2_values.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+Require Import Sail2_state_monad.
+Import ListNotations.
+
+(* Lifting from prompt monad to state monad *)
+(*val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e*)
+Fixpoint liftState {Regval Regs A E} (ra : register_accessors Regs Regval) (m : monad Regval A E) : monadS Regs A E :=
+ match m with
+  | (Done a)                   => returnS a
+  | (Read_mem rk a sz k)       => bindS (read_mem_bytesS rk a sz)       (fun v => liftState ra (k v))
+  | (Read_memt rk a sz k)      => bindS (read_memt_bytesS rk a sz)      (fun v => liftState ra (k v))
+  | (Write_mem wk a sz v k)    => bindS (write_mem_bytesS wk a sz v)    (fun v => liftState ra (k v))
+  | (Write_memt wk a sz v t k) => bindS (write_memt_bytesS wk a sz v t) (fun v => liftState ra (k v))
+  | (Read_reg r k)             => bindS (read_regvalS ra r)             (fun v => liftState ra (k v))
+  | (Excl_res k)               => bindS (excl_resultS tt)               (fun v => liftState ra (k v))
+  | (Choose _ k)               => bindS (choose_boolS tt)               (fun v => liftState ra (k v))
+  | (Write_reg r v k)          => seqS (write_regvalS ra r v)           (liftState ra k)
+  | (Write_ea _ _ _ k)         => liftState ra k
+  | (Footprint k)              => liftState ra k
+  | (Barrier _ k)              => liftState ra k
+  | (Print _ k)                => liftState ra k (* TODO *)
+  | (Fail descr)               => failS descr
+  | (Exception e)              => throwS e
+end.
+
+Local Open Scope bool_scope.
+
+(*val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
+Definition emitEventS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (e : event Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
+match e with
+  | E_read_mem _ addr sz v =>
+     option_bind (get_mem_bytes addr sz s) (fun '(v', _) =>
+     if generic_eq v' v then Some s else None)
+  | E_read_memt _ addr sz (v, tag) =>
+     option_bind (get_mem_bytes addr sz s) (fun '(v', tag') =>
+     if generic_eq v' v && generic_eq tag' tag then Some s else None)
+  | E_write_mem _ addr sz v success =>
+     if success then Some (put_mem_bytes addr sz v B0 s) else None
+  | E_write_memt _ addr sz v tag success =>
+     if success then Some (put_mem_bytes addr sz v tag s) else None
+  | E_read_reg r v =>
+     let (read_reg, _) := ra in
+     option_bind (read_reg r s.(regstate)) (fun v' =>
+     if generic_eq v' v then Some s else None)
+  | E_write_reg r v =>
+     let (_, write_reg) := ra in
+     option_bind (write_reg r v s.(regstate)) (fun rs' =>
+     Some {| regstate := rs'; memstate := s.(memstate); tagstate := s.(tagstate) |})
+  | _ => Some s
+end.
+
+Local Close Scope bool_scope.
+
+(*val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
+Fixpoint runTraceS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (t : trace Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
+match t with
+  | [] => Some s
+  | e :: t' => option_bind (emitEventS ra e s) (runTraceS ra t')
+end.
diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v
index c48db31b..235e4b9e 100644
--- a/lib/coq/Sail2_state_monad.v
+++ b/lib/coq/Sail2_state_monad.v
@@ -1,184 +1,237 @@
 Require Import Sail2_instr_kinds.
 Require Import Sail2_values.
-(*
-(* 'a is result type *)
-
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
+Require FMapList.
+Require Import OrderedType.
+Require OrderedTypeEx.
+Require Import List.
+Require bbv.Word.
+Import ListNotations.
+
+(* TODO: revisit choice of FMapList *)
+Module NatMap := FMapList.Make(OrderedTypeEx.Nat_as_OT).
+
+Definition Memstate : Type := NatMap.t memory_byte.
+Definition Tagstate : Type := NatMap.t bitU.
 (* type regstate = map string (vector bitU) *)
 
-type sequential_state 'regs =
-  <| regstate : 'regs;
-     memstate : memstate;
-     tagstate : tagstate;
-     write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool|>
-
-val init_state : forall 'regs. 'regs -> sequential_state 'regs
-let init_state regs =
-  <| regstate = regs;
-     memstate = Map.empty;
-     tagstate = Map.empty;
-     write_ea = Nothing;
-     last_exclusive_operation_was_load = false |>
-
-type ex 'e =
-  | Failure of string
-  | Throw of 'e
-
-type result 'a 'e =
-  | Value of 'a
-  | Ex of (ex 'e)
+Record sequential_state {Regs} :=
+  { regstate : Regs;
+    memstate : Memstate;
+    tagstate : Tagstate }.
+Arguments sequential_state : clear implicits.
+
+(*val init_state : forall 'regs. 'regs -> sequential_state 'regs*)
+Definition init_state {Regs} regs : sequential_state Regs :=
+  {| regstate := regs;
+     memstate := NatMap.empty _;
+     tagstate := NatMap.empty _ |}.
+
+Inductive ex E :=
+  | Failure : string -> ex E
+  | Throw : E -> ex E.
+Arguments Failure {E} _.
+Arguments Throw {E} _.
+
+Inductive result A E :=
+  | Value : A -> result A E
+  | Ex : ex E -> result A E.
+Arguments Value {A} {E} _.
+Arguments Ex {A} {E} _.
 
 (* State, nondeterminism and exception monad with result value type 'a
    and exception type 'e. *)
-type monadS 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs)
-
-val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e
-let returnS a s = [(Value a,s)]
-
-val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e
-let bindS m f (s : sequential_state 'regs) =
-  List.concatMap (function
-                  | (Value a, s') -> f a s'
-                  | (Ex e, s') -> [(Ex e, s')]
-                  end) (m s)
-
-val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
-let seqS m n = bindS m (fun (_ : unit) -> n)
-
+(* TODO: the list was originally a set, can we reasonably go back to a set? *)
+Definition monadS Regs a e : Type :=
+ sequential_state Regs -> list (result a e * sequential_state Regs).
+
+(*val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e*)
+Definition returnS {Regs A E} (a:A) : monadS Regs A E := fun s => [(Value a,s)].
+
+(*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*)
+Definition bindS {Regs A B E} (m : monadS Regs A E) (f : A -> monadS Regs B E) : monadS Regs B E :=
+ fun (s : sequential_state Regs) =>
+  List.concat (List.map (fun v => match v with
+                | (Value a, s') => f a s'
+                | (Ex e, s') => [(Ex e, s')]
+                end) (m s)).
+
+(*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*)
+Definition seqS {Regs B E} (m : monadS Regs unit E) (n : monadS Regs B E) : monadS Regs B E :=
+ bindS m (fun (_ : unit) => n).
+(*
 let inline (>>$=) = bindS
 let inline (>>$) = seqS
-
-val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e
-let chooseS xs s = List.map (fun x -> (Value x, s)) xs
-
-val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
-let readS f = (fun s -> returnS (f s) s)
-
-val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
-let updateS f = (fun s -> returnS () (f s))
-
-val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
-let failS msg s = [(Ex (Failure msg), s)]
-
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () = failS "exit"
-
-val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
-let throwS e s = [(Ex (Throw e), s)]
-
-val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2
-let try_catchS m h s =
-  List.concatMap (function
-                  | (Value a, s') -> returnS a s'
-                  | (Ex (Throw e), s') -> h e s'
-                  | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')]
-                  end) (m s)
-
-val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e
-let assert_expS exp msg = if exp then returnS () else failS msg
+*)
+Notation "m >>$= f" := (bindS m f) (at level 50, left associativity).
+Notation "m >>$ n" := (seqS m n) (at level 50, left associativity).
+
+(*val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e*)
+Definition chooseS {Regs A E} (xs : list A) : monadS Regs A E :=
+ fun s => (List.map (fun x => (Value x, s)) xs).
+
+(*val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e*)
+Definition readS {Regs A E} (f : sequential_state Regs -> A) : monadS Regs A E :=
+ (fun s => returnS (f s) s).
+
+(*val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e*)
+Definition updateS {Regs E} (f : sequential_state Regs -> sequential_state Regs) : monadS Regs unit E :=
+ (fun s => returnS tt (f s)).
+
+(*val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e*)
+Definition failS {Regs A E} msg : monadS Regs A E :=
+ fun s => [(Ex (Failure msg), s)].
+
+(*val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e*)
+Definition choose_boolS {Regs E} (_:unit) : monadS Regs bool E :=
+ chooseS [false; true].
+Definition undefined_boolS {Regs E} := @choose_boolS Regs E.
+
+(*val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e*)
+Definition exitS {Regs A E} (_:unit) : monadS Regs A E := failS "exit".
+
+(*val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e*)
+Definition throwS {Regs A E} (e : E) :monadS Regs A E :=
+ fun s => [(Ex (Throw e), s)].
+
+(*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2*)
+Definition try_catchS {Regs A E1 E2} (m : monadS Regs A E1) (h : E1 -> monadS Regs A E2) : monadS Regs A E2 :=
+fun s =>
+  List.concat (List.map (fun v => match v with
+                | (Value a, s') => returnS a s'
+                | (Ex (Throw e), s') => h e s'
+                | (Ex (Failure msg), s') => [(Ex (Failure msg), s')]
+                end) (m s)).
+
+(*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*)
+Definition assert_expS {Regs E} (exp : bool) (msg : string) : monadS Regs unit E :=
+ if exp then returnS tt else failS msg.
 
 (* For early return, we abuse exceptions by throwing and catching
    the return value. The exception type is "either 'r 'e", where "Right e"
    represents a proper exception and "Left r" an early return of value "r". *)
-type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+Definition monadRS Regs A R E := monadS Regs A (sum R E).
 
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
-let early_returnS r = throwS (Left r)
+(*val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e*)
+Definition early_returnS {Regs A R E} (r : R) : monadRS Regs A R E := throwS (inl r).
 
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
-let catch_early_returnS m =
+(*val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e*)
+Definition catch_early_returnS {Regs A E} (m : monadRS Regs A A E) : monadS Regs A E :=
   try_catchS m
-    (function
-      | Left a -> returnS a
-      | Right e -> throwS e
-     end)
+    (fun v => match v with
+      | inl a => returnS a
+      | inr e => throwS e
+     end).
 
 (* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+(*val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e*)
+Definition liftRS {A R Regs E} (m : monadS Regs A E) : monadRS Regs A R E :=
+ try_catchS m (fun e => throwS (inr e)).
 
 (* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) ->  monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+(*val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2*)
+Definition try_catchRS {Regs A R E1 E2} (m : monadRS Regs A R E1) (h : E1 -> monadRS Regs A R E2) : monadRS Regs A R E2 :=
   try_catchS m
-    (function
-      | Left r -> throwS (Left r)
-      | Right e -> h e
-     end)
+    (fun v => match v with
+      | inl r => throwS (inl r)
+      | inr e => h e
+     end).
+
+(*val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e*)
+Definition maybe_failS {Regs A E} msg (v : option A) : monadS Regs A E :=
+match v with
+  | Some a  => returnS a
+  | None => failS msg
+end.
+
+(*val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e*)
+Definition read_tagS {Regs A E} (addr : mword A) : monadS Regs bitU E :=
+  let addr := Word.wordToNat (get_word addr) in
+  readS (fun s => opt_def B0 (NatMap.find addr s.(tagstate))).
+
+Fixpoint genlist_acc {A:Type} (f : nat -> A) n acc : list A :=
+  match n with
+    | O => acc
+    | S n' => genlist_acc f n' (f n' :: acc)
+  end.
+Definition genlist {A} f n := @genlist_acc A f n [].
 
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
-let read_tagS addr =
-  readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate))
 
 (* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS read_kind addr sz =
-  let addr = unsigned addr in
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
-  let read_byte s addr = Map.lookup addr s.memstate in
-  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
-    | Just mem_val ->
-       updateS (fun s ->
-         if read_is_exclusive read_kind
-         then <| s with last_exclusive_operation_was_load = true |>
-         else s) >>$
-       returnS mem_val
-    | Nothing -> failS "read_memS"
-  end)
-
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
-let read_memS rk a sz =
-  read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes ->
-  returnS (bits_of_mem_bytes bytes))
-
-val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () =
-  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
-  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
-  chooseS (if excl_load then [false; true] else [false]))
-
-val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz =
-  let addr = unsigned addr in
-  let sz = integerFromNat sz in
-  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)
-
-(* Write little-endian list of bytes to previously announced address *)
-val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS v =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, sz) ->
-         let addrs = index_list addr (addr+sz-1) 1 in
-         (*let v = external_mem_value (bits_of v) in*)
-         let a_v = List.zip addrs v in
-         let write_byte mem (addr, v) = Map.insert addr v mem in
-         updateS (fun s ->
-           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
-         returnS true
-    end)
-
-val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
-let write_mem_valS v = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS v
-  | Nothing -> failS "write_mem_val"
-end
-
-val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e
-let write_tagS t =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, _) ->
-         (*let taddr = addr / cap_alignment in*)
-         updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-         returnS true
-    end)
-
-val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
-let read_regS reg = readS (fun s -> reg.read_from s.regstate)
+(*val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)*)
+Definition get_mem_bytes {Regs} addr sz (s : sequential_state Regs) : option (list memory_byte * bitU) :=
+  let addrs := genlist (fun n => addr + n)%nat sz in
+  let read_byte s addr := NatMap.find addr s.(memstate) in
+  let read_tag s addr := opt_def B0 (NatMap.find addr s.(tagstate)) in
+  option_map
+    (fun mem_val => (mem_val, List.fold_left and_bit (List.map (read_tag s) addrs) B1))
+    (just_list (List.map (read_byte s) addrs)).
+
+(*val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e*)
+Definition read_memt_bytesS {Regs E} (_ : read_kind) addr sz : monadS Regs (list memory_byte * bitU) E :=
+  readS (get_mem_bytes addr sz) >>$=
+  maybe_failS "read_memS".
+
+(*val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e*)
+Definition read_mem_bytesS {Regs E} (rk : read_kind) addr sz : monadS Regs (list memory_byte) E :=
+  read_memt_bytesS rk addr sz >>$= (fun '(bytes, _) =>
+  returnS bytes).
+
+(*val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e*)
+Definition read_memtS {Regs E A B} (rk : read_kind) (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B * bitU) E :=
+  let a := Word.wordToNat (get_word a) in
+  read_memt_bytesS rk a (Z.to_nat sz) >>$= (fun '(bytes, tag) =>
+  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val =>
+  returnS (mem_val, tag))).
+
+(*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e*)
+Definition read_memS {Regs E A B} rk (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B) E :=
+  read_memtS rk a sz >>$= (fun '(bytes, _) =>
+  returnS bytes).
+
+(*val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e*)
+Definition excl_resultS {Regs E} : unit -> monadS Regs bool E :=
+  (* TODO: This used to be more deterministic, checking a flag in the state
+     whether an exclusive load has occurred before.  However, this does not
+     seem very precise; it might be safer to overapproximate the possible
+     behaviours by always making a nondeterministic choice. *)
+  @undefined_boolS Regs E.
+
+(* Write little-endian list of bytes to given address *)
+(*val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs*)
+Definition put_mem_bytes {Regs} addr sz (v : list memory_byte) (tag : bitU) (s : sequential_state Regs) : sequential_state Regs :=
+  let addrs := genlist (fun n => addr + n)%nat sz in
+  let a_v := List.combine addrs v in
+  let write_byte mem '(addr, v) := NatMap.add addr v mem in
+  let write_tag mem addr := NatMap.add addr tag mem in
+  {| regstate := s.(regstate);
+     memstate := List.fold_left write_byte a_v s.(memstate);
+     tagstate := List.fold_left write_tag addrs s.(tagstate) |}.
+
+(*val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e*)
+Definition write_memt_bytesS {Regs E} (_ : write_kind) addr sz (v : list memory_byte) (t : bitU) : monadS Regs bool E :=
+  updateS (put_mem_bytes addr sz v t) >>$
+  returnS true.
+
+(*val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e*)
+Definition write_mem_bytesS {Regs E} wk addr sz (v : list memory_byte) : monadS Regs bool E :=
+ write_memt_bytesS wk addr sz v B0.
+
+(*val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e*)
+Definition write_memtS {Regs E A B} wk (addr : mword A) sz (v : mword B) (t : bitU) : monadS Regs bool E :=
+  match (Word.wordToNat (get_word addr), mem_bytes_of_bits v) with
+    | (addr, Some v) => write_memt_bytesS wk addr (Z.to_nat sz) v t
+    | _ => failS "write_mem"
+  end.
+
+(*val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e*)
+Definition write_memS {Regs E A B} wk (addr : mword A) sz (v : mword B) : monadS Regs bool E :=
+ write_memtS wk addr sz v B0.
+
+(*val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*)
+Definition read_regS {Regs RV A E} (reg : register_ref Regs RV A) : monadS Regs A E :=
+ readS (fun s => reg.(read_from) s.(regstate)).
 
 (* TODO
 let read_reg_range reg i j state =
@@ -194,25 +247,27 @@ let read_reg_bitfield reg regfield =
   let (i,_) = register_field_indices reg regfield in
   read_reg_bit reg i *)
 
-val read_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg =
-  readS (fun s -> read reg s.regstate) >>$= (function
-      | Just v ->  returnS v
-      | Nothing -> failS ("read_regvalS " ^ reg)
-    end)
-
-val write_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
-let write_regvalS (_, write) reg v =
-  readS (fun s -> write reg v s.regstate) >>$= (function
-      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
-      | Nothing ->  failS ("write_regvalS " ^ reg)
-    end)
-
-val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
-let write_regS reg v =
-  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
+(*val read_regvalS : forall 'regs 'rv 'e.
+  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e*)
+Definition read_regvalS {Regs RV E} (acc : register_accessors Regs RV) reg : monadS Regs RV E :=
+  let '(read, _) := acc in
+  readS (fun s => read reg s.(regstate)) >>$= (fun v => match v with
+      | Some v =>  returnS v
+      | None => failS ("read_regvalS " ++ reg)
+    end).
+
+(*val write_regvalS : forall 'regs 'rv 'e.
+  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*)
+Definition write_regvalS {Regs RV E} (acc : register_accessors Regs RV) reg (v : RV) : monadS Regs unit E :=
+  let '(_, write) := acc in
+  readS (fun s => write reg v s.(regstate)) >>$= (fun x => match x with
+      | Some rs' => updateS (fun s => {| regstate := rs'; memstate := s.(memstate); tagstate := s.(tagstate) |})
+      | None =>  failS ("write_regvalS " ++ reg)
+    end).
+
+(*val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*)
+Definition write_regS {Regs RV A E} (reg : register_ref Regs RV A) (v:A) : monadS Regs unit E :=
+  updateS (fun s => {| regstate := reg.(write_to) v s.(regstate); memstate := s.(memstate); tagstate := s.(tagstate) |}).
 
 (* TODO
 val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
@@ -250,4 +305,17 @@ let update_reg_field_bit regfield i reg_val bit =
   let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
-*)
+
+(* TODO Add Show typeclass for value and exception type *)
+(*val show_result : forall 'a 'e. result 'a 'e -> string*)
+Definition show_result {A E} (x : result A E) : string := match x with
+  | Value _ => "Value ()"
+  | Ex (Failure msg) => "Failure " ++ msg
+  | Ex (Throw _) => "Throw"
+end.
+
+(*val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit*)
+Definition prerr_results {A E S} (rs : list (result A E * S)) : unit := tt.
+(*  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
+  ()*)
+
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index f11e057a..d1f1a768 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -110,6 +110,9 @@ refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H'
 * right. intuition.
 Defined.
 
+Instance Decidable_eq_list {A : Type} `(D : forall x y : A, Decidable (x = y)) : forall (x y : list A), Decidable (x = y) :=
+  Decidable_eq_from_dec (list_eq_dec (fun x y => generic_dec x y)).
+
 (* Used by generated code that builds Decidable equality instances for records. *)
 Ltac cmp_record_field x y :=
   let H := fresh "H" in
@@ -144,6 +147,47 @@ unfold pow.
 auto using Z.le_refl.
 Qed.
 
+Lemma ZEuclid_div_pos : forall x y, y > 0 -> x >= 0 -> ZEuclid.div x y >= 0.
+intros.
+unfold ZEuclid.div.
+change 0 with (0 * 0).
+apply Zmult_ge_compat; auto with zarith.
+* apply Z.le_ge. apply Z.sgn_nonneg. apply Z.ge_le. auto with zarith.
+* apply Z_div_ge0; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith.
+Qed.
+
+Lemma ZEuclid_div_ge : forall x y, y > 0 -> x >= 0 -> x - ZEuclid.div x y >= 0.
+intros.
+unfold ZEuclid.div.
+rewrite Z.sgn_pos; auto with zarith.
+rewrite Z.mul_1_l.
+apply Z.le_ge.
+apply Zle_minus_le_0.
+apply Z.div_le_upper_bound.
+* apply Z.abs_pos. auto with zarith.
+* rewrite Z.mul_comm.
+  assert (0 < Z.abs y). {
+    apply Z.abs_pos.
+    omega.
+  }
+  revert H1.
+  generalize (Z.abs y). intros. nia.
+Qed.
+
+Lemma ZEuclid_div_mod0 : forall x y, y <> 0 ->
+  ZEuclid.modulo x y = 0 ->
+  y * ZEuclid.div x y = x.
+intros x y H1 H2.
+rewrite Zplus_0_r_reverse at 1.
+rewrite <- H2.
+symmetry.
+apply ZEuclid.div_mod.
+assumption.
+Qed.
+
+Hint Resolve ZEuclid_div_pos ZEuclid_div_ge ZEuclid_div_mod0 : sail.
+
+
 (*
 Definition inline lt := (<)
 Definition inline gt := (>)
@@ -416,19 +460,23 @@ Definition binop_bit op x y :=
   match (x, y) with
   | (BU,_) => BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
   | (_,BU) => BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (x,y) => bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y))
+(*  | (x,y) => bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y))*)
+  | (B0,B0) => bitU_of_bool (op false false)
+  | (B0,B1) => bitU_of_bool (op false  true)
+  | (B1,B0) => bitU_of_bool (op  true false)
+  | (B1,B1) => bitU_of_bool (op  true  true)
   end.
 
-(*val and_bit : bitU -> bitU -> bitU
-Definition and_bit := binop_bit (&&)
+(*val and_bit : bitU -> bitU -> bitU*)
+Definition and_bit := binop_bit andb.
 
-val or_bit : bitU -> bitU -> bitU
-Definition or_bit := binop_bit (||)
+(*val or_bit : bitU -> bitU -> bitU*)
+Definition or_bit := binop_bit orb.
 
-val xor_bit : bitU -> bitU -> bitU
-Definition xor_bit := binop_bit xor
+(*val xor_bit : bitU -> bitU -> bitU*)
+Definition xor_bit := binop_bit xorb.
 
-val (&.) : bitU -> bitU -> bitU
+(*val (&.) : bitU -> bitU -> bitU
 Definition inline (&.) x y := and_bit x y
 
 val (|.) : bitU -> bitU -> bitU
@@ -1061,8 +1109,8 @@ Ltac unbool_comparisons_goal :=
   | |- context [generic_eq _ _ = false] => apply generic_eq_false
   | |- context [generic_neq _ _ = true] => apply generic_neq_true
   | |- context [generic_neq _ _ = false] => apply generic_neq_false
-  | |- context [_ <> true] => rewrite Bool.not_true_iff_false
-  | |- context [_ <> false] => rewrite Bool.not_false_iff_true
+  | |- context [_ <> true] => setoid_rewrite Bool.not_true_iff_false
+  | |- context [_ <> false] => setoid_rewrite Bool.not_false_iff_true
   end.
 
 (* Split up dependent pairs to get at proofs of properties *)
@@ -1135,7 +1183,7 @@ Qed.
    the variable is unused.  This is used so that we can use eauto with a low
    search bound that doesn't include the exists.  (Not terribly happy with
    how this works...) *)
-Ltac drop_exists :=
+Ltac drop_Z_exists :=
 repeat
   match goal with |- @ex Z ?p =>
    let a := eval hnf in (p 0) in
@@ -1152,10 +1200,14 @@ repeat
    clear xx
   end.
 *)
+(* For boolean solving we just use plain metavariables *)
+Ltac drop_bool_exists :=
+repeat match goal with |- @ex bool _ => eexists end.
 
 (* The linear solver doesn't like existentials. *)
 Ltac destruct_exists :=
-  repeat match goal with H:@ex Z _ |- _ => destruct H end.
+  repeat match goal with H:@ex Z _ |- _ => destruct H end;
+  repeat match goal with H:@ex bool _ |- _ => destruct H end.
 
 Ltac prepare_for_solver :=
 (*dump_context;*)
@@ -1169,6 +1221,7 @@ Ltac prepare_for_solver :=
  destruct_exists;
  unbool_comparisons;
  unbool_comparisons_goal;
+ repeat match goal with H:and _ _ |- _ => destruct H end;
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
  reduce_pow;
@@ -1202,6 +1255,27 @@ match goal with
 | _ => tauto
 end.
 
+Lemma or_iff_cong : forall A B C D, A <-> B -> C <-> D -> A \/ C <-> B \/ D.
+intros.
+tauto.
+Qed.
+
+Lemma and_iff_cong : forall A B C D, A <-> B -> C <-> D -> A /\ C <-> B /\ D.
+intros.
+tauto.
+Qed.
+
+Ltac solve_euclid :=
+repeat match goal with |- context [ZEuclid.modulo ?x ?y] =>
+  specialize (ZEuclid.div_mod x y);
+  specialize (ZEuclid.mod_always_pos x y);
+  generalize (ZEuclid.modulo x y);
+  generalize (ZEuclid.div x y);
+  intros
+end;
+nia.
+
+
 Ltac solve_arithfact :=
 (* Attempt a simple proof first to avoid lengthy preparation steps (especially
    as the large proof terms can upset subsequent proofs). *)
@@ -1209,30 +1283,42 @@ intros; (* To solve implications for derive_m *)
 try (exact trivial_range);
 try fill_in_evar_eq;
 try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end;
+(* Trying reflexivity will fill in more complex metavariable examples than
+   fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
+try (constructor; reflexivity);
 try (constructor; omega);
 prepare_for_solver;
 (*dump_context;*)
+constructor;
+repeat match goal with |- and _ _ => split end;
  solve
- [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
+ [ match goal with |- (?x _) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) _) end
  | apply ArithFact_mword; assumption
- | constructor; omega with Z
+ | omega with Z
    (* Try sail hints before dropping the existential *)
- | constructor; eauto 3 with zarith sail
+ | subst; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
- | constructor; drop_exists; eauto 3 with datatypes zarith sail
- | match goal with |- context [Z.mul] => constructor; nia end
+ | subst; drop_Z_exists; eauto 3 with datatypes zarith sail
+ | subst; match goal with |- context [ZEuclid.div] => solve_euclid
+                        | |- context [ZEuclid.modulo] => solve_euclid
+   end
+ | match goal with |- context [Z.mul] => nia end
    (* Booleans - and_boolMP *)
- | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => 
-     constructor; intros [|] [|] H1 H2;
+ | drop_bool_exists; solve [eauto using iff_refl, or_iff_cong, and_iff_cong | intuition]
+ | match goal with |- (forall l r:bool, _ -> _ -> exists _ : bool, _) => 
+     intros [|] [|] H1 H2;
      repeat match goal with H:?X = ?X -> _ |- _ => specialize (H eq_refl) end;
      repeat match goal with H:@ex _ _ |- _ => destruct H end;
      bruteforce_bool_exists
    end
+(* While firstorder was quite effective at dealing with existentially quantified
+   goals from boolean expressions, it attempts lazy normalization of terms,
+   which blows up on integer comparisons with large constants.
  | match goal with |- context [@eq bool _ _] =>
      (* Don't use auto for the fallback to keep runtime down *)
      firstorder fail
-   end
- | constructor; idtac "Unable to solve constraint"; dump_context; fail
+   end*)
+ | idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get
    slow running constraints into proof mode. *)
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 9e4010a0..5e20fc71 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -1,23 +1,12 @@
-/* Definitions for use with the -mono_rewrites option */
-
-/* External definitions not in the usual asl prelude */
-
-infix 6 <<
-
-val shiftleft = "shiftl" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
-
-overload operator << = {shiftleft}
-
-infix 6 >>
+$ifndef _MONO_REWRITES
+$define _MONO_REWRITES
 
-val shiftright = "shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+/* Definitions for use with the -mono_rewrites option */
 
-overload operator >> = {shiftright}
+$include <arith.sail>
+$include <vector_dec.sail>
 
-val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+/* External definitions not in the usual asl prelude */
 
 val extzv = "extz_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 
@@ -30,23 +19,18 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p
 
 /* Definitions for the rewrites */
 
-val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
-function slice_mask(n,i,l) =
-  let one : bits('n) = extzv(n, 0b1) in
-  ((one << l) - one) << i
-
 val is_zero_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
 function is_zero_subrange (xs, i, j) = {
-  (xs & slice_mask(j, i-j+1)) == extzv(0b0)
+  (xs & slice_mask(j, i-j+1)) == extzv([bitzero] : bits(1))
 }
 
 val is_zeros_slice : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
 function is_zeros_slice (xs, i, l) = {
-  (xs & slice_mask(i, l)) == extzv(0b0)
+  (xs & slice_mask(i, l)) == extzv([bitzero] : bits(1))
 }
 
 val is_ones_subrange : forall 'n, 'n >= 0.
@@ -69,17 +53,17 @@ val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
   (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
 
 function slice_slice_concat (r, xs, i, l, ys, i', l') = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  let ys = (ys & slice_mask(i',l')) >> i' in
-  extzv(r, xs) << l' | extzv(r, ys)
+  let xs = sail_shiftright(xs & slice_mask(i,l), i) in
+  let ys = sail_shiftright(ys & slice_mask(i',l'), i') in
+  sail_shiftleft(extzv(r, xs), l') | extzv(r, ys)
 }
 
 val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0.
   (bits('n), int, atom('p), atom('q)) -> bits('p + 'q) effect pure
 
 function slice_zeros_concat (xs, i, l, l') = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(l + l', xs) << l'
+  let xs = sail_shiftright(xs & slice_mask(i,l), i) in
+  sail_shiftleft(extzv(l + l', xs), l')
 }
 
 /* Assumes initial vectors are of equal size */
@@ -88,8 +72,8 @@ val subrange_subrange_eq : forall 'n, 'n >= 0.
   (bits('n), int, int, bits('n), int, int) -> bool effect pure
 
 function subrange_subrange_eq (xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j+1)) >> j in
-  let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
+  let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
+  let ys = sail_shiftright(ys & slice_mask(j',i'-j'+1), j') in
   xs == ys
 }
 
@@ -97,25 +81,25 @@ val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 &
   (implicit('s), bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
 
 function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j+1)) >> j in
-  let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
-  extzv(s, xs) << (i' - j' + 1) | extzv(s, ys)
+  let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
+  let ys = sail_shiftright(ys & slice_mask(j',i'-j'+1), j) in
+  sail_shiftleft(extzv(s, xs), i' - j' + 1) | extzv(s, ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
 function place_subrange(m,xs,i,j,shift) = {
-  let xs = (xs & slice_mask(j,i-j+1)) >> j in
-  extzv(m, xs) << shift
+  let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
+  sail_shiftleft(extzv(m, xs), shift)
 }
 
 val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
 function place_slice(m,xs,i,l,shift) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(m, xs) << shift
+  let xs = sail_shiftright(xs & slice_mask(i,l), i) in
+  sail_shiftleft(extzv(m, xs), shift)
 }
 
 val set_slice_zeros : forall 'n, 'n >= 0.
@@ -123,14 +107,14 @@ val set_slice_zeros : forall 'n, 'n >= 0.
 
 function set_slice_zeros(n, xs, i, l) = {
   let ys : bits('n) = slice_mask(n, i, l) in
-  xs & ~(ys)
+  xs & not_vec(ys)
 }
 
 val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
 function zext_slice(m,xs,i,l) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
+  let xs = sail_shiftright(xs & slice_mask(i,l), i) in
   extzv(m, xs)
 }
 
@@ -138,7 +122,7 @@ val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
 function sext_slice(m,xs,i,l) = {
-  let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in
+  let xs = sail_arith_shiftright(sail_shiftleft((xs & slice_mask(i,l)), ('n - i - l)), 'n - l) in
   extsv(m, xs)
 }
 
@@ -146,7 +130,7 @@ val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
 function place_slice_signed(m,xs,i,l,shift) = {
-  sext_slice(m, xs, i, l) << shift
+  sail_shiftleft(sext_slice(m, xs, i, l), shift)
 }
 
 /* This has different names in the aarch64 prelude (UInt) and the other
@@ -157,28 +141,46 @@ val _builtin_unsigned = {
   lem: "uint",
   interpreter: "uint",
   c: "sail_uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+} : forall 'n. bits('n) -> {'m, 0 <= 'm < 2 ^ 'n. int('m)}
+
+/* There are different implementation choices for division and remainder, but
+   they agree on positive values.  We use this here to give more precise return
+   types for unsigned_slice and unsigned_subrange. */
 
-val unsigned_slice : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> int effect pure
+val _builtin_mod_nat = {
+  smt: "mod",
+  ocaml: "modulus",
+  lem: "integerMod",
+  c: "tmod_int",
+  coq: "Z.rem"
+} : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m)) -> {'r, 0 <= 'r < 'm. int('r)}
+
+/* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return
+   type of pow2, as SMT solvers tend to have problems with exponentiation. */
+val _builtin_pow2 = "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}
+
+val unsigned_slice : forall 'n 'l, 'n >= 0 & 'l >= 0.
+  (bits('n), int, int('l)) -> {'m, 0 <= 'm < 2 ^ 'l. int('m)} effect pure
 
 function unsigned_slice(xs,i,l) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  _builtin_unsigned(xs)
+  let xs = sail_shiftright(xs & slice_mask(i,l), i) in
+  _builtin_mod_nat(_builtin_unsigned(xs), _builtin_pow2(l))
 }
 
-val unsigned_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> int effect pure
+val unsigned_subrange : forall 'n 'i 'j, 'n >= 0 & ('i - 'j) >= 0.
+  (bits('n), int('i), int('j)) -> {'m, 0 <= 'm < 2 ^ ('i - 'j + 1). int('m)} effect pure
 
 function unsigned_subrange(xs,i,j) = {
-  let xs = (xs & slice_mask(j,i-j+1)) >> i in
-  _builtin_unsigned(xs)
+  let xs = sail_shiftright(xs & slice_mask(j,i-j+1), i) in
+  _builtin_mod_nat(_builtin_unsigned(xs), _builtin_pow2(i - j + 1))
 }
 
 
 val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n) effect pure
 
 function zext_ones(n, m) = {
-  let v : bits('n) = extsv(0b1) in
-  v >> (n - m)
+  let v : bits('n) = extsv([bitone] : bits(1)) in
+  sail_shiftright(v, n - m)
 }
+
+$endif
diff --git a/lib/sail.c b/lib/sail.c
index 6c71d7ae..2d47939e 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -350,6 +350,27 @@ void mult_int(sail_int *rop, const sail_int op1, const sail_int op2)
   mpz_mul(*rop, op1, op2);
 }
 
+
+inline
+void ediv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  /* GMP doesn't have Euclidean division but we can emulate it using 
+     flooring and ceiling division. */
+  if (mpz_sgn(op2) >= 0) {
+    mpz_fdiv_q(*rop, op1, op2);
+  } else {
+    mpz_cdiv_q(*rop, op1, op2);
+  }
+}
+
+inline
+void emod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  /* The documentation isn't that explicit but I think this is 
+     Euclidean mod. */
+  mpz_mod(*rop, op1, op2);
+}
+
 inline
 void tdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
diff --git a/lib/sail.h b/lib/sail.h
index e06629f0..1c368d2d 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -138,6 +138,8 @@ SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(ediv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(emod_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int);
diff --git a/lib/smt.sail b/lib/smt.sail
index d886c127..4d250bef 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -3,24 +3,21 @@ $define _SMT
 
 // see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
 
-val div = {
+/*! Euclidean division */
+val ediv_int = {
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "tdiv_int",
+  c: "ediv_int",
   coq: "ediv_with_eq"
 } : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
-overload operator / = {div}
-
-val mod = {
+val emod_int = {
   ocaml: "modulus",
   lem: "integerMod",
-  c: "tmod_int",
+  c: "emod_int",
   coq: "emod_with_eq"
 } : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
-overload operator % = {mod}
-
 val abs_int = {
   ocaml: "abs_int",
   lem: "abs_int",
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index f31e4ed2..b4014aa6 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -15,6 +15,16 @@ val eq_bits = {
 
 overload operator == = {eq_bit, eq_bits}
 
+val neq_bits = {
+  lem: "neq_vec",
+  c: "neq_bits",
+  coq: "neq_vec"
+} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+
+function neq_bits(x, y) = not_bool(eq_bits(x, y))
+
+overload operator != = {neq_bits}
+
 val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n)
 
 val vector_length = {
@@ -27,8 +37,6 @@ val vector_length = {
 
 overload length = {bitvector_length, vector_length}
 
-val sail_zeros = "zeros" : forall 'n. atom('n) -> bits('n)
-
 val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "prerr_bits" : forall 'n. (string, bits('n)) -> unit
@@ -126,6 +134,23 @@ val add_bits_int = {
 
 overload operator + = {add_bits, add_bits_int}
 
+val sub_bits = {
+  ocaml: "sub_vec",
+  lem: "sub_vec",
+  c: "sub_bits",
+  coq: "sub_vec"
+} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
+
+val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator & = {and_vec}
+
+val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator | = {or_vec}
+
 val vector_subrange = {
   ocaml: "subrange",
   interpreter: "subrange",
@@ -143,8 +168,37 @@ val vector_update_subrange = {
   coq: "update_subrange_vec_dec"
 } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
+val sail_shiftleft = "shiftl" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+val sail_shiftright = "shiftr" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+val sail_arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+val sail_zeros = "zeros" : forall 'n, 'n >= 0. atom('n) -> bits('n)
+
+val sail_ones : forall 'n, 'n >= 0. atom('n) -> bits('n)
+
+function sail_ones(n) = not_vec(sail_zeros(n))
+
 // Some ARM specific builtins
 
+val slice = "slice" : forall 'n 'm 'o, 0 <= 'm & 0 <= 'n.
+  (bits('m), atom('o), atom('n)) -> bits('n)
+
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+
+val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
+function slice_mask(n,i,l) =
+  if l >= n then {
+    sail_ones(n)
+  } else {
+    let one : bits('n) = sail_mask(n, [bitone] : bits(1)) in
+    sail_shiftleft(sub_bits(sail_shiftleft(one, l), one), i)
+  }
+
 val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
 
 val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
@@ -152,11 +206,6 @@ val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w))
 val set_slice_bits = "set_slice" : forall 'n 'm.
   (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
 
-val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n.
-  (bits('m), atom('o), atom('n)) -> bits('n)
-
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-
 /*!
 converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
  */