8 files changed, 237 insertions, 193 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index d398ab52..756bb699 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,24 +1,24 @@
 open import Pervasives_extra
-open import Sail_impl_base
+(*open import Sail_impl_base*)
 open import Sail_values
 open import Prompt_monad
 open import {isabelle} `Prompt_monad_extras`
 
-val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
+val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let rec iter_aux i f xs = match xs with
   | x :: xs -> f i x >> iter_aux (i + 1) f xs
   | [] -> return ()
   end
 
-val iteri : forall 'a 'e. (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
+val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iteri f xs = iter_aux 0 f xs
 
-val iter : forall 'a 'e. ('a -> M unit 'e) -> list 'a -> M unit 'e
+val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iter f xs = iteri (fun _ x -> f x) xs
 
 
-val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
+val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec foreachM_inc (i,stop,by) vars body =
   if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then
@@ -27,8 +27,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
+val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec foreachM_dec (i,stop,by) vars body =
   if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then
@@ -40,21 +40,21 @@ val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'va
 let rec while_PP vars cond body =
   if cond vars then while_PP (body vars) cond body else vars
 
-val while_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec while_PM vars cond body =
   if cond vars then
     body vars >>= fun vars -> while_PM vars cond body
   else return vars
 
-val while_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> 'vars) -> M 'vars 'e
+val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> 'vars) -> monad 'rv 'vars 'e
 let rec while_MP vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then while_MP (body vars) cond body else return vars
 
-val while_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec while_MM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then
@@ -66,21 +66,21 @@ let rec until_PP vars cond body =
   let vars = body vars in
   if (cond vars) then vars else until_PP (body vars) cond body
 
-val until_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec until_PM vars cond body =
   body vars >>= fun vars ->
   if (cond vars) then return vars else until_PM vars cond body
 
-val until_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> 'vars) -> M 'vars 'e
+val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> 'vars) -> monad 'rv 'vars 'e
 let rec until_MP vars cond body =
   let vars = body vars in
   cond vars >>= fun cond_val ->
   if cond_val then return vars else until_MP vars cond body
 
-val until_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec until_MM vars cond body =
   body vars >>= fun vars ->
   cond vars >>= fun cond_val ->
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 45733caa..ff5e3726 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -1,70 +1,88 @@
 open import Pervasives_extra
-open import Sail_impl_base
+(*open import Sail_impl_base*)
+open import Sail_instr_kinds
 open import Sail_values
 
-type M 'a 'e = outcome 'a 'e
-
-val return : forall 'a 'e. 'a -> M 'a 'e
+type register_name = string
+
+type monad 'regval 'a 'e =
+  | Done of 'a
+  | Read_mem of read_kind * integer * integer * (list memory_byte -> monad 'regval 'a 'e)
+  (* Tell the system a write is imminent, at address lifted, of size nat *)
+  | Write_ea of write_kind * integer * integer * 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 *)
+  | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
+  (* Request a memory barrier *)
+  | Barrier of barrier_kind * monad 'regval 'a 'e
+  (* Request to read register, will track dependency when mode.track_values *)
+  | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
+  (* Request to write register *)
+  | Write_reg of register_name * 'regval * monad 'regval 'a 'e
+  (*Result of a failed assert with possible error message to report*)
+  | Fail of string
+  | Error of string
+  (* Exception of type 'e *)
+  | Exception of 'e
+  (* TODO: Reading/writing tags *)
+
+val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
-val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e
+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 descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (bind o f,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (bind o f,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         Exception e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
+  | Done a -> f a
+  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
+  | Write_memv descr k -> Write_memv descr (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)
+  | Write_ea wk a sz k -> Write_ea wk a sz (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
 end
 
 let inline (>>=) = bind
-val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e
+val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
 let inline (>>) m n = m >>= fun (_ : unit) -> n
 
-val exit : forall 'a 'e. unit -> M 'a 'e
-let exit () = Fail Nothing
+val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
+let exit () = Fail "exit"
 
-val assert_exp : forall 'e. bool -> string -> M unit 'e
-let assert_exp exp msg = if exp then Done () else Fail (Just msg)
+val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
+let assert_exp exp msg = if exp then Done () else Fail msg
 
-val throw : forall 'a 'e. 'e -> M 'a 'e
+val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e
 let throw e = Exception e
 
-val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) ->  M 'a 'e2
+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 descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (try_catch o h,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (try_catch o h,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (try_catch o h,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (try_catch o h,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         h e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (try_catch o h ,opt))
+  | Done a ->             Done a
+  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
+  | Write_memv descr k -> Write_memv descr (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)
+  | Write_ea wk a sz k -> Write_ea wk a sz (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
 end
 
 (* 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 MR 'a 'r 'e = M 'a (either 'r 'e)
+type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e)
 
-val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e
+val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e
 let early_return r = throw (Left r)
 
-val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e
+val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e
 let catch_early_return m =
   try_catch m
     (function
@@ -73,11 +91,11 @@ let catch_early_return m =
      end)
 
 (* Lift to monad with early return by wrapping exceptions *)
-val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e
+val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e
 let liftR m = try_catch m (fun e -> throw (Right e))
 
 (* Catch exceptions in the presence of early returns *)
-val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) ->  MR 'a 'r 'e2
+val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) ->  monadR 'rv 'a 'r 'e2
 let try_catchR m h =
   try_catch m
     (function
@@ -86,59 +104,62 @@ let try_catchR m h =
      end)
 
 
-val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e
+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 =
-  let addr = address_lifted_of_bitv (bits_of addr) in
-  let sz = natFromInteger sz in
-  let k memory_value =
-    let bitv = of_bits (internal_mem_value memory_value) in
-    (Done bitv,Nothing) in
-  Read_mem (rk,addr,sz) k
-
-val excl_result : forall 'e. unit -> M bool 'e
+  let addr = unsigned addr in
+  let k bytes =
+    let bitv = bits_of_bytes (List.reverse bytes) in
+    (Done bitv) in
+  Read_mem rk addr sz k
+
+val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
-  let k successful = (return successful,Nothing) in
+  let k successful = (return successful) in
   Excl_res k
 
-val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e
-let write_mem_ea wk addr sz =
-  let addr = address_lifted_of_bitv (bits_of addr) in
-  let sz = natFromInteger sz in
-  Write_ea (wk,addr,sz) (Done (),Nothing)
-
-val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e
-let write_mem_val v =
-  let v = external_mem_value (bits_of v) in
-  let k successful = (return successful,Nothing) in
-  Write_memv v k
-
-val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e
-let read_reg_aux reg =
-  let k reg_value =
-    let v = of_bits (internal_reg_value reg_value) in
-    (Done v,Nothing) in
-  Read_reg reg 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 (unsigned addr) sz (Done ())
 
+val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
+let write_mem_val v = match bytes_of_bits v with
+  | Just v ->
+     let k successful = (return successful) in
+     Write_memv (List.reverse v) k
+  | Nothing -> fail "write_mem_val"
+end
+
+val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
-  read_reg_aux (external_reg_whole reg)
+  let k v =
+    match reg.of_regval v with
+      | Just v -> Done v
+      | Nothing -> Error "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
 let read_reg_range reg i j =
-  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
+  read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
+
 let read_reg_bit reg i =
-  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
+  read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
   return (extract_only_element v)
+
 let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield.field_name)
+  read_reg_aux (external_reg_field_whole reg regfield)
+
 let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
-  return (extract_only_element v)
+  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
+  return (extract_only_element v)*)
 
 let reg_deref = read_reg
 
-val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e
-let write_reg_aux reg_name v =
-  let regval = external_reg_value reg_name (bits_of v) in
-  Write_reg (reg_name,regval) (Done (), Nothing)
+val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e
+let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())
 
+(* TODO
 let write_reg reg v =
   write_reg_aux (external_reg_whole reg) v
 let write_reg_range reg i j v =
@@ -149,20 +170,17 @@ let write_reg_pos reg i 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
-(*let 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))*)
+                (Vector [bit] 0 (is_inc_of_reg reg))
 let 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
 let write_reg_field_pos reg regfield i v =
   write_reg_field_range reg regfield i i [v]
-let write_reg_field_bit = write_reg_field_pos
-
-let write_reg_ref (reg, v) = write_reg reg v
-
-val barrier : forall 'e. barrier_kind -> M unit 'e
-let barrier bk = Barrier bk (Done (), Nothing)
+let write_reg_field_bit = write_reg_field_pos*)
 
+val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
+let barrier bk = Barrier bk (Done ())
 
-val footprint : forall 'e. M unit 'e
-let footprint = Footprint (Done (),Nothing)
+(*val footprint : forall 'rv 'e. monad 'rv unit 'e
+let footprint = Footprint (Done ())*)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index ada91bd0..7d6b156b 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -1,6 +1,5 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_impl_base
 open import Sail_values
 
 (*** Bit vector operations *)
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index d2a2aea1..5658dc21 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -1,6 +1,5 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_impl_base
 open import Sail_values
 open import Sail_operators
 
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index bd7ef2b4..fcc3153b 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -1,6 +1,5 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_impl_base
 open import Sail_values
 open import Sail_operators
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4cbcc269..34e4bd98 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -2,7 +2,7 @@
 
 open import Pervasives_extra
 open import Machine_word
-open import Sail_impl_base
+(*open import Sail_impl_base*)
 
 
 type ii = integer
@@ -57,6 +57,7 @@ val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
   if n <= 0 then []
   else xs ++ repeat xs (n-1)
+declare {isabelle} termination_argument repeat = automatic
 
 let duplicate_to_list bit length = repeat [bit] length
 
@@ -66,6 +67,7 @@ let rec replace bs (n : integer) b' = match bs with
      if n = 0 then b' :: bs
               else b :: replace bs (n - 1) b'
   end
+declare {isabelle} termination_argument replace = automatic
 
 let upper n = n
 
@@ -135,7 +137,7 @@ end
 
 let cast_bit_bool = bool_of_bitU
 
-let bit_lifted_of_bitU = function
+(*let bit_lifted_of_bitU = function
   | B0 -> Bitl_zero
   | B1 -> Bitl_one
   | BU -> Bitl_undef
@@ -157,7 +159,7 @@ let bitU_of_bit_lifted = function
   | Bitl_one  -> B1
   | Bitl_undef -> BU
   | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
-  end
+  end*)
 
 let not_bit = function
   | B1 -> B0
@@ -200,6 +202,7 @@ val bits_of_nat_aux : natural -> list bitU
 let rec bits_of_nat_aux x =
   if x = 0 then []
   else (if x mod 2 = 1 then B1 else B0) :: bits_of_nat_aux (x / 2)
+declare {isabelle} termination_argument bits_of_nat_aux = automatic
 let bits_of_nat n = List.reverse (bits_of_nat_aux n)
 
 val nat_of_bits : list bitU -> natural
@@ -239,6 +242,7 @@ let signed_of_bits bits =
 val pad_bitlist : bitU -> list bitU -> integer -> list bitU
 let rec pad_bitlist b bits n =
   if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1)
+declare {isabelle} termination_argument pad_bitlist = automatic
 
 let ext_bits pad len bits =
   let longer = len - (integerFromNat (List.length bits)) in
@@ -259,6 +263,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with
   | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
   | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
 end
+declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic
 
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
@@ -300,6 +305,7 @@ let rec hexstring_of_bits bs = match bs with
      end
   | _ -> Nothing
   end
+declare {isabelle} termination_argument hexstring_of_bits = automatic
 
 let show_bitlist bs =
   match hexstring_of_bits bs with
@@ -370,6 +376,21 @@ let extract_only_element = function
   | _ -> failwith "extract_only_element called for list with more elements"
 end
 
+(* just_list takes a list of maybes and returns Just xs if all elements have
+   a value, and Nothing if one of the elements is Nothing. *)
+val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
+let rec just_list [] = Just []
+and just_list (x :: xs) =
+  match (x, just_list xs) with
+    | (Just x, Just xs) -> Just (x :: xs)
+    | (_, _) -> Nothing
+  end
+declare {isabelle} termination_argument just_list = automatic
+
+lemma just_list_spec:
+  ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
+   (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es)))
+
 (*** Machine words *)
 
 val length_mword : forall 'a. mword 'a -> integer
@@ -503,14 +524,24 @@ let string_of_bv v = show_bitlist (bits_of v)
 
 (*** Bytes and addresses *)
 
-val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
-let rec byte_chunks n list = match (n,list) with
-  | (0,_) -> []
-  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
-  | _ -> failwith "byte_chunks not given enough bits"
+type memory_byte = list bitU
+
+val byte_chunks : forall 'a. list 'a -> maybe (list (list 'a))
+let rec byte_chunks bs = match bs with
+  | [] -> Just []
+  | a::b::c::d::e::f::g::h::rest ->
+     Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest))
+  | _ -> Nothing
 end
+declare {isabelle} termination_argument byte_chunks = automatic
+
+val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)
+let bytes_of_bits bs = byte_chunks (bits_of bs)
 
-val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
+val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a
+let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs))
+
+(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
 let bitv_of_byte_lifteds v =
   foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v
 
@@ -545,10 +576,13 @@ let address_lifted_of_bitv v =
     end in
   Address_lifted byte_lifteds maybe_address_integer
 
+val bitv_of_address_lifted : address_lifted -> list bitU
+let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs
+
 val address_of_bitv : list bitU -> address
 let address_of_bitv v =
   let bytes = bytes_of_bitv v in
-  address_of_byte_list bytes
+  address_of_byte_list bytes*)
 
 let rec reverse_endianness_list bits =
   if List.length bits <= 8 then bits else
@@ -560,7 +594,7 @@ let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v))
 
 (*** Registers *)
 
-type register_field = string
+(*type register_field = string
 type register_field_index = string * (integer * integer) (* name, start and end *)
 
 type register =
@@ -570,14 +604,19 @@ type register =
                 bool * (* is increasing *)
                   list register_field_index
   | UndefinedRegister of integer (* length *)
-  | RegisterPair of register * register
+  | RegisterPair of register * register*)
 
-type register_ref 'regstate 'a =
-  <| reg_name : string;
-     reg_start : integer;
-     reg_is_inc : bool;
+type register_ref 'regstate 'regval 'a =
+  <| name : string;
+     is_inc : bool;
      read_from : 'regstate -> 'a;
-     write_to : 'regstate -> 'a -> 'regstate |>
+     write_to : 'regstate -> 'a -> 'regstate;
+     of_regval : 'regval -> maybe 'a;
+     regval_of : 'a -> 'regval |>
+
+type register_accessors 'regstate 'regval =
+  ((string -> 'regstate -> maybe 'regval) *
+   (string -> 'regval -> 'regstate -> maybe 'regstate))
 
 type field_ref 'regtype 'a =
   <| field_name : string;
@@ -586,7 +625,7 @@ type field_ref 'regtype 'a =
      get_field : 'regtype -> 'a;
      set_field : 'regtype -> 'a -> 'regtype |>
 
-let name_of_reg = function
+(*let name_of_reg = function
   | Register name _ _ _ _ -> name
   | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
   | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
@@ -597,7 +636,7 @@ let size_of_reg = function
   | UndefinedRegister size -> size
   | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
 end
-                              
+
 let start_of_reg = function
   | Register _ _ start _ _ -> start
   | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
@@ -638,11 +677,11 @@ let register_field_indices register rfield =
 
 let register_field_indices_nat reg regfield=
   let (i,j) = register_field_indices reg regfield in
-  (natFromInteger i,natFromInteger j)
+  (natFromInteger i,natFromInteger j)*)
 
-let rec external_reg_value reg_name v = 
+(*let rec external_reg_value reg_name v =
   let (internal_start, external_start, direction) =
-    match reg_name with 
+    match reg_name with
      | Reg _ start size dir ->
         (start, (if dir = D_increasing then start else (start - (size +1))), dir)
      | Reg_slice _ reg_start dir (slice_start, _) ->
@@ -653,10 +692,10 @@ let rec external_reg_value reg_name v =
          slice_start, dir)
      | Reg_f_slice _ reg_start dir _ _ (slice_start, _) ->
         ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir) 
+         slice_start, dir)
      end in
   let bits = bit_lifteds_of_bitv v in
-  <| rv_bits           = bits; 
+  <| rv_bits           = bits;
      rv_dir            = direction;
      rv_start          = external_start;
      rv_start_internal = internal_start |>
@@ -672,42 +711,45 @@ let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
   (*This is the case the thread/concurrecny model expects, so no change needed*)
   | D_increasing -> (i,j)
-  | D_decreasing -> let slice_i = start - i in 
+  | D_decreasing -> let slice_i = start - i in
                     let slice_j = (i - j) + slice_i in
                     (slice_i,slice_j)
-  end 
+  end *)
 
-let external_reg_whole reg =
-  Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg)
-      
-let external_reg_slice reg (i,j) =
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j))
+(* TODO
+let external_reg_whole r =
+  Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc)
+
+let external_reg_slice r (i,j) =
+  let start = natFromInteger r.start in
+  let dir = dir_of_bool r.is_inc in
+  Reg_slice (r.name) start dir (external_slice dir start (i,j))
 
-let external_reg_field_whole reg rfield = 
+let external_reg_field_whole reg rfield =
   let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
   Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
-            
-let external_reg_field_slice reg rfield (i,j) = 
+
+let external_reg_field_slice reg rfield (i,j) =
   let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
   Reg_f_slice (name_of_reg reg) start dir rfield
               (external_slice dir start (m,n))
-              (external_slice dir start (i,j))
+              (external_slice dir start (i,j))*)
 
+(*val external_mem_value : list bitU -> memory_value
 let external_mem_value v =
   byte_lifteds_of_bitv v $> List.reverse
 
+val internal_mem_value : memory_value -> list bitU
 let internal_mem_value bytes =
-  List.reverse bytes $> bitv_of_byte_lifteds
+  List.reverse bytes $> bitv_of_byte_lifteds*)
+
 
 
 
-                       
 
 val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                    (integer -> 'vars -> 'vars) -> 'vars
@@ -756,7 +798,7 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) =
   | RSliceBit of (string * integer)
   | RField of (string * string)
 
-type niafp = 
+type niafp =
   | NIAFP_successor
   | NIAFP_concrete_address of vector bitU
   | NIAFP_LR
@@ -764,13 +806,13 @@ type niafp =
   | NIAFP_register of regfp
 
 (* only for MIPS *)
-type diafp = 
+type diafp =
   | DIAFP_none
   | DIAFP_concrete of vector bitU
   | DIAFP_reg of regfp
 
 let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
-  | RFull name -> 
+  | RFull name ->
      let (start,length,direction,_) = reg_info name Nothing in
      Reg name start length direction
   | RSlice (name,i,j) ->
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index ac6d55b5..d4e2b128 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,5 +1,4 @@
 open import Pervasives_extra
-open import Sail_impl_base
 open import Sail_values
 open import State_monad
 open import {isabelle} `State_monad_extras`
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 2d8e412e..a3bf4b5f 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -1,5 +1,5 @@
 open import Pervasives_extra
-open import Sail_impl_base
+open import Sail_instr_kinds
 open import Sail_values
 
 (* 'a is result type *)
@@ -103,37 +103,21 @@ let rec range i j =
   else if i = j then [i]
   else i :: range (i+1) j
 
-val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
+val get_reg : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a
 let get_reg state reg = reg.read_from state.regstate
 
-val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs
+val set_reg : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -> sequential_state 'regs
 let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
-let is_exclusive = function
-  | Sail_impl_base.Read_plain -> false
-  | Sail_impl_base.Read_reserve -> true
-  | Sail_impl_base.Read_acquire -> false
-  | Sail_impl_base.Read_exclusive -> true
-  | Sail_impl_base.Read_exclusive_acquire -> true
-  | Sail_impl_base.Read_stream -> false
-  | Sail_impl_base.Read_RISCV_acquire -> false
-  | Sail_impl_base.Read_RISCV_strong_acquire -> false
-  | Sail_impl_base.Read_RISCV_reserved -> true
-  | Sail_impl_base.Read_RISCV_reserved_acquire -> true
-  | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true
-  | Sail_impl_base.Read_X86_locked -> true
-end
-
-
 val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e
 let read_mem read_kind addr sz state =
   let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = of_bits (Sail_values.internal_mem_value memory_value) in
-  if is_exclusive read_kind
+  let value = bits_of_bytes (List.reverse memory_value) in
+  if read_is_exclusive read_kind
   then [(Value value, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Value value, state)]
 
@@ -147,7 +131,7 @@ let read_tag read_kind addr state =
     | Just t -> t
     | Nothing -> B0
   end in
-  if is_exclusive read_kind
+  if read_is_exclusive read_kind
   then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Value tag, state)]
 
@@ -167,11 +151,15 @@ let write_mem_val v state =
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value (bits_of v) in
-  let addresses_with_value = List.zip addrs v in
-  let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
-                            state.memstate addresses_with_value in
-  [(Value true,  <| state with memstate = memstate |>)]
+  match bytes_of_bits v with
+    | Just v ->
+       let addresses_with_value = List.zip addrs (List.reverse v) in
+       let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
+                                 state.memstate addresses_with_value in
+       [(Value true,  <| state with memstate = memstate |>)]
+    | Nothing ->
+       [(Exception (Assert "write_mem_val"), state)]
+  end
 
 val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e
 let write_tag t state =
@@ -182,7 +170,7 @@ let write_tag t state =
   let tagstate = Map.insert taddr t state.tagstate in
   [(Value true,  <| state with tagstate = tagstate |>)]
 
-val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e
+val read_reg : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> M 'regs 'a 'e
 let read_reg reg state =
   let v = reg.read_from state.regstate in
   [(Value v,state)]
@@ -201,13 +189,13 @@ let read_reg_bitfield reg regfield =
 
 let reg_deref = read_reg
 
-val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e
+val write_reg : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> M 'regs unit 'e
 let write_reg reg v state =
   [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
 
 let write_reg_ref (reg, v) = write_reg reg v
 
-val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e
+val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e
 let update_reg reg f v state =
   let current_value = get_reg state reg in
   let new_value = f current_value v in
@@ -215,14 +203,14 @@ let update_reg reg f v state =
 
 let write_reg_field reg regfield = update_reg reg regfield.set_field
 
-val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a
-let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) reg_val i j (bits_of new_val)
+val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
+let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val)
 let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
 
-let update_reg_pos reg i reg_val x = update_list reg.reg_is_inc reg_val i x
+let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x
 let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
 
-let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) reg_val i (to_bitU bit)
+let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit)
 let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
 
 let update_reg_field_range regfield i j reg_val new_val =