Merge branch 'sail2' into rmem_interpreter

6 files changed, 342 insertions, 152 deletions

diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index e01cc051..3cde7ade 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -38,6 +38,11 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
+let genlistM f n =
+  let indices = genlist (fun n -> n) n in
+  foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
+
 val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
 let and_boolM l r = l >>= (fun l -> if l then r else return false)
 
@@ -55,7 +60,7 @@ val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_nondet = function
   | B0 -> return false
   | B1 -> return true
-  | BU -> undefined_bool ()
+  | BU -> choose_bool "bool_of_bitU"
 end
 
 val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
@@ -93,16 +98,25 @@ let rec untilM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then return vars else untilM vars cond body
 
-val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
-let internal_pick xs =
-  (* Use sufficiently many undefined bits and convert into an index into the list *)
-  bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
+let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
+
+val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
+let choose descr xs =
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_bools descr (List.length xs) >>= fun bs ->
   let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
   match index xs idx with
     | Just x -> return x
-    | Nothing -> Fail "internal_pick"
+    | Nothing -> Fail ("choose " ^ descr)
   end
 
+declare {isabelle} rename function choose = chooseM
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = choose "internal_pick" xs
+
 (*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 78b1615e..e0ac09f6 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -8,19 +8,20 @@ type address = list bitU
 
 type monad 'regval 'a 'e =
   | Done of 'a
-  (* Read a number of bytes from memory, returned in little endian order *)
-  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
-  (* Read the tag of a memory address *)
-  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
-  (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of write_kind * address * nat * 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 of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e)
+  | Read_memt of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+  (* Tell the system a write is imminent, at the given address and with the
+     given size. *)
+  | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> 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 of list memory_byte * (bool -> monad 'regval 'a 'e)
-  (* Request to write the tag at given address. *)
-  | Write_tag of address * bitU * (bool -> 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 of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e)
+  | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -29,8 +30,10 @@ type monad 'regval 'a 'e =
   | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
   (* Request to write register *)
   | Write_reg of register_name * 'regval * monad 'regval 'a 'e
-  (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
-  | Undefined of (bool -> monad 'regval 'a 'e)
+  (* 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 of string * (bool -> monad 'regval 'a 'e)
   (* Print debugging or tracing information *)
   | Print of string * monad 'regval 'a 'e
   (*Result of a failed assert with possible error message to report*)
@@ -38,33 +41,52 @@ type monad 'regval 'a 'e =
   (* Exception of type 'e *)
   | Exception of 'e
 
+type event 'regval =
+  | E_read_mem of read_kind * nat * nat * list memory_byte
+  | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * nat * nat * list memory_byte * bool
+  | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
+  | E_write_ea of write_kind * nat * nat
+  | E_excl_res of bool
+  | E_barrier of barrier_kind
+  | E_footprint
+  | E_read_reg of register_name * 'regval
+  | E_write_reg of register_name * 'regval
+  | E_choose of string * bool
+  | E_print of string
+
+type trace 'regval = list (event 'regval)
+
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
 val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
 let rec bind m f = 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)
-  | Print msg k ->        Print msg        (bind k f)
-  | Fail descr ->         Fail 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
 
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
 let exit () = Fail "exit"
 
+val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e
+let choose_bool descr = Choose descr return
+
 val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = Undefined return
+let undefined_bool () = choose_bool "undefined_bool"
 
 val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
 let assert_exp exp msg = if exp then Done () else Fail msg
@@ -74,21 +96,21 @@ let throw e = Exception e
 
 val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
 let rec try_catch m h = 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)
-  | Print msg k ->        Print msg        (try_catch k h)
-  | Fail descr ->         Fail 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
@@ -126,19 +148,37 @@ let maybe_fail msg = function
   | Nothing -> 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
+let read_memt_bytes rk addr sz =
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Read_memt rk addr (nat_of_int sz) return)
+
+val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
+let read_memt rk addr sz =
+  bind
+    (read_memt_bytes rk addr sz)
+    (fun (bytes, tag) ->
+       match of_bits (bits_of_mem_bytes bytes) with
+         | Just v -> return (v, tag)
+         | Nothing -> 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
 let read_mem_bytes rk addr sz =
-  Read_mem rk (bits_of addr) (nat_of_int sz) return
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Read_mem rk addr (nat_of_int sz) return)
 
 val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
 let read_mem rk addr sz =
   bind
     (read_mem_bytes rk addr sz)
     (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
-let read_tag addr = Read_tag (bits_of addr) return
+       match of_bits (bits_of_mem_bytes bytes) with
+         | Just v -> return v
+         | Nothing -> Fail "bits_of_mem_bytes"
+       end)
 
 val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
@@ -146,16 +186,28 @@ let excl_result () =
   Excl_res k
 
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
-
-val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match mem_bytes_of_bits v with
-  | Just v -> Write_memv v return
-  | Nothing -> Fail "write_mem_val"
-end
-
-val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
-let write_tag addr b = Write_tag (bits_of addr) b return
+let write_mem_ea wk addr sz =
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
+
+val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr sz v =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_mem wk addr (nat_of_int sz) v return
+    | _ -> 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
+let write_memt wk addr sz v tag =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_memt wk addr (nat_of_int sz) v tag return
+    | _ -> Fail "write_mem"
+  end
 
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
@@ -214,6 +266,68 @@ let barrier bk = Barrier bk (Done ())
 val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
 let footprint _ = Footprint (Done ())
 
+(* Event traces *)
+
+val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)
+let emitEvent m e = match (e, m) with
+  | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing
+  | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
+  | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
+  | (E_read_reg r v, Read_reg r' k) ->
+     if r' = r then Just (k v) else Nothing
+  | (E_write_reg r v, Write_reg r' v' k) ->
+     if r' = r && v' = v then Just k else Nothing
+  | (E_write_ea wk a sz, Write_ea wk' a' sz' k) ->
+     if wk' = wk && a' = a && sz' = sz then Just k else Nothing
+  | (E_barrier bk, Barrier bk' k) ->
+     if bk' = bk then Just k else Nothing
+  | (E_print m, Print m' k) ->
+     if m' = m then Just k else Nothing
+  | (E_excl_res v, Excl_res k) -> Just (k v)
+  | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
+  | (E_footprint, Footprint k) -> Just k
+  | _ -> Nothing
+end
+
+val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)
+let rec runTrace t m = match t with
+  | [] -> Just m
+  | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
+end
+
+declare {isabelle} termination_argument runTrace = automatic
+
+val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
+let final = function
+  | Done _ -> true
+  | Fail _ -> true
+  | Exception _ -> true
+  | _ -> false
+end
+
+val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasTrace t m = match runTrace t m with
+  | Just m -> final m
+  | Nothing -> false
+end
+
+val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasException t m = match runTrace t m with
+  | Just (Exception _) -> true
+  | _ -> false
+end
+
+val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasFailure t m = match runTrace t m with
+  | Just (Fail _) -> true
+  | _ -> false
+end
+
 (* Define a type synonym that also takes the register state as a type parameter,
    in order to make switching to the state monad without changing generated
    definitions easier, see also lib/hol/prompt_monad.lem. *)
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index f703dead..ec787764 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -28,6 +28,11 @@ end
 
 declare {isabelle} termination_argument foreachS = automatic
 
+val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e
+let genlistS f n =
+  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
 let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
 
@@ -84,12 +89,17 @@ 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
+let choose_boolsS n = genlistS (fun _ -> choose_boolS ()) 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 undefined bits and convert into an index into the list *)
-  bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+  (* 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 "internal_pick"
+    | Nothing -> failS "choose internal_pick"
   end
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 039343e2..98a5390d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -5,23 +5,53 @@ open import Sail2_prompt
 open import Sail2_state_monad
 open import {isabelle} `Sail2_state_monad_lemmas`
 
-(* State monad wrapper around prompt monad *)
-
+(* 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
-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_tag a t k)    -> bindS (write_tagS a 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
-  | (Print _ k)          -> liftState ra k (* TODO *)
-  | (Fail descr)         -> failS descr
-  | (Exception e)        -> throwS e
+let rec liftState ra m = 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 ())               (fun v -> liftState ra (k v))
+  | (Choose _ k)               -> bindS (choose_boolS ())               (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
+
+val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let emitEventS ra e s = match e with
+  | E_read_mem _ addr sz v ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
+     if v' = v then Just s else Nothing)
+  | E_read_memt _ addr sz (v, tag) ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
+     if v' = v && tag' = tag then Just s else Nothing)
+  | E_write_mem _ addr sz v success ->
+     if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
+  | E_write_memt _ addr sz v tag success ->
+     if success then Just (put_mem_bytes addr sz v tag s) else Nothing
+  | E_read_reg r v ->
+     let (read_reg, _) = ra in
+     Maybe.bind (read_reg r s.regstate) (fun v' ->
+     if v' = v then Just s else Nothing)
+  | E_write_reg r v ->
+     let (_, write_reg) = ra in
+     Maybe.bind (write_reg r v s.regstate) (fun rs' ->
+     Just <| s with regstate = rs' |>)
+  | _ -> Just s
 end
+
+val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let rec runTraceS ra t s = match t with
+  | [] -> Just s
+  | e :: t' -> Maybe.bind (emitEventS ra e s) (runTraceS ra t')
+end
+
+declare {isabelle} termination_argument runTraceS = automatic
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 30b296cc..3042700c 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -4,24 +4,20 @@ open import Sail2_values
 
 (* 'a is result type *)
 
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
+type memstate = map nat memory_byte
+type tagstate = map nat 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 |>
+     tagstate : tagstate |>
 
 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 |>
+     tagstate = Map.empty |>
 
 type ex 'e =
   | Failure of string
@@ -51,8 +47,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n)
 let inline (>>$=) = bindS
 let inline (>>$) = seqS
 
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
+val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = Set.fromList (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)
@@ -63,8 +59,9 @@ 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 undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () = chooseS {false; true}
+val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
+let choose_boolS () = chooseS [false; true]
+let undefined_boolS = choose_boolS
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"
@@ -120,69 +117,78 @@ end
 
 val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
 let read_tagS addr =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  maybe_failS "nat_of_bv" (nat_of_bv addr) >>$= (fun addr ->
   readS (fun s -> fromMaybe B0 (Map.lookup 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 =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
+val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
+let get_mem_bytes addr sz s =
+  let addrs = genlist (fun n -> addr + n) sz 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))
+  let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
+  Maybe.map
+    (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
+    (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
+let read_memt_bytesS _ addr sz =
+  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
+let read_mem_bytesS rk addr sz =
+  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
+let read_memtS rk a sz =
+  maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
+  read_memt_bytesS rk a (nat_of_int 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
 let read_memS rk a sz =
-  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes ->
-  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
+  read_memtS rk a sz >>$= (fun (bytes, _) ->
+  returnS 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 =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-  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 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
-let write_tagS addr t =
-   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-   updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-   returnS true)
+let excl_resultS =
+  (* 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
+
+(* 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
+let put_mem_bytes addr sz v tag s =
+  let addrs = genlist (fun n -> addr + n) sz in
+  let a_v = List.zip addrs v in
+  let write_byte mem (addr, v) = Map.insert addr v mem in
+  let write_tag mem addr = Map.insert addr tag mem in
+  <| s with memstate = List.foldl write_byte s.memstate a_v;
+            tagstate = List.foldl write_tag s.tagstate addrs |>
+
+val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_memt_bytesS _ addr sz v t =
+  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
+let write_mem_bytesS wk addr sz v = 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
+let write_memtS wk addr sz v t =
+  match (nat_of_bv addr, mem_bytes_of_bits v) with
+    | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int 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
+let write_memS wk addr sz v = write_memtS wk addr sz v B0
 
 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)
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 8957f0dd..5e6537a8 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -47,7 +47,11 @@ let power_real b e = realPowInteger b e*)
 
 val print_endline : string -> unit
 let print_endline _ = ()
-(* declare ocaml target_rep function print_endline = `print_endline` *)
+declare ocaml target_rep function print_endline = `print_endline`
+
+val print : string -> unit
+let print _ = ()
+declare ocaml target_rep function print = `print_string`
 
 val prerr_endline : string -> unit
 let prerr_endline _ = ()
@@ -625,9 +629,21 @@ let extz_bv n v = extz_bits n (bits_of v)
 val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
 let exts_bv n v = exts_bits n (bits_of v)
 
+val nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat
+let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
+
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
 
+val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+let print_bits str v = print_endline (str ^ string_of_bv v)
+
+val dec_str : integer -> string
+let dec_str bv = show bv
+
+val concat_str : string -> string -> string
+let concat_str str1 str2 = str1 ^ str2
+
 val int_of_bit : bitU -> integer
 let int_of_bit b =
   match b with