Coq: update prompt monad to match the Lem, and port the state monad/lifting

NB: requires minor changes in the models

7 files changed, 627 insertions, 323 deletions

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_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 7edc8843..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
@@ -457,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