Add/generate Isabelle lemmas about the monad lifting

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

9 files changed, 317 insertions, 309 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 756bb699..728014eb 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -10,81 +10,38 @@ let rec iter_aux i f xs = match xs with
   | [] -> return ()
   end
 
+declare {isabelle} termination_argument iter_aux = automatic
+
 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 '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 : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
+let rec foreachM [] vars _ = return vars
+and foreachM (x :: xs) vars body =
+  body x vars >>= fun vars ->
+  foreachM xs vars body
 
-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
-    body i vars >>= fun vars ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return vars
-
-
-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
-    body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return vars
-
-val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec while_PP vars cond body =
-  if cond vars then while_PP (body vars) cond body else vars
-
-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
+declare {isabelle} termination_argument foreachM = automatic
 
-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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val whileM : 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 =
+let rec whileM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then
-    body vars >>= fun vars -> while_MM vars cond body
+    body vars >>= fun vars -> whileM vars cond body
   else return vars
 
-val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-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 '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 '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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val untilM : 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 =
+let rec untilM vars cond body =
   body vars >>= fun vars ->
   cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MM vars cond body
+  if cond_val then return vars else untilM vars cond body
 
 (*let write_two_regs r1 r2 vec =
   let is_inc =
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 38f79868..3c414d6e 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -4,17 +4,25 @@ open import Sail_instr_kinds
 open import Sail_values
 
 type register_name = string
+type address = list bitU
 
 type monad 'regval 'a 'e =
   | Done of 'a
-  | Read_mem of read_kind * integer * integer * (list memory_byte -> monad 'regval 'a 'e)
+  (* 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 * integer * integer * monad 'regval 'a 'e
+  | Write_ea of write_kind * address * 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 *)
+     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 last signalled address. *)
+  | Write_tagv of bitU * (bool -> monad 'regval 'a 'e)
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of 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 *)
@@ -35,10 +43,13 @@ val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> mo
 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_tagv t k ->     Write_tagv 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)
   | 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
@@ -63,10 +74,13 @@ val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a
 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_tagv t k ->     Write_tagv 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)
   | 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
@@ -106,11 +120,8 @@ let try_catchR m h =
 
 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 = unsigned addr in
-  let k bytes =
-    let bitv = bits_of_bytes (List.reverse bytes) in
-    (Done bitv) in
-  Read_mem rk addr sz k
+  let k bytes = Done (bits_of_mem_bytes bytes) in
+  Read_mem rk (bits_of addr) (natFromInteger sz) k
 
 val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
@@ -118,13 +129,11 @@ 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 (unsigned addr) sz (Done ())
+let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger 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
+let write_mem_val v = match mem_bytes_of_bits v with
+  | Just v -> Write_memv v return
   | Nothing -> Fail "write_mem_val"
 end
 
@@ -182,5 +191,5 @@ 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 'rv 'e. monad 'rv unit 'e
-let footprint = Footprint (Done ())*)
+val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
+let footprint _ = Footprint (Done ())
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b981bb91..ead63d62 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -205,18 +205,15 @@ let rec bits_of_nat_aux x =
 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
-let nat_of_bits bits =
-  let (sum,_) =
-    List.foldr
-      (fun b (acc,exp) ->
-        match b with
-        | B1 -> (acc + naturalPow 2 exp, exp + 1)
-        | B0 -> (acc, exp + 1)
-        | BU -> failwith "nat_of_bits: bitvector has undefined bits"
-        end)
-      (0,0) bits in
-  sum
+val nat_of_bits_aux : natural -> list bitU -> natural
+let rec nat_of_bits_aux acc bs = match bs with
+  | [] -> acc
+  | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs
+  | B0 :: bs -> nat_of_bits_aux (2 * acc) bs
+  | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits"
+end
+declare {isabelle} termination_argument nat_of_bits_aux = automatic
+let nat_of_bits bits = nat_of_bits_aux 0 bits
 
 let not_bits = List.map not_bit
 
@@ -543,6 +540,9 @@ let bytes_of_bits bs = byte_chunks (bits_of bs)
 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))
 
+let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs)
+let bits_of_mem_bytes bs = bits_of_bytes (List.reverse 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
@@ -612,7 +612,7 @@ type register_ref 'regstate 'regval 'a =
   <| name : string;
      (*is_inc : bool;*)
      read_from : 'regstate -> 'a;
-     write_to : 'regstate -> 'a -> 'regstate;
+     write_to : 'a -> 'regstate -> 'regstate;
      of_regval : 'regval -> maybe 'a;
      regval_of : 'a -> 'regval |>
 
@@ -750,24 +750,28 @@ let internal_mem_value bytes =
   List.reverse bytes $> bitv_of_byte_lifteds*)
 
 
+val foreach : forall 'a 'vars.
+  (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
+let rec foreach [] vars _ = vars
+and foreach (x :: xs) vars body = foreach xs (body x vars) body
+
+declare {isabelle} termination_argument foreach = automatic
 
+val index_list : integer -> integer -> integer -> list integer
+let rec index_list from to step =
+  if (step > 0 && from <= to) || (step < 0 && to <= from) then
+    from :: index_list (from + step) to step
+  else []
 
+val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while vars cond body =
+  if cond vars then while (body vars) cond body else vars
 
-val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
-                   (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then let vars = body i vars in
-       foreach_inc (i + by,stop,by) vars body
-  else vars
+val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec until vars cond body =
+  let vars = body vars in
+  if cond vars then vars else until (body vars) cond body
 
-val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then let vars = body i vars in
-       foreach_dec (i - by,stop,by) vars body
-  else vars
 
 let assert' b msg_opt =
   let msg = match msg_opt with
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index fba8d9b7..1740174e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -11,12 +11,15 @@ open import {isabelle} `State_monad_extras`
 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_memS rk a sz)     (fun v -> liftState ra (k v))
-  | (Write_memv descr k) -> bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
-  | (Read_reg descr k)   -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
-  | (Excl_res k)         -> bindS (excl_resultS ())       (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)
+  | (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))
+  | (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
@@ -24,99 +27,43 @@ let rec liftState ra s = match s with
 end
 
 
-(* TODO
-val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let rec iter_aux i f xs = match xs with
-  | x :: xs -> f i x >> iter_aux (i + 1) f xs
-  | [] -> return ()
+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
 
-val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let iteri f xs = iter_aux 0 f xs
+declare {isabelle} termination_argument iterS_aux = automatic
 
-val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let iter f xs = iteri (fun _ x -> f x) xs
+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 foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec foreachM_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return vars
+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 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 ->
+     foreachS xs vars body
+end
 
-val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return vars
-
-val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec while_PP vars cond body =
-  if cond vars then while_PP (body vars) cond body else vars
-
-val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_PM vars cond body s =
-  if cond vars then
-    bind (body vars) (fun vars s' -> while_PM vars cond body s') s
-  else return vars s
-
-val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec while_MP vars cond body s =
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then while_MP (body vars) cond body s' else return vars s') s
-
-val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_MM vars cond body s =
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then
-        bind
-          (body vars)
-          (fun vars s'' -> while_MM vars cond body s'') s'
-      else return vars s') s
-
-val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec until_PP vars cond body =
-  let vars = body vars in
-  if (cond vars) then vars else until_PP (body vars) cond body
+declare {isabelle} termination_argument foreachS = automatic
 
-val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_PM vars cond body s =
-  bind
-    (body vars)
-    (fun vars s' ->
-      if (cond vars) then return vars s' else until_PM vars cond body s') s
 
-val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec until_MP vars cond body s =
-  let vars = body vars in
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then return vars s' else until_MP vars cond body s') s
+val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec whileS vars cond body s =
+  (cond vars >>$= (fun cond_val s' ->
+  if cond_val then
+    (body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s'
+  else returnS vars s')) s
 
-val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_MM vars cond body s =
-  bind
-    (body vars)
-    (fun vars s' ->
-      bind
-        (cond vars)
-        (fun cond_val s''->
-          if cond_val then return vars s'' else until_MM vars cond body s'') s') s
-*)
+val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec untilS vars cond body s =
+  (body vars >>$= (fun vars s' ->
+  (cond vars >>$= (fun cond_val s'' ->
+  if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index f324a9f4..8ff39d62 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -24,7 +24,6 @@ let init_state regs =
      last_exclusive_operation_was_load = false |>
 
 type ex 'e =
-  | Exit
   | Failure of string
   | Throw of 'e
 
@@ -49,12 +48,24 @@ let bindS m f (s : sequential_state 'regs) =
 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)
 
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () s = [(Ex Exit, s)]
+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)]
 
@@ -63,7 +74,6 @@ let try_catchS m h s =
   List.concatMap (function
                   | (Value a, s') -> returnS a s'
                   | (Ex (Throw e), s') -> h e s'
-                  | (Ex Exit, s') -> [(Ex Exit, s')]
                   | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')]
                   end) (m s)
 
@@ -99,85 +109,77 @@ let try_catchSR m h =
       | Right e -> h e
      end)
 
-val range : integer -> integer -> list integer
-let rec range i j =
-  if j < i then []
-  else if i = j then [i]
-  else i :: range (i+1) j
-
-val get_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a
-let get_regS state reg = reg.read_from state.regstate
-
-val set_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -> sequential_state 'regs
-let set_regS state reg v =
-  <| state with regstate = reg.write_to state.regstate v |>
-
-
-val read_memS : forall 'regs 'e. read_kind -> integer -> integer -> monadS 'regs (list memory_byte) 'e
-let read_memS read_kind addr sz s =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  let addrs = range addr (addr+sz-1) in
-  match just_list (List.map (fun addr -> Map.lookup addr s.memstate) addrs) with
+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 ->
-       let s' =
+       updateS (fun s ->
          if read_is_exclusive read_kind
          then <| s with last_exclusive_operation_was_load = true |>
-         else s
-       in
-       returnS (List.reverse mem_val) s'
-    | Nothing -> failS "read_memS" s
-  end
-
-(* caps are aligned at 32 bytes *)
-let cap_alignment = (32 : integer)
-
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> monadS 'regs bitU 'e
-let read_tagS read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
-  let tag = match (Map.lookup addr state.tagstate) with
-    | Just t -> t
-    | Nothing -> B0
-  end in
-  if read_is_exclusive read_kind
-  then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
-  else [(Value tag, state)]
+         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 () state =
-  let success =
-    (Value true,  <| state with last_exclusive_operation_was_load = false |>) in
-  (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-
-val write_mem_eaS : forall 'regs 'e. write_kind -> integer -> integer -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz state =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  [(Value (), <| state with write_ea = Just (write_kind, addr, sz) |>)]
-
-val write_mem_valS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_valS v state =
-  let (_,addr,sz) = match state.write_ea with
-    | 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 (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 |>)]
+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 state =
-  let (_,addr,_) = match state.write_ea with
-    | Nothing -> failwith "write ea has not been announced yet"
-    | Just write_ea -> write_ea end in
-  let taddr = addr / cap_alignment in
-  let tagstate = Map.insert taddr t state.tagstate in
-  [(Value true,  <| state with tagstate = tagstate |>)]
+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 s = [(Value (reg.read_from s.regstate), s)]
+let read_regS reg = readS (fun s -> reg.read_from s.regstate)
 
 (* TODO
 let read_reg_range reg i j state =
@@ -195,23 +197,23 @@ let read_reg_bitfield reg regfield =
 
 val read_regvalS : forall 'regs 'rv 'e.
   register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg s =
-  match read reg s.regstate with
-    | Just v ->  returnS v s
-    | Nothing -> failS ("read_regvalS " ^ reg) s
-  end
+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 s =
-  match write reg v s.regstate with
-    | Just rs' -> returnS () (<| s with regstate = rs' |>)
-    | Nothing ->  failS ("write_regvalS " ^ reg) s
-  end
+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 state =
-  [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
+let write_regS reg v =
+  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
 
 (* TODO
 val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ac8ad48d..a0390a94 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -622,13 +622,13 @@ let doc_exp_lem, doc_let_lem =
                  | E_aux (E_let (LB_aux (LB_val (
                      P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
-               let combinator = match effectful (effect_of body), ord_exp with
-                 | false, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreach_dec"
-                 | false, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreach_inc"
-                 | true, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreachM_dec"
-                 | true, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreachM_inc"
-                 | _ -> raise (Reporting_basic.err_unreachable l "Unable to figure out loop combinator") in
-               let indices_pp = parens (separate_map comma expY [exp1; exp2; exp3]) in
+               let step = match ord_exp with
+                 | E_aux (E_lit (L_aux (L_false, _)), _) ->
+                    parens (separate space [string "integerNegate"; expY exp3])
+                 | _ -> expY exp3
+               in
+               let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
+               let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
                parens (
                    (prefix 2 1)
                      ((separate space) [string combinator; indices_pp; expY vartuple])
@@ -643,11 +643,14 @@ let doc_exp_lem, doc_let_lem =
           begin
             match args with
             | [cond; varstuple; body] ->
-               let csuffix = match effectful (effect_of cond), effectful (effect_of body) with
-                 | false, false -> "_PP"
-                 | false, true  -> "_PM"
-                 | true,  false -> "_MP"
-                 | true,  true  -> "_MM" in
+               let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in
+               let csuffix, cond, body =
+                 match effectful (effect_of cond), effectful (effect_of body) with
+                   | false, false -> "", cond, body
+                   | false, true  -> "M", return cond, body
+                   | true,  false -> "M", cond, return body
+                   | true,  true  -> "M", cond, body
+               in
                parens (
                    (prefix 2 1)
                      ((separate space) [string (combinator ^ csuffix); expY varstuple])
@@ -717,7 +720,7 @@ let doc_exp_lem, doc_let_lem =
         | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
           when Env.is_record tid env ->
            let fname =
-             if prefix_recordtype
+             if prefix_recordtype && string_of_id tid <> "regstate"
              then (string (string_of_id tid ^ "_")) ^^ doc_id_lem id
              else doc_id_lem id in
            expY fexp ^^ dot ^^ fname
@@ -732,10 +735,11 @@ let doc_exp_lem, doc_let_lem =
        let eff = effect_of full_exp in
        let base_typ = Env.base_typ_of env typ in
        if has_effect eff BE_rreg then
-         let epp = separate space [string "read_reg";doc_id_lem id] in
+         let epp = separate space [string "read_reg";doc_id_lem (append_id id "_ref")] in
          if is_bitvector_typ base_typ
          then liftR (parens (epp ^^ doc_tannot_lem ctxt env true base_typ))
          else liftR epp
+       else if Env.is_register id env then doc_id_lem (append_id id "_ref")
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
     | E_lit lit -> doc_lit_lem lit
@@ -870,7 +874,7 @@ let doc_exp_lem, doc_let_lem =
 
   and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) =
     let fname =
-      if prefix_recordtype
+      if prefix_recordtype && string_of_id recordtyp <> "regstate"
       then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
       else doc_id_lem id in
     group (doc_op equals fname (top_exp ctxt true e))
@@ -886,8 +890,8 @@ let doc_exp_lem, doc_let_lem =
   and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
        parens (separate empty [doc_lexp_deref_lem ctxt le;dot;doc_id_lem id])
-    | LEXP_id id -> doc_id_lem id
-    | LEXP_cast (typ,id) -> doc_id_lem id
+    | LEXP_id id -> doc_id_lem (append_id id "_ref")
+    | LEXP_cast (typ,id) -> doc_id_lem (append_id id "_ref")
     | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps)
     | _ ->
        raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
@@ -911,7 +915,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
        (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
        (doc_typschm_lem false typschm)
   | TD_record(id,nm,typq,fs,_) ->
-    let fname fid = if prefix_recordtype
+    let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
     let f_pp (typ,fid) =
@@ -1420,7 +1424,7 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
   let exc_typ = find_exc_typ defs in
   let typdefs, defs = List.partition is_typ_def defs in
   let statedefs, defs = List.partition is_state_def defs in
-  let register_refs = State.register_refs_lem prefix_recordtype !opt_mwords (State.find_registers defs) in
+  let register_refs = State.register_refs_lem !opt_mwords (State.find_registers defs) in
   (print types_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
diff --git a/src/process_file.ml b/src/process_file.ml
index 80cfdccb..a447061b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -48,6 +48,9 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open PPrint
+open Pretty_print_common
+
 let opt_lem_sequential = ref false
 let opt_lem_mwords = ref false
 
@@ -243,7 +246,22 @@ let output_lem filename libs defs =
       "Sail_values";
       operators_module
     ] @ monad_modules
-    in
+  in
+  let isa_thy_name = String.capitalize filename ^ "_lemmas" in
+  let isa_lemmas =
+    separate hardline [
+      string ("theory " ^ isa_thy_name);
+      string  "  imports";
+      string  "    Sail.Sail_values_extras";
+      string  "    Sail.State_extras";
+      string ("    " ^ String.capitalize filename);
+      string  "begin";
+      string  "";
+      State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs;
+      string  "";
+      string  "end"
+    ] ^^ hardline
+  in
   let ((ot,_, _) as ext_ot) =
     open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in
   let ((o,_, _) as ext_o) =
@@ -253,7 +271,11 @@ let output_lem filename libs defs =
      (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
-  close_output_with_check ext_o
+  close_output_with_check ext_o;
+  let ((ol, _, _) as ext_ol) =
+    open_output_with_check_unformatted (isa_thy_name ^ ".thy") in
+  print ol isa_lemmas;
+  close_output_with_check ext_ol
 
 let rec iterate (f : int -> unit) (n : int) : unit =
   if n = 0 then ()
diff --git a/src/state.ml b/src/state.ml
index 5873c472..690c7948 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -177,7 +177,7 @@ let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
      let id = string_of_id (regval_constr_id mwords typ) in
      "(fun v -> " ^ id ^ "_of_regval v)", "(fun v -> regval_of_" ^ id ^ " v)"
 
-let register_refs_lem prefix_recordtype mwords registers =
+let register_refs_lem mwords registers =
   let generic_convs =
     separate_map hardline string [
       "val vector_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)";
@@ -212,20 +212,20 @@ let register_refs_lem prefix_recordtype mwords registers =
   in
   let register_ref (typ, id) =
     let idd = string (string_of_id id) in
-    let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in
+    (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *)
     let of_regval, regval_of = regval_convs_lem mwords typ in
-    concat [string "let "; idd; string " = <|"; hardline;
+    concat [string "let "; idd; string "_ref = <|"; hardline;
       string "  name = \""; idd; string "\";"; hardline;
-      string "  read_from = (fun s -> s."; field; string ");"; hardline;
-      string "  write_to = (fun s v -> (<| s with "; field; string " = v |>));"; hardline;
+      string "  read_from = (fun s -> s."; idd; string ");"; hardline;
+      string "  write_to = (fun v s -> (<| s with "; idd; string " = v |>));"; hardline;
       string "  of_regval = "; string of_regval; string ";"; hardline;
       string "  regval_of = "; string regval_of; string " |>"; hardline]
   in
   let refs = separate_map hardline register_ref registers in
   let get_set_reg (_, id) =
     let idd = string_of_id id in
-    string ("  if reg_name = \"" ^ idd ^ "\" then Just (" ^ idd ^ ".regval_of (" ^ idd ^ ".read_from s)) else"),
-    string ("  if reg_name = \"" ^ idd ^ "\" then Maybe.map (" ^ idd ^ ".write_to s) (" ^ idd ^ ".of_regval v) else")
+    string ("  if reg_name = \"" ^ idd ^ "\" then Just (" ^ idd ^ "_ref.regval_of (" ^ idd ^ "_ref.read_from s)) else"),
+    string ("  if reg_name = \"" ^ idd ^ "\" then Maybe.map (fun v -> " ^ idd ^ "_ref.write_to v s) (" ^ idd ^ "_ref.of_regval v) else")
   in
   let getters_setters =
     let getters, setters = List.split (List.map get_set_reg registers) in
@@ -237,11 +237,72 @@ let register_refs_lem prefix_recordtype mwords registers =
     string "let set_regval reg_name v s =" ^^ hardline ^^
     separate hardline setters ^^ hardline ^^
     string "  Nothing" ^^ hardline ^^ hardline ^^
-    string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline ^^
-    string "let liftS s = liftState register_accessors s" ^^ hardline
+    string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline
+    (* string "let liftS s = liftState register_accessors s" ^^ hardline *)
   in
   separate hardline [generic_convs; refs; getters_setters]
 
+let generate_isa_lemmas mwords (Defs defs : tannot defs) =
+  let rec drop_while f = function
+    | x :: xs when f x -> drop_while f xs
+    | xs -> xs
+  in
+  let remove_leading_underscores str =
+    String.concat "_" (drop_while (fun s -> s = "") (Util.split_on_char '_' str))
+  in
+  let remove_trailing_underscores str =
+    Util.split_on_char '_' str |> List.rev |>
+    drop_while (fun s -> s = "") |> List.rev |>
+    String.concat "_"
+  in
+  let registers = find_registers defs in
+  let regtyp_ids =
+    register_base_types mwords (List.map fst registers)
+    |> Bindings.bindings |> List.map fst
+  in
+  let register_defs =
+    let reg_id id = remove_leading_underscores (string_of_id id) in
+    hang 2 (flow_map (break 1) string
+      (["lemmas register_defs"; "="; "get_regval_def"; "set_regval_def"] @
+      (List.map (fun (typ, id) -> reg_id id ^ "_ref_def") registers)))
+  in
+  let conv_lemma typ_id =
+    let typ_id = remove_trailing_underscores (string_of_id typ_id) in
+    let typ_id' = remove_leading_underscores typ_id in
+    string ("lemma regval_" ^ typ_id ^ "[simp]:") ^^ hardline ^^
+    string ("  \"" ^ typ_id' ^ "_of_regval (regval_of_" ^ typ_id ^ " v) = Some v\"") ^^ hardline ^^
+    string ("  by (auto simp: regval_of_" ^ typ_id ^ "_def)")
+  in
+  let register_lemmas (typ, id) =
+    let id = remove_leading_underscores (string_of_id id) in
+    let id' = remove_trailing_underscores id in
+    separate_map hardline string [
+      "lemma liftS_read_reg_" ^ id ^ "[simp]:";
+      "  \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\"";
+      "  by (auto simp: liftState_read_reg_readS register_defs)";
+      "";
+      "lemma liftS_write_reg_" ^ id ^ "[simp]:";
+      "  \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
+      "  by (auto simp: liftState_write_reg_updateS register_defs)"
+    ]
+  in
+  string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
+  hardline ^^ hardline ^^
+  register_defs ^^
+  hardline ^^ hardline ^^
+  separate_map (hardline ^^ hardline) conv_lemma regtyp_ids ^^
+  hardline ^^ hardline ^^
+  separate_map hardline string [
+    "lemma vector_of_rv_rv_of_vector[simp]:";
+    "  assumes \"\\<And>v. of_rv (rv_of v) = Some v\"";
+    "  shows \"vector_of_regval of_rv (regval_of_vector rv_of len is_inc v) = Some v\"";
+    "proof -";
+    "  from assms have \"of_rv \\<circ> rv_of = Some\" by auto";
+    "  then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def)";
+    "qed"] ^^
+  hardline ^^ hardline ^^
+  separate_map (hardline ^^ hardline) register_lemmas registers
+
 let generate_regstate_defs mwords defs =
   (* FIXME We currently don't want to generate undefined_type functions
      for register state and values.  For the Lem backend, this would require
diff --git a/src/type_check.mli b/src/type_check.mli
index b03e2e00..4685b676 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -148,6 +148,8 @@ module Env : sig
 
   val is_union_constructor : id -> t -> bool
 
+  val is_register : id -> t -> bool
+
   (** Return a fresh kind identifier that doesn't exist in the
      environment. The optional argument bases the new identifer on the
      old one. *)