From f9b81e15c97014425a9a958492ebf4fd92d8a8bc Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 14 Mar 2018 11:49:37 +0000
Subject: Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
---
 aarch64/aarch64_extras.lem                         | 136 +++++++++++++++++++++
 aarch64/aarch64_extras_embed_sequential.lem        | 131 --------------------
 aarch64/mono/aarch64_extras.lem                    | 132 ++++++++++----------
 .../demo/aarch64_no_vector/aarch64_no_vector.sail  |   2 +-
 aarch64/no_vector/spec.sail                        |   2 +-
 aarch64/prelude.sail                               |   2 +-
 cheri/Makefile                                     |  43 ++++++-
 cheri/cheri_prelude_common.sail                    |  11 +-
 mips/Makefile                                      |   6 +-
 mips/mips_extras.lem                               |  93 +++++++++-----
 mips/mips_tlb_stub.sail                            |   2 +-
 mips/prelude.sail                                  |  12 +-
 src/gen_lib/sail_operators_bitlists.lem            |   3 +
 src/gen_lib/sail_operators_mwords.lem              |   6 +-
 src/rewrites.ml                                    |  52 ++++++--
 src/sail_lib.ml                                    |   4 +-
 16 files changed, 374 insertions(+), 263 deletions(-)
 create mode 100644 aarch64/aarch64_extras.lem
 delete mode 100644 aarch64/aarch64_extras_embed_sequential.lem

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
new file mode 100644
index 00000000..58f1b9c7
--- /dev/null
+++ b/aarch64/aarch64_extras.lem
@@ -0,0 +1,136 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_bitlists
+open import Prompt_monad
+open import Prompt
+
+type ty512
+instance (Size ty512) let size = 512 end
+declare isabelle target_rep type ty512 = `512`
+type ty1024
+instance (Size ty1024) let size = 1024 end
+declare isabelle target_rep type ty1024 = `1024`
+type ty2048
+instance (Size ty2048) let size = 2048 end
+declare isabelle target_rep type ty2048 = `2048`
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
+let get_slice_int_bl len n lo =
+  (* TODO: Is this the intended behaviour? *)
+  let hi = lo + len - 1 in
+  let bs = bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
+
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bit_list_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
+  let ext_bs = exts_bits len_n bs in
+  maybe_failwith (signed (update_subrange_list false ext_bs hi lo (bits_of v)))
+
+(*let ext_slice signed v i j =
+  let len = length v in
+  let bits = get_bits false (bits_of v) i j in
+  of_bits (if signed then exts_bits len bits else extz_bits len bits)
+val exts_slice : list bitU -> integer -> integer -> list bitU
+let exts_slice v i j = ext_slice true v i j
+val extz_slice : list bitU -> integer -> integer -> list bitU
+let extz_slice v i j = ext_slice false v i j*)
+
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
+let hexchar_to_bool_list c =
+  if c = #'0' then      Just ([false;false;false;false])
+  else if c = #'1' then Just ([false;false;false;true ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools s =
+  match (toCharList s) with
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
+  end
+
+val hex_slice : forall 'rv 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
+let hex_slice v len lo =
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* Use constants for undefined values for now *)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
+
+let write_ram addrsize size hexRAM address value =
+  write_mem_ea Write_plain address size >>
+  write_mem_val value >>= fun _ ->
+  return ()
+
+let read_ram addrsize size hexRAM address =
+  read_mem Read_plain address size
diff --git a/aarch64/aarch64_extras_embed_sequential.lem b/aarch64/aarch64_extras_embed_sequential.lem
deleted file mode 100644
index 4f9e0fe3..00000000
--- a/aarch64/aarch64_extras_embed_sequential.lem
+++ /dev/null
@@ -1,131 +0,0 @@
-open import Pervasives_extra
-open import Sail_impl_base
-open import Sail_values
-open import Sail_operators_bitlists
-open import State
-
-type ty2048
-instance (Size ty2048) let size = 2048 end
-declare isabelle target_rep type ty2048 = `2048`
-
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
-
-val uint : list bitU -> integer
-let uint = unsigned
-val sint : list bitU -> integer
-let sint = signed
-
-val slice : list bitU -> integer -> integer -> list bitU
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
-let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
-  update_subrange_vec_dec out (n + slice_len - 1) n v
-
-let get_slice_int_bl len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  get_bits false bits hi lo
-
-val get_slice_int : integer -> integer -> integer -> list bitU
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
-
-val set_slice_int : integer -> integer -> integer -> list bitU -> integer
-let set_slice_int len n lo v =
-  let hi = lo + len - 1 in
-  let bits = bitlist_of_int n in
-  let len_n = max (hi + 1) (integerFromNat (List.length bits)) in
-  let ext_bits = exts_bits len_n bits in
-  signed (set_bits false ext_bits hi lo (bits_of v))
-
-let ext_slice signed v i j =
-  let len = length v in
-  let bits = get_bits false (bits_of v) i j in
-  of_bits (if signed then exts_bits len bits else extz_bits len bits)
-val exts_slice : list bitU -> integer -> integer -> list bitU
-let exts_slice v i j = ext_slice true v i j
-val extz_slice : list bitU -> integer -> integer -> list bitU
-let extz_slice v i j = ext_slice false v i j
-
-val shr_int : ii -> ii -> ii
-let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
-
-val shl_int : integer -> integer -> integer
-let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
-
-let hexchar_to_bitlist c =
-  if c = #'0' then [B0;B0;B0;B0]
-  else if c = #'1' then [B0;B0;B0;B1]
-  else if c = #'2' then [B0;B0;B1;B0]
-  else if c = #'3' then [B0;B0;B1;B1]
-  else if c = #'4' then [B0;B1;B0;B0]
-  else if c = #'5' then [B0;B1;B0;B1]
-  else if c = #'6' then [B0;B1;B1;B0]
-  else if c = #'7' then [B0;B1;B1;B1]
-  else if c = #'8' then [B1;B0;B0;B0]
-  else if c = #'9' then [B1;B0;B0;B1]
-  else if c = #'A' then [B1;B0;B1;B0]
-  else if c = #'a' then [B1;B0;B1;B0]
-  else if c = #'B' then [B1;B0;B1;B1]
-  else if c = #'b' then [B1;B0;B1;B1]
-  else if c = #'C' then [B1;B1;B0;B0]
-  else if c = #'c' then [B1;B1;B0;B0]
-  else if c = #'D' then [B1;B1;B0;B1]
-  else if c = #'d' then [B1;B1;B0;B1]
-  else if c = #'E' then [B1;B1;B1;B0]
-  else if c = #'e' then [B1;B1;B1;B0]
-  else if c = #'F' then [B1;B1;B1;B1]
-  else if c = #'f' then [B1;B1;B1;B1]
-  else failwith "hexchar_to_bitlist given unrecognized character"
-
-let hexstring_to_bits s =
-  match (toCharList s) with
-  | z :: x :: hs ->
-    let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
-    List.concat (List.map hexchar_to_bitlist str)
-  | _ -> failwith "hexstring_to_bits called with unexpected string"
-  end
-
-val hex_slice : string -> integer -> integer -> list bitU
-let hex_slice v len lo =
-  let hi = len + lo - 1 in
-  let bits = extz_bits (len + lo) (hexstring_to_bits v) in
-  of_bits (get_bits false bits hi lo)
-
-let internal_pick vs = head vs
-
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : integer -> list bitU
-let undefined_bitvector len = duplicate B0 len
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
-
-let write_ram addrsize size hexRAM address value = ()
-  (*write_mem_ea Write_plain address size >>
-  write_mem_val value >>= fun _ ->
-  return ()*)
-
-let read_ram addrsize size hexRAM address =
-  (*let _ = prerr_endline ("Reading " ^ (stringFromInteger size) ^ " bytes from address " ^ (stringFromInteger (unsigned address))) in*)
-  (*read_mem false Read_plain address size*)
-  undefined_bitvector (8 * size)
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 8af9ee5d..0a6bab11 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -3,7 +3,7 @@ open import Sail_instr_kinds
 open import Sail_values
 open import Sail_operators_mwords
 open import Prompt_monad
-open import State
+open import Prompt
 
 type ty512
 instance (Size ty512) let size = 512 end
@@ -26,11 +26,6 @@ val putchar : integer -> unit
 let putchar _ = ()
 declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
 
-val uint : forall 'a. Size 'a => mword 'a -> integer
-let uint = unsigned
-val sint : forall 'a. Size 'a => mword 'a -> integer
-let sint = signed
-
 val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
 let slice v lo len =
   subrange_vec_dec v (lo + len - 1) lo
@@ -42,28 +37,28 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 let get_slice_int_bl len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  get_bits false bits hi lo
+  let bs = bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
 
 val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
 
 val set_slice_int :  forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
 let set_slice_int len n lo v =
   let hi = lo + len - 1 in
-  let bits = bitlist_of_int n in
-  let len_n = max (hi + 1) (integerFromNat (List.length bits)) in
-  let ext_bits = exts_bits len_n bits in
-  signed (set_bits false ext_bits hi lo (bits_of v))
+  let bs = bool_list_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
+  let ext_bs = exts_bools len_n bs in
+  signed_of_bools (update_subrange_list false ext_bs hi lo (bitlistFromWord v))
 
-let ext_slice signed v i j =
+(*let ext_slice signed v i j =
   let len = length v in
   let bits = get_bits false (bits_of v) i j in
   of_bits (if signed then exts_bits len bits else extz_bits len bits)
 val exts_slice : list bitU -> integer -> integer -> list bitU
 let exts_slice v i j = ext_slice true v i j
 val extz_slice : list bitU -> integer -> integer -> list bitU
-let extz_slice v i j = ext_slice false v i j
+let extz_slice v i j = ext_slice false v i j*)
 
 val shr_int : ii -> ii -> ii
 let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
@@ -71,61 +66,66 @@ let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
 val shl_int : integer -> integer -> integer
 let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
 
-let hexchar_to_bitlist c =
-  if c = #'0' then [B0;B0;B0;B0]
-  else if c = #'1' then [B0;B0;B0;B1]
-  else if c = #'2' then [B0;B0;B1;B0]
-  else if c = #'3' then [B0;B0;B1;B1]
-  else if c = #'4' then [B0;B1;B0;B0]
-  else if c = #'5' then [B0;B1;B0;B1]
-  else if c = #'6' then [B0;B1;B1;B0]
-  else if c = #'7' then [B0;B1;B1;B1]
-  else if c = #'8' then [B1;B0;B0;B0]
-  else if c = #'9' then [B1;B0;B0;B1]
-  else if c = #'A' then [B1;B0;B1;B0]
-  else if c = #'a' then [B1;B0;B1;B0]
-  else if c = #'B' then [B1;B0;B1;B1]
-  else if c = #'b' then [B1;B0;B1;B1]
-  else if c = #'C' then [B1;B1;B0;B0]
-  else if c = #'c' then [B1;B1;B0;B0]
-  else if c = #'D' then [B1;B1;B0;B1]
-  else if c = #'d' then [B1;B1;B0;B1]
-  else if c = #'E' then [B1;B1;B1;B0]
-  else if c = #'e' then [B1;B1;B1;B0]
-  else if c = #'F' then [B1;B1;B1;B1]
-  else if c = #'f' then [B1;B1;B1;B1]
-  else failwith "hexchar_to_bitlist given unrecognized character"
-
-let hexstring_to_bits s =
+let hexchar_to_bool_list c =
+  if c = #'0' then      Just ([false;false;false;false])
+  else if c = #'1' then Just ([false;false;false;true ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools s =
   match (toCharList s) with
-  | z :: x :: hs ->
-    let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
-    List.concat (List.map hexchar_to_bitlist str)
-  | _ -> failwith "hexstring_to_bits called with unexpected string"
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
   end
 
-val hex_slice : forall 'n. Size 'n => string -> integer -> integer -> mword 'n
+val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
 let hex_slice v len lo =
-  let hi = len + lo - 1 in
-  let bits = extz_bits (len + lo) (hexstring_to_bits v) in
-  of_bits (get_bits false bits hi lo)
-
-let internal_pick vs = head vs
-
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a
-let undefined_bitvector len = duplicate B0 len
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* Use constants for undefined values for now *)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
 
 let write_ram addrsize size hexRAM address value =
   write_mem_ea Write_plain address size >>
diff --git a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail b/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
index 2960240d..202f69ac 100644
--- a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
@@ -2546,7 +2546,7 @@ function PACInvSub Tinput = {
   return(Toutput)
 }
 
-val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg}
+val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg, escape}
 
 function ComputePAC (data, modifier, key0, key1) = {
   workingval : bits(64) = undefined;
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 21448bc1..44dc4224 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -2544,7 +2544,7 @@ function PACInvSub Tinput = {
   return(Toutput)
 }
 
-val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg}
+val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {escape, rreg, undef, wreg}
 
 function ComputePAC (data, modifier, key0, key1) = {
   workingval : bits(64) = undefined;
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index d9ba1cde..097dbf47 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -142,7 +142,7 @@ val UInt = {
 
 val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) effect {escape}
 
 val __SetSlice_bits = "set_slice" : forall 'n 'm.
   (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
diff --git a/cheri/Makefile b/cheri/Makefile
index c7f72557..6fa738a7 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -7,16 +7,51 @@ CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri
 SAIL:=$(SAIL_DIR)/sail
 SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail
 
-CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+MIPS_PRE:=$(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail
+MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail
+MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
+MIPS_INSTS:=$(MIPS_SAIL_DIR)/mips_insts.sail
+MIPS_EPILOGUE:=$(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail
+CHERI128_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail
+CHERI_INSTS:=$(CHERI_SAIL_DIR)/cheri_insts.sail
 
-CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE)
+CHERI_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE)
+CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE)
+CHERI128_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE)
+CHERI_MAIN:=$(CHERI_SAIL_DIR)/main.sail
 
-cheri: $(CHERI_SAILS)
+cheri: $(CHERI_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml -o $@ $^
 
-cheri128: $(CHERI128_SAILS)
+cheri128: $(CHERI128_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml -o $@ $^
 
+# TODO Using bit lists for now in Lem generation; for machine words,
+# monomorphisation is needed due to some variable length bitvectors, e.g. in
+# CLoad as of commit b34c3fb, in the TLB translation, and in compressed
+# capability functions
+
+cheri_no_tlb.lem: $(CHERI_NO_TLB_SAILS)
+	$(SAIL) -lem -o cheri_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri_no_tlb_types.lem: cheri_no_tlb.lem
+
+cheri.lem: $(CHERI_SAILS)
+	$(SAIL) -lem -o cheri -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri_types.lem: cheri.lem
+
+cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS)
+	$(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri128_no_tlb_types.lem: cheri128_no_tlb.lem
+
+cheri128.lem: $(CHERI128_SAILS)
+	$(SAIL) -lem -o cheri128 -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri128_types.lem: cheri128.lem
+
+C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
+	lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
+
 clean:
 	rm -rf cheri cheri128 _sbuild inst_*.sail
 
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 5dd14974..0072ded7 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -255,8 +255,8 @@ function register_inaccessible(r) =
   else
     false
 
-val MEMr_tag = "read_tag"  : bits(64) -> bool effect { rmemt }
-val MEMw_tag = "write_tag" : (bits(64) , bool) -> unit effect { wmvt }
+val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
+val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
 
 val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { escape, rmem, rmemt }
 function MEMr_tagged (addr) =
@@ -360,7 +360,12 @@ function addrWrapper(addr, accessType, width) =
       to_bits(64, vAddr); /* XXX vAddr not truncated because top <= 2^64 and size > 0 */
   }
 
-val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape}
+$ifdef _MIPS_TLB_STUB
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape}
+$else
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef}
+$endif
+
 function TranslatePC (vAddr) = {
   incrementCP0Count();
   let pcc = capRegToCapStruct(PCC);
diff --git a/mips/Makefile b/mips/Makefile
index 55d8e986..87fc96b6 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -13,15 +13,15 @@ MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.s
 MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail
 
 mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
-	$(SAIL) -ocaml -o mips $^
+	$(SAIL) -ocaml -o mips -memo_z3 $^
 
 mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
-	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen $^
+	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_no_tlb_types.lem: mips_no_tlb.lem
 
 # TODO: Use monomorphisation so that we can switch to machine words
 mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
-	$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen $^
+	$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_types.lem: mips.lem
 
 M%.thy: m%.lem m%_types.lem mips_extras.lem
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 12915271..bed8cd39 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -14,15 +14,23 @@ val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a
 let MEMr addr size             = read_mem Read_plain addr size
 let MEMr_reserve addr size     = read_mem Read_reserve addr size
 
+val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e
+let read_tag_bool addr =
+  read_tag addr >>= fun t ->
+  maybe_fail "read_tag_bool" (bool_of_bitU t)
+
+val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e
+let write_tag_bool addr t = write_tag addr (bitU_of_bool t) >>= fun _ -> return ()
+
 let MEMr_tag addr size =
   read_mem Read_plain addr size >>= fun v ->
-  read_tag addr >>= fun t ->
-  return (bool_of_bitU t, v)
+  read_tag_bool addr >>= fun t ->
+  return (t, v)
 
 let MEMr_tag_reserve addr size =
   read_mem Read_plain addr size >>= fun v ->
-  read_tag addr >>= fun t ->
-  return (bool_of_bitU t, v)
+  read_tag_bool addr >>= fun t ->
+  return (t, v)
 
 
 val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
@@ -44,8 +52,8 @@ val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b
 
 let MEMval _ size v                      = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional _ size v          = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag addr size t v             = write_mem_val v >>= fun _ -> write_tag addr (bitU_of_bool t) >>= fun _ -> return ()
-let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag addr (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
+let MEMval_tag addr size t v             = write_mem_val v >>= fun _ -> write_tag_bool addr t >>= fun _ -> return ()
+let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag_bool addr t >>= fun _ -> return (if b then true else false)
 
 val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e
 
@@ -57,11 +65,11 @@ let MEM_sync () = barrier Barrier_MIPS_SYNC
 let get_slice_int_bl len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  get_bits false bits hi lo
+  let bs = bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
 
 val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
 
 let write_ram _ size _ addr data =
   MEMea addr size >>
@@ -69,29 +77,48 @@ let write_ram _ size _ addr data =
 
 let read_ram _ size _ addr = MEMr addr size
 
-let sign_extend bits len = exts_bv len bits
-let zero_extend bits len = extz_bv len bits
-
-let shift_bits_left v n = shiftl_bv v (unsigned n)
-let shift_bits_right v n = shiftr_bv v (unsigned n)
-let shift_bits_right_arith v n = arith_shiftr_bv v (unsigned n)
-
-(* TODO: These could be monadic instead of hardcoded *)
-let internal_pick vs = head vs
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a
-let undefined_bitvector len = of_bits (repeat [B0] len)
-val undefined_bits : forall 'a. Bitvector 'a => integer -> 'a
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
+let string_of_bits bs = string_of_bv (bits_of bs)
+let string_of_int = show
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+let sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
+let zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
+
+let shift_bits_left v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in
+  maybe_fail "shift_bits_left" r
+let shift_bits_right v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in
+  maybe_fail "shift_bits_right" r
+let shift_bits_right_arith v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in
+  maybe_fail "shift_bits_right_arith" r
+
+(* Use constants for undefined values for now *)
+let internal_pick vs = return (head vs)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
 
 let skip () = return ()
diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail
index f0ffb9dd..c42e4764 100644
--- a/mips/mips_tlb_stub.sail
+++ b/mips/mips_tlb_stub.sail
@@ -36,7 +36,7 @@ $ifndef _MIPS_TLB_STUB
 $define _MIPS_TLB_STUB
 
 val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
-function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None
+function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None()
 
 val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
 function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) = 
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 5b89521f..272b6e04 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -86,9 +86,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
 overload operator | = {or_bool, or_vec}
 
-val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
-val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
 val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
 
@@ -355,18 +355,18 @@ infix 1 >>
 infix 1 <<
 infix 1 >>_s
 
-val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
 
 val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
 val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
 
 overload operator >> = {shift_bits_right, shiftr}
 overload operator << = {shift_bits_left, shiftl}
-val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
 
 infix 7 *_s
-val operator *_s = "smult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
+val operator *_s = "mults_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
 infix 7 *_u
 val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
 
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index 9b81e233..edba83ba 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -220,6 +220,9 @@ let duplicate_oracle b n =
   bool_of_bitU_oracle b >>= (fun b ->
   return (duplicate (bitU_of_bool b) n))
 
+val reverse_endianness : list bitU -> list bitU
+let reverse_endianness v = reverse_endianness_list v
+
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 val ult_vec   : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index ea7c11cf..e87f4b7c 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,9 +5,6 @@ open import Sail_operators
 open import Prompt_monad
 open import Prompt
 
-val mword_zero : forall 'a. Size 'a => mword 'a
-let mword_zero = wordFromInteger 0
-
 (* Specialisation of operators to machine words *)
 
 let uint v = unsignedIntegerFromWord v
@@ -233,6 +230,9 @@ let duplicate_fail   b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_b
 let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n))
 let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 
+val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
+let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
+
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 6e98abb0..fbaf1234 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -174,14 +174,50 @@ let find_updated_vars exp =
   fst (fold_exp
     { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
 
+let lookup_equal_kids env =
+  let get_eq_kids kid eqs = match KBindings.find_opt kid eqs with
+    | Some kids -> kids
+    | None -> KidSet.singleton kid
+  in
+  let add_eq_kids kid1 kid2 eqs =
+    let kids = KidSet.union (get_eq_kids kid2 eqs) (get_eq_kids kid1 eqs) in
+    eqs
+    |> KBindings.add kid1 kids
+    |> KBindings.add kid2 kids
+  in
+  let add_nc eqs = function
+    | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _) ->
+       add_eq_kids kid1 kid2 eqs
+    | _ -> eqs
+  in
+  List.fold_left add_nc KBindings.empty (Env.get_constraints env)
+
+let lookup_constant_kid env kid =
+  match KBindings.find_opt kid (lookup_equal_kids env) with
+    | Some kids ->
+       let check_nc const nc = match const, nc with
+         | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _)
+           when KidSet.mem kid kids ->
+            Some i
+         | _, _ -> const
+       in
+       List.fold_left check_nc None (Env.get_constraints env)
+    | None -> None
+
 let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
-| Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
-| Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
-| Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
-| Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
-| Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l)
-| Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
-| _ -> nexp_aux
+  | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
+  | Nexp_var kid ->
+     begin
+       match lookup_constant_kid env kid with
+         | Some i -> nconstant i
+         | None -> nexp_aux
+     end
+  | Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+  | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+  | Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+  | Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l)
+  | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
+  | _ -> nexp_aux
 
 let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
   let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with
@@ -3097,6 +3133,7 @@ let rewrite_defs_lem = [
   ("guarded_pats", rewrite_defs_guarded_pats);
   ("bitvector_exps", rewrite_bitvector_exps);
   (* ("register_ref_writes", rewrite_register_ref_writes); *)
+  ("nexp_ids", rewrite_defs_nexp_ids);
   ("fix_val_specs", rewrite_fix_val_specs);
   ("split_execute", rewrite_split_fun_constr_pats "execute");
   ("recheck_defs", recheck_defs);
@@ -3107,7 +3144,6 @@ let rewrite_defs_lem = [
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
-  ("nexp_ids", rewrite_defs_nexp_ids);
   ("fix_val_specs", rewrite_fix_val_specs);
   ("remove_blocks", rewrite_defs_remove_blocks);
   ("letbind_effects", rewrite_defs_letbind_effects);
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 76dec253..96baa279 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -437,11 +437,11 @@ let read_ram (addr_size, data_size, hex_ram, addr) =
 
 let tag_ram : bool RAM.t = RAM.create 256
 
-let write_tag (addr, tag) =
+let write_tag_bool (addr, tag) =
   let addri = uint addr in
   RAM.add tag_ram addri tag
 
-let read_tag addr =
+let read_tag_bool addr =
   let addri = uint addr in
   try RAM.find tag_ram addri with Not_found -> false
 
-- 
cgit v1.2.3