Merge branch 'sail2' into smt_experiments

25 files changed, 535 insertions, 265 deletions

diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile
index b9abec80..fe4c5841 100644
--- a/aarch64_small/Makefile
+++ b/aarch64_small/Makefile
@@ -1,7 +1,7 @@
-SAIL:=../src/sail.native
+SAIL:=../sail -Ofast_undefined
 LEM:=../../lem/lem
 
-default: armV8_embed.lem
+default: all
 
 # the order of the files is important
 SOURCES=prelude.sail\
@@ -13,24 +13,33 @@ SOURCES=prelude.sail\
   armV8_lib.h.sail\
   armV8_common_lib.sail\
   armV8_A64_lib.sail\
-  armV8.sail
+  armV8.sail\
+  ../lib/regfp.sail\
+  aarch64_regfp.sail
 
-all: armV8.lem armV8.ml armV8_embed.lem
+all: armV8.lem for-rmem/armV8.lem for-rmem/armV8_toFromInterp2.ml for-rmem/armV8.defs
 
 armV8.lem: $(SOURCES)
-	$(SAIL) -lem_ast -o armV8 $(SOURCES)
+# also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem
+	$(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^
 
-armV8.ml: armV8.lem ../src/lem_interp/interp_ast.lem
-	$(LEM) -ocaml -lib ../src/lem_interp/ $<
+for-rmem/armV8.lem: $(SOURCES)
+	mkdir -p $(dir $@)
+#	We do not need the isabelle .thy files, but sail always generates them
+	$(SAIL) -lem -lem_lib ArmV8_extras_embed -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o $(notdir $(basename $@)) $^
 
+for-rmem/armV8_toFromInterp2.ml: $(SOURCES)
+	mkdir -p $(dir $@)
+	$(SAIL) -tofrominterp -tofrominterp_lem  -tofrominterp_output_dir $(dir $@) -o armV8 $^
 
-armV8_embed.lem: $(SOURCES) ../lib/regfp.sail aarch64_regfp.sail
-# also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem
-	$(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^
+for-rmem/armV8.defs: $(SOURCES)
+	mkdir -p $(dir $@)
+	$(SAIL) -marshal -o $(basename $@) $^
 
 clean:
 	rm -f armV8.lem armV8.ml
 	rm -f armV8_embed*.lem armV8_toFromInterp.lem
+	rm -f for-rmem/*
 
 ######################################################################
 ETCDIR=../etc
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index b1eac1e7..d0f0b830 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -275,3 +275,4 @@ function UNKNOWN_BITS(N) = (replicate_bits(0b0, 'N)) : bits('N)
 let UNKNOWN_BIT = b0
 
 /* external */ val speculate_exclusive_success : unit -> bool effect {exmem}
+function speculate_exclusive_success () = __excl_res ()
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index a9a78900..d8ee0bbe 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -125,7 +125,7 @@ function clause execute (TMStart(t)) = {
   }
 }
 
-/* external */ val TMCommitEffect : unit -> unit effect {barr}
+/* external */ val "TMCommitEffect" : unit -> unit effect {barr}
 
 /* TCOMMIT - dummy decoding */
 val decodeTMCommit : unit -> option(ast) effect pure
@@ -2091,7 +2091,7 @@ function clause execute ( ConditionalSelect((d,n,m,datasize as int('R),condition
   wX(d) = result;
 }
 
-val decodeData1Source : bits(32) -> option(ast) effect pure
+val decodeData1Source : bits(32) -> option(ast) effect {escape}
 scattered function decodeData1Source
 
 /* RBIT */
@@ -2178,7 +2178,7 @@ function clause execute (CountLeading((d,n,datasize as int('R),opcode))) = {
 
 end decodeData1Source
 
-val decodeData2Source : bits(32) -> option(ast) effect pure
+val decodeData2Source : bits(32) -> option(ast) effect {escape}
 scattered function decodeData2Source
 
 /* SDIV o1=1 */
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index cc65a03e..8c684fc7 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -504,7 +504,6 @@ function AArch64_ResetSpecialRegisters() -> unit =
 
 /** FUNCTION:aarch64/functions/registers/PC */
 
-val rPC : unit -> bits(64) effect {rreg}
 function rPC () = _PC
 
 /** FUNCTION:// SP[] - assignment form */
diff --git a/aarch64_small/armV8_A64_sys_regs.sail b/aarch64_small/armV8_A64_sys_regs.sail
index 36f7c3f6..20aa4a5c 100644
--- a/aarch64_small/armV8_A64_sys_regs.sail
+++ b/aarch64_small/armV8_A64_sys_regs.sail
@@ -176,8 +176,7 @@ register SCTLR_EL3 : SCTLR_type /* System Control Register (EL3) */
 
 
 /* CP: added coercion from SCTLR_EL1_type to SCTLR_type for the SCTLR function */
-val cast SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type
-
+val cast "SCTLR_EL1_type_to_SCTLR_type" : SCTLR_EL1_type -> SCTLR_type
 
 bitfield TCR_EL1_type : bits(64) =
 {
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index c2ed72ee..b758b28e 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -32,6 +32,20 @@
 /*  SUCH DAMAGE.                                                          */
 /*========================================================================*/
 
+
+/** FUNCTION:shared/functions/system/Unreachable */
+
+/* CP: adding two variants, one that takes a string argument, the other one doesn't  */
+val Unreachable_no_message : forall ('a : Type) . unit -> 'a effect{escape}
+function Unreachable_no_message() = 
+    error("Unreachable reached")
+
+val Unreachable_message : forall ('a : Type) . string -> 'a effect{escape}
+function Unreachable_message(message) = 
+    error(message)
+
+overload Unreachable = {Unreachable_no_message, Unreachable_message}
+
 /** FUNCTION:shared/debug/DoubleLockStatus/DoubleLockStatus */
 
 function DoubleLockStatus() -> boolean= {
@@ -550,8 +564,11 @@ function BigEndianReverse (value) = {
 /** FUNCTION:shared/functions/memory/DataMemoryBarrier */
 
 /* external */ val DataMemoryBarrier_Reads : unit -> unit effect {barr}
+function DataMemoryBarrier_Reads () = __barrier(Barrier_DMB_LD)
 /* external */ val DataMemoryBarrier_Writes : unit -> unit effect {barr}
+function DataMemoryBarrier_Writes () = __barrier(Barrier_DMB_ST)
 /* external */ val DataMemoryBarrier_All : unit -> unit effect {barr}
+function DataMemoryBarrier_All () = __barrier(Barrier_DMB)
 
 val DataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr, escape}
 function DataMemoryBarrier(domain, types) =
@@ -569,8 +586,11 @@ function DataMemoryBarrier(domain, types) =
 /** FUNCTION:shared/functions/memory/DataSynchronizationBarrier */
 
 /* external */ val DataSynchronizationBarrier_Reads : unit -> unit effect {barr}
+function DataSynchronizationBarrier_Reads () = __barrier(Barrier_DSB_LD)
 /* external */ val DataSynchronizationBarrier_Writes : unit -> unit effect {barr}
+function DataSynchronizationBarrier_Writes () = __barrier(Barrier_DSB_ST)
 /* external */ val DataSynchronizationBarrier_All : unit -> unit effect {barr}
+function DataSynchronizationBarrier_All () = __barrier(Barrier_DSB)
 
 val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr,escape}
 function DataSynchronizationBarrier(domain, types) =
@@ -602,14 +622,19 @@ function Hint_Prefetch(addr,hint,target,stream) = ()
 
 /* regular load */
 /* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_NORMAL (address, size) = __read_mem(Read_plain, 64, address, size)
 /* non-temporal load (LDNP), see ARM ARM for special exception to normal memory ordering rules */
 /* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_STREAM (address, size) = __read_mem(Read_stream, 64, address, size)
 /* load-acquire */
 /* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ORDERED (address, size) = __read_mem(Read_acquire, 64, address, size)
 /* load-exclusive */
 /* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ATOMIC (address, size) = __read_mem(Read_exclusive, 64, address, size)
 /* load-exclusive+acquire */
 /* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ATOMIC_ORDERED (address, size) = __read_mem(Read_exclusive_acquire, 64, address, size)
 
 struct read_buffer_type = {
   acctype : AccType,
@@ -678,12 +703,16 @@ function flush_read_buffer(read_buffer, size) =
 
 /* regular store */
 /* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_NORMAL (address, size) = { __write_mem_ea(Write_plain, 64, address, size); () }
 /* store-release */
 /* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ORDERED (address, size) = { __write_mem_ea(Write_release, 64, address, size); () }
 /* store-exclusive */
 /* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ATOMIC (address, size) = { __write_mem_ea(Write_exclusive, 64, address, size); () }
 /* store-exclusive+release */
 /* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ATOMIC_ORDERED (address, size) = { __write_mem_ea(Write_exclusive_release, 64, address, size); () }
 
 val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), int('N), AccType, boolean) -> unit effect {eamem, escape}
 function wMem_Addr(address, size, acctype, excl) =
@@ -701,9 +730,15 @@ function wMem_Addr(address, size, acctype, excl) =
 
 
 /* regular store */
-/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+function wMem_Val_NORMAL (address, size, value) = { let b = __write_mem(Write_plain, 64, address, size, value); () }
+/* external */ val wMem_Val_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+function wMem_Val_ORDERED (address, size, value) = { let b = __write_mem(Write_release, 64, address, size, value); () }
 /* store-exclusive */
-/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+function wMem_Val_ATOMIC (address, size, value) = __write_mem(Write_exclusive, 64, address, size, value)
+/* external */ val wMem_Val_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+function wMem_Val_ATOMIC_ORDERED (address, size, value) = __write_mem(Write_exclusive_release, 64, address, size, value)
 
 
 struct write_buffer_type = {
@@ -752,10 +787,10 @@ function flush_write_buffer(write_buffer) = {
   let s : range(0,16) = write_buffer.size;
   assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
   match write_buffer.acctype {
-    AccType_NORMAL   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_STREAM   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_UNPRIV   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_ORDERED  => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_NORMAL   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_STREAM   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_UNPRIV   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ORDERED (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
     _  => not_implemented("unrecognised memory access")
   };
 }
@@ -766,8 +801,8 @@ function flush_write_buffer_exclusive(write_buffer) = {
   let s = write_buffer.size;
   assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
   match write_buffer.acctype {
-    AccType_ATOMIC   => wMem_Val_ATOMIC(s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_ORDERED  => wMem_Val_ATOMIC(s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ATOMIC   => wMem_Val_ATOMIC(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ATOMIC_ORDERED(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
     _  => { not_implemented("unrecognised memory access"); false; }
   };
 }
@@ -947,6 +982,7 @@ function Hint_Yield() -> unit = ()
 
 /** FUNCTION:shared/functions/system/InstructionSynchronizationBarrier */
 /* external */ val InstructionSynchronizationBarrier : unit -> unit effect {barr}
+function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB)
 /** FUNCTION:shared/functions/system/InterruptPending */
 
 function InterruptPending () -> boolean = not_implemented_extern("InterruptPending")
@@ -996,19 +1032,6 @@ function SendEvent() -> unit =
   /* TODO: ??? */
 }
 
-/** FUNCTION:shared/functions/system/Unreachable */
-
-/* CP: adding two variants, one that takes a string argument, the other one doesn't  */
-val Unreachable_no_message : forall ('a : Type) . unit -> 'a effect{escape}
-function Unreachable_no_message() = 
-    error("Unreachable reached")
-
-val Unreachable_message : forall ('a : Type) . string -> 'a effect{escape}
-function Unreachable_message(message) = 
-    error(message)
-
-overload Unreachable = {Unreachable_no_message, Unreachable_message}
-
 
 /** FUNCTION:shared/functions/system/UsingAArch32 */
 
diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem
index 86570fc4..c5a1b8bc 100644
--- a/aarch64_small/armV8_extras_embed.lem
+++ b/aarch64_small/armV8_extras_embed.lem
@@ -1,47 +1,55 @@
 open import Pervasives
-open import Sail_impl_base
-open import Sail_values
-open import Prompt
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+open import ArmV8_types
 
-val rMem_NORMAL         : (vector bitU * integer) -> M (vector bitU)
-val rMem_STREAM         : (vector bitU * integer) -> M (vector bitU)
-val rMem_ORDERED        : (vector bitU * integer) -> M (vector bitU)
-val rMem_ATOMICL        : (vector bitU * integer) -> M (vector bitU)
-val rMem_ATOMIC_ORDERED : (vector bitU * integer) -> M (vector bitU)
+val rMem_NORMAL         : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val rMem_STREAM         : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val rMem_ORDERED        : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val rMem_ATOMICL        : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val rMem_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
 
-let rMem_NORMAL (addr,size)         = read_mem false Read_plain addr size
-let rMem_STREAM (addr,size)         = read_mem false Read_stream addr size
-let rMem_ORDERED (addr,size)        = read_mem false Read_acquire addr size
-let rMem_ATOMIC (addr,size)         = read_mem false Read_exclusive addr size
-let rMem_ATOMIC_ORDERED (addr,size) = read_mem false Read_exclusive_acquire addr size
+let rMem_NORMAL addr size         = read_mem Read_plain () addr size
+let rMem_STREAM addr size         = read_mem Read_stream () addr size
+let rMem_ORDERED addr size        = read_mem Read_acquire () addr size
+let rMem_ATOMIC addr size         = read_mem Read_exclusive () addr size
+let rMem_ATOMIC_ORDERED addr size = read_mem Read_exclusive_acquire () addr size
 
-val wMem_Addr_NORMAL         : (vector bitU * integer) -> M unit
-val wMem_Addr_ORDERED        : (vector bitU * integer) -> M unit
-val wMem_Addr_ATOMIC         : (vector bitU * integer) -> M unit
-val wMem_Addr_ATOMIC_ORDERED : (vector bitU * integer) -> M unit
+val wMem_Addr_NORMAL         : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
+val wMem_Addr_ORDERED        : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
+val wMem_Addr_ATOMIC         : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
+val wMem_Addr_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
 
-let wMem_Addr_NORMAL (addr,size)         = write_mem_ea Write_plain addr size
-let wMem_Addr_ORDERED (addr,size)        = write_mem_ea Write_release addr size
-let wMem_Addr_ATOMIC (addr,size)         = write_mem_ea Write_exclusive addr size
-let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_mem_ea Write_exclusive_release addr size
+let wMem_Addr_NORMAL addr size         = write_mem_ea Write_plain () addr size
+let wMem_Addr_ORDERED addr size        = write_mem_ea Write_release () addr size
+let wMem_Addr_ATOMIC addr size         = write_mem_ea Write_exclusive () addr size
+let wMem_Addr_ATOMIC_ORDERED addr size = write_mem_ea Write_exclusive_release () addr size
 
 
-val wMem_Val_NORMAL : (integer * vector bitU) -> M unit
-val wMem_Val_ATOMIC : (integer * vector bitU) -> M bitU
+val wMem_Val_NORMAL : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
+val wMem_Val_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
+val wMem_Val_ATOMIC : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e
+val wMem_Val_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e
 
-let wMem_Val_NORMAL (_,v) = write_mem_val v >>= fun _ -> return ()
+let wMem_Val_NORMAL addr size v = write_mem Write_plain () addr size v >>= fun _ -> return ()
+let wMem_Val_ORDERED addr size v = write_mem Write_release () addr size v >>= fun _ -> return ()
 (* in ARM the status returned is inversed *)
-let wMem_Val_ATOMIC (_,v) = write_mem_val v >>= fun b -> return (if b then B0 else B1)
+let wMem_Val_ATOMIC addr size v = write_mem Write_exclusive () addr size v >>= fun b -> return (not b)
+let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () addr size v >>= fun b -> return (not b)
 
-let speculate_exclusive_success () = excl_result () >>= fun b -> return (if b then B1 else B0)
+let speculate_exclusive_success () = excl_result ()
 
-val DataMemoryBarrier_Reads            : unit -> M unit
-val DataMemoryBarrier_Writes           : unit -> M unit
-val DataMemoryBarrier_All              : unit -> M unit
-val DataSynchronizationBarrier_Reads   : unit -> M unit
-val DataSynchronizationBarrier_Writes  : unit -> M unit
-val DataSynchronizationBarrier_All     : unit -> M unit
-val InstructionSynchronizationBarrier  : unit -> M unit
+val DataMemoryBarrier_Reads            : forall 'rv 'e. unit -> monad 'rv unit 'e
+val DataMemoryBarrier_Writes           : forall 'rv 'e. unit -> monad 'rv unit 'e
+val DataMemoryBarrier_All              : forall 'rv 'e. unit -> monad 'rv unit 'e
+val DataSynchronizationBarrier_Reads   : forall 'rv 'e. unit -> monad 'rv unit 'e
+val DataSynchronizationBarrier_Writes  : forall 'rv 'e. unit -> monad 'rv unit 'e
+val DataSynchronizationBarrier_All     : forall 'rv 'e. unit -> monad 'rv unit 'e
+val InstructionSynchronizationBarrier  : forall 'rv 'e. unit -> monad 'rv unit 'e
 
 let DataMemoryBarrier_Reads ()           = barrier Barrier_DMB_LD
 let DataMemoryBarrier_Writes ()          = barrier Barrier_DMB_ST
@@ -51,9 +59,8 @@ let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST
 let DataSynchronizationBarrier_All ()    = barrier Barrier_DSB
 let InstructionSynchronizationBarrier () = barrier Barrier_ISB
 
-val TMCommitEffect : unit -> M unit
+val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e
 let TMCommitEffect () = barrier Barrier_TM_COMMIT
 
-let duplicate_bits (Vector bits start direction,len) =
-  let bits' = repeat bits len in
-  Vector bits' start direction
+val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type
+let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |>
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 332ad18c..5ace3f01 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -179,7 +179,6 @@ val Halted : unit -> boolean effect {rreg}
 val HaveEL : bits(2) -> boolean effect {escape}
 val HaveAnyAArch32 : unit -> boolean effect pure
 val HighestELUsingAArch32 : unit -> boolean effect pure
-val Unreachable : unit -> unit effect {escape}
 val Hint_Branch : BranchType -> unit effect pure
 
 /*************************************************************************/
diff --git a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
index b8fe851c..2d0ac5e2 100644
--- a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
+++ b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
@@ -1,20 +1,20 @@
-| `AArch64Unallocated -> Unallocated
+| `AArch64Unallocated -> Unallocated ()
 | `AArch64TMStart t -> TMStart (translate_reg "t" t)
 
-| `AArch64TMCommit -> TMCommit
+| `AArch64TMCommit -> TMCommit ()
 
 | `AArch64TMAbort (retry,reason) ->
     TMAbort
-      (translate_boolean "retry" retry,
+      (translate_bool "retry" retry,
         translate_bit5 "reason" reason)
 
-| `AArch64TMTest -> TMTest
+| `AArch64TMTest -> TMTest ()
 
 | `AArch64ImplementationDefinedStopFetching ->
-    ImplementationDefinedStopFetching
+    ImplementationDefinedStopFetching ()
 
 | `AArch64ImplementationDefinedThreadStart ->
-    ImplementationDefinedThreadStart
+    ImplementationDefinedThreadStart ()
 
 | `AArch64ImplementationDefinedTestBeginEnd(isEnd) ->
     ImplementationDefinedTestBeginEnd
diff --git a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
index e14a37e3..6ca50f83 100644
--- a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
+++ b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
@@ -1,4 +1,4 @@
-open Sail_values
+open Sail2_values
 
 let is_inc = false
 
@@ -6,16 +6,16 @@ let translate_big_int bits (name : string) value =
   (name, Range0 (Some bits), IInt.bit_list_of_integer bits value)
 
 let translate_big_bit bits (name:string) value =
-  Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,value)
+  Sail2_values.bits_of_int (Nat_big_num.of_int bits) value
 
 let translate_int (size : int) (name:string) value = (Nat_big_num.of_int value)
 
 let translate_bits bits (name:string) value =
-  Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,Nat_big_num.of_int value)
+  Sail2_values.bits_of_int (Nat_big_num.of_int bits) (Nat_big_num.of_int value)
 
 let translate_bool _ = function
-  | true -> B1
-  | false -> B0
+  | true -> B10
+  | false -> B00
 
 let translate_reg_size name value =
   match value with
@@ -59,95 +59,95 @@ let translate_range8_64 = translate_int 7
 let translate_uinteger = translate_int 63
 
 let translate_extendType _ = function
-  | ExtendType_UXTB -> ArmV8_embed_types.ExtendType_UXTB
-  | ExtendType_UXTH -> ArmV8_embed_types.ExtendType_UXTH
-  | ExtendType_UXTW -> ArmV8_embed_types.ExtendType_UXTW
-  | ExtendType_UXTX -> ArmV8_embed_types.ExtendType_UXTX
-  | ExtendType_SXTB -> ArmV8_embed_types.ExtendType_SXTB
-  | ExtendType_SXTH -> ArmV8_embed_types.ExtendType_SXTH
-  | ExtendType_SXTW -> ArmV8_embed_types.ExtendType_SXTW
-  | ExtendType_SXTX -> ArmV8_embed_types.ExtendType_SXTX
+  | ExtendType_UXTB -> ArmV8_types.ExtendType_UXTB
+  | ExtendType_UXTH -> ArmV8_types.ExtendType_UXTH
+  | ExtendType_UXTW -> ArmV8_types.ExtendType_UXTW
+  | ExtendType_UXTX -> ArmV8_types.ExtendType_UXTX
+  | ExtendType_SXTB -> ArmV8_types.ExtendType_SXTB
+  | ExtendType_SXTH -> ArmV8_types.ExtendType_SXTH
+  | ExtendType_SXTW -> ArmV8_types.ExtendType_SXTW
+  | ExtendType_SXTX -> ArmV8_types.ExtendType_SXTX
 
 let translate_shiftType _ = function
-  | ShiftType_LSL -> ArmV8_embed_types.ShiftType_LSL
-  | ShiftType_LSR -> ArmV8_embed_types.ShiftType_LSR
-  | ShiftType_ASR -> ArmV8_embed_types.ShiftType_ASR
-  | ShiftType_ROR -> ArmV8_embed_types.ShiftType_ROR
+  | ShiftType_LSL -> ArmV8_types.ShiftType_LSL
+  | ShiftType_LSR -> ArmV8_types.ShiftType_LSR
+  | ShiftType_ASR -> ArmV8_types.ShiftType_ASR
+  | ShiftType_ROR -> ArmV8_types.ShiftType_ROR
 
 let translate_logicalOp _ = function
-  | LogicalOp_AND -> ArmV8_embed_types.LogicalOp_AND
-  | LogicalOp_EOR -> ArmV8_embed_types.LogicalOp_EOR
-  | LogicalOp_ORR -> ArmV8_embed_types.LogicalOp_ORR
+  | LogicalOp_AND -> ArmV8_types.LogicalOp_AND
+  | LogicalOp_EOR -> ArmV8_types.LogicalOp_EOR
+  | LogicalOp_ORR -> ArmV8_types.LogicalOp_ORR
 
 let translate_branchType _ = function
-  | BranchType_CALL -> ArmV8_embed_types.BranchType_CALL
-  | BranchType_ERET -> ArmV8_embed_types.BranchType_ERET
-  | BranchType_DBGEXIT -> ArmV8_embed_types.BranchType_DBGEXIT
-  | BranchType_RET -> ArmV8_embed_types.BranchType_RET
-  | BranchType_JMP -> ArmV8_embed_types.BranchType_JMP
-  | BranchType_EXCEPTION -> ArmV8_embed_types.BranchType_EXCEPTION
-  | BranchType_UNKNOWN -> ArmV8_embed_types.BranchType_UNKNOWN
+  | BranchType_CALL -> ArmV8_types.BranchType_CALL
+  | BranchType_ERET -> ArmV8_types.BranchType_ERET
+  | BranchType_DBGEXIT -> ArmV8_types.BranchType_DBGEXIT
+  | BranchType_RET -> ArmV8_types.BranchType_RET
+  | BranchType_JMP -> ArmV8_types.BranchType_JMP
+  | BranchType_EXCEPTION -> ArmV8_types.BranchType_EXCEPTION
+  | BranchType_UNKNOWN -> ArmV8_types.BranchType_UNKNOWN
 
 let translate_countOp _ = function
-  | CountOp_CLZ -> ArmV8_embed_types.CountOp_CLZ
-  | CountOp_CLS -> ArmV8_embed_types.CountOp_CLS
-  | CountOp_CNT -> ArmV8_embed_types.CountOp_CNT
+  | CountOp_CLZ -> ArmV8_types.CountOp_CLZ
+  | CountOp_CLS -> ArmV8_types.CountOp_CLS
+  | CountOp_CNT -> ArmV8_types.CountOp_CNT
 
 let translate_memBarrierOp _ = function
-  | MemBarrierOp_DSB -> ArmV8_embed_types.MemBarrierOp_DSB
-  | MemBarrierOp_DMB -> ArmV8_embed_types.MemBarrierOp_DMB
-  | MemBarrierOp_ISB -> ArmV8_embed_types.MemBarrierOp_ISB
+  | MemBarrierOp_DSB -> ArmV8_types.MemBarrierOp_DSB
+  | MemBarrierOp_DMB -> ArmV8_types.MemBarrierOp_DMB
+  | MemBarrierOp_ISB -> ArmV8_types.MemBarrierOp_ISB
 
 let translate_mBReqDomain _ = function
-  | MBReqDomain_Nonshareable -> ArmV8_embed_types.MBReqDomain_Nonshareable
-  | MBReqDomain_InnerShareable -> ArmV8_embed_types.MBReqDomain_InnerShareable
-  | MBReqDomain_OuterShareable -> ArmV8_embed_types.MBReqDomain_OuterShareable
-  | MBReqDomain_FullSystem -> ArmV8_embed_types.MBReqDomain_FullSystem
+  | MBReqDomain_Nonshareable -> ArmV8_types.MBReqDomain_Nonshareable
+  | MBReqDomain_InnerShareable -> ArmV8_types.MBReqDomain_InnerShareable
+  | MBReqDomain_OuterShareable -> ArmV8_types.MBReqDomain_OuterShareable
+  | MBReqDomain_FullSystem -> ArmV8_types.MBReqDomain_FullSystem
 
 let translate_mBReqTypes _ = function
-  | MBReqTypes_Reads -> ArmV8_embed_types.MBReqTypes_Reads
-  | MBReqTypes_Writes -> ArmV8_embed_types.MBReqTypes_Writes
-  | MBReqTypes_All -> ArmV8_embed_types.MBReqTypes_All
+  | MBReqTypes_Reads -> ArmV8_types.MBReqTypes_Reads
+  | MBReqTypes_Writes -> ArmV8_types.MBReqTypes_Writes
+  | MBReqTypes_All -> ArmV8_types.MBReqTypes_All
 
 let translate_systemHintOp _ = function
-  | SystemHintOp_NOP -> ArmV8_embed_types.SystemHintOp_NOP
-  | SystemHintOp_YIELD -> ArmV8_embed_types.SystemHintOp_YIELD
-  | SystemHintOp_WFE -> ArmV8_embed_types.SystemHintOp_WFE
-  | SystemHintOp_WFI -> ArmV8_embed_types.SystemHintOp_WFI
-  | SystemHintOp_SEV -> ArmV8_embed_types.SystemHintOp_SEV
-  | SystemHintOp_SEVL -> ArmV8_embed_types.SystemHintOp_SEVL
+  | SystemHintOp_NOP -> ArmV8_types.SystemHintOp_NOP
+  | SystemHintOp_YIELD -> ArmV8_types.SystemHintOp_YIELD
+  | SystemHintOp_WFE -> ArmV8_types.SystemHintOp_WFE
+  | SystemHintOp_WFI -> ArmV8_types.SystemHintOp_WFI
+  | SystemHintOp_SEV -> ArmV8_types.SystemHintOp_SEV
+  | SystemHintOp_SEVL -> ArmV8_types.SystemHintOp_SEVL
 
 let translate_accType _ = function
-  | AccType_NORMAL -> ArmV8_embed_types.AccType_NORMAL
-  | AccType_VEC -> ArmV8_embed_types.AccType_VEC
-  | AccType_STREAM -> ArmV8_embed_types.AccType_STREAM
-  | AccType_VECSTREAM -> ArmV8_embed_types.AccType_VECSTREAM
-  | AccType_ATOMIC -> ArmV8_embed_types.AccType_ATOMIC
-  | AccType_ORDERED -> ArmV8_embed_types.AccType_ORDERED
-  | AccType_UNPRIV -> ArmV8_embed_types.AccType_UNPRIV
-  | AccType_IFETCH -> ArmV8_embed_types.AccType_IFETCH
-  | AccType_PTW -> ArmV8_embed_types.AccType_PTW
-  | AccType_DC -> ArmV8_embed_types.AccType_DC
-  | AccType_IC -> ArmV8_embed_types.AccType_IC
-  | AccType_AT -> ArmV8_embed_types.AccType_AT
+  | AccType_NORMAL -> ArmV8_types.AccType_NORMAL
+  | AccType_VEC -> ArmV8_types.AccType_VEC
+  | AccType_STREAM -> ArmV8_types.AccType_STREAM
+  | AccType_VECSTREAM -> ArmV8_types.AccType_VECSTREAM
+  | AccType_ATOMIC -> ArmV8_types.AccType_ATOMIC
+  | AccType_ORDERED -> ArmV8_types.AccType_ORDERED
+  | AccType_UNPRIV -> ArmV8_types.AccType_UNPRIV
+  | AccType_IFETCH -> ArmV8_types.AccType_IFETCH
+  | AccType_PTW -> ArmV8_types.AccType_PTW
+  | AccType_DC -> ArmV8_types.AccType_DC
+  | AccType_IC -> ArmV8_types.AccType_IC
+  | AccType_AT -> ArmV8_types.AccType_AT
 
 let translate_memOp _ = function
-  | MemOp_LOAD -> ArmV8_embed_types.MemOp_LOAD
-  | MemOp_STORE -> ArmV8_embed_types.MemOp_STORE
-  | MemOp_PREFETCH -> ArmV8_embed_types.MemOp_PREFETCH
+  | MemOp_LOAD -> ArmV8_types.MemOp_LOAD
+  | MemOp_STORE -> ArmV8_types.MemOp_STORE
+  | MemOp_PREFETCH -> ArmV8_types.MemOp_PREFETCH
 
 let translate_moveWideOp _ = function
-  | MoveWideOp_N -> ArmV8_embed_types.MoveWideOp_N
-  | MoveWideOp_Z -> ArmV8_embed_types.MoveWideOp_Z
-  | MoveWideOp_K -> ArmV8_embed_types.MoveWideOp_K
+  | MoveWideOp_N -> ArmV8_types.MoveWideOp_N
+  | MoveWideOp_Z -> ArmV8_types.MoveWideOp_Z
+  | MoveWideOp_K -> ArmV8_types.MoveWideOp_K
 
 let translate_revOp _ = function
-  | RevOp_RBIT -> ArmV8_embed_types.RevOp_RBIT
-  | RevOp_REV16 -> ArmV8_embed_types.RevOp_REV16
-  | RevOp_REV32 -> ArmV8_embed_types.RevOp_REV32
-  | RevOp_REV64 -> ArmV8_embed_types.RevOp_REV64
+  | RevOp_RBIT -> ArmV8_types.RevOp_RBIT
+  | RevOp_REV16 -> ArmV8_types.RevOp_REV16
+  | RevOp_REV32 -> ArmV8_types.RevOp_REV32
+  | RevOp_REV64 -> ArmV8_types.RevOp_REV64
 
 let translate_pSTATEField _ = function
-  | PSTATEField_DAIFSet -> ArmV8_embed_types.PSTATEField_DAIFSet
-  | PSTATEField_DAIFClr -> ArmV8_embed_types.PSTATEField_DAIFClr
-  | PSTATEField_SP -> ArmV8_embed_types.PSTATEField_SP
+  | PSTATEField_DAIFSet -> ArmV8_types.PSTATEField_DAIFSet
+  | PSTATEField_DAIFClr -> ArmV8_types.PSTATEField_DAIFClr
+  | PSTATEField_SP -> ArmV8_types.PSTATEField_SP
diff --git a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
index 55179a97..96b74b4f 100644
--- a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
+++ b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
@@ -1,20 +1,20 @@
-| Unallocated -> `AArch64Unallocated
+| Unallocated () -> `AArch64Unallocated
 
 | TMStart t ->
   `AArch64TMStart (translate_out_regzr Set64 t)
 
-| TMCommit -> `AArch64TMCommit
+| TMCommit () -> `AArch64TMCommit
 
 | TMAbort (retry, reason) ->
   `AArch64TMAbort ( translate_out_bool retry,
                     translate_out_bits reason)
 
-| TMTest -> `AArch64TMTest
+| TMTest () -> `AArch64TMTest
 
-| ImplementationDefinedStopFetching ->
+| ImplementationDefinedStopFetching () ->
   `AArch64ImplementationDefinedStopFetching
 
-| ImplementationDefinedThreadStart ->
+| ImplementationDefinedThreadStart () ->
   `AArch64ImplementationDefinedThreadStart
 
 | ImplementationDefinedTestBeginEnd (isEnd) ->
diff --git a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
index 771f52ac..a26879b4 100644
--- a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
+++ b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
@@ -1,17 +1,17 @@
-let translate_out_big_int_bits x = Sail_values.unsigned x
+let translate_out_big_int_bits bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
-let translate_out_big_bit = Sail_values.unsigned
+let translate_out_big_bit bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
-let translate_out_signed_big_bit = Sail_values.signed
+let translate_out_signed_big_bit bits = (match Sail2_values.signed_of_bits bits with Some x -> x | None -> failwith "signed_of_bits returned None")
 
 let translate_out_int inst = (Nat_big_num.to_int inst)
 
-let translate_out_bits bits = Nat_big_num.to_int (Sail_values.unsigned bits)
+let translate_out_bits bits = Nat_big_num.to_int (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
 let translate_out_bool = function
-  | Sail_values.B1 -> true
-  | Sail_values.B0 -> false
-  | Sail_values.BU -> failwith "translate_out_bool Undef"
+  | Sail2_values.B10 -> true
+  | Sail2_values.B00 -> false
+  | Sail2_values.BU0 -> failwith "translate_out_bool Undef"
 
 let translate_out_enum (name,_,bits) =
     Nat_big_num.to_int (IInt.integer_of_bit_list bits)
@@ -44,7 +44,7 @@ let translate_out_regzrbyext regsize extend_type reg =  begin match extend_type
   end
 
 let translate_out_reg_size_bits bits =
-  match Nat_big_num.to_int (Sail_values.length bits) with
+  match (List.length bits) with
     | 32 -> R32Bits (translate_out_bits bits)
     | 64 -> R64Bits (translate_out_big_bit bits)
     | _ -> assert false
@@ -58,97 +58,97 @@ let translate_out_data_size inst =
     | _ -> assert false
 
 let translate_out_extendType = function
-    | ArmV8_embed_types.ExtendType_UXTB -> ExtendType_UXTB
-    | ArmV8_embed_types.ExtendType_UXTH -> ExtendType_UXTH
-    | ArmV8_embed_types.ExtendType_UXTW -> ExtendType_UXTW
-    | ArmV8_embed_types.ExtendType_UXTX -> ExtendType_UXTX
-    | ArmV8_embed_types.ExtendType_SXTB -> ExtendType_SXTB
-    | ArmV8_embed_types.ExtendType_SXTH -> ExtendType_SXTH
-    | ArmV8_embed_types.ExtendType_SXTW -> ExtendType_SXTW
-    | ArmV8_embed_types.ExtendType_SXTX -> ExtendType_SXTX
+    | ArmV8_types.ExtendType_UXTB -> ExtendType_UXTB
+    | ArmV8_types.ExtendType_UXTH -> ExtendType_UXTH
+    | ArmV8_types.ExtendType_UXTW -> ExtendType_UXTW
+    | ArmV8_types.ExtendType_UXTX -> ExtendType_UXTX
+    | ArmV8_types.ExtendType_SXTB -> ExtendType_SXTB
+    | ArmV8_types.ExtendType_SXTH -> ExtendType_SXTH
+    | ArmV8_types.ExtendType_SXTW -> ExtendType_SXTW
+    | ArmV8_types.ExtendType_SXTX -> ExtendType_SXTX
 
 let translate_out_shiftType = function
-    | ArmV8_embed_types.ShiftType_LSL -> ShiftType_LSL
-    | ArmV8_embed_types.ShiftType_LSR -> ShiftType_LSR
-    | ArmV8_embed_types.ShiftType_ASR -> ShiftType_ASR
-    | ArmV8_embed_types.ShiftType_ROR -> ShiftType_ROR
+    | ArmV8_types.ShiftType_LSL -> ShiftType_LSL
+    | ArmV8_types.ShiftType_LSR -> ShiftType_LSR
+    | ArmV8_types.ShiftType_ASR -> ShiftType_ASR
+    | ArmV8_types.ShiftType_ROR -> ShiftType_ROR
 
 let translate_out_logicalOp = function
-    | ArmV8_embed_types.LogicalOp_AND -> LogicalOp_AND
-    | ArmV8_embed_types.LogicalOp_EOR -> LogicalOp_EOR
-    | ArmV8_embed_types.LogicalOp_ORR -> LogicalOp_ORR
+    | ArmV8_types.LogicalOp_AND -> LogicalOp_AND
+    | ArmV8_types.LogicalOp_EOR -> LogicalOp_EOR
+    | ArmV8_types.LogicalOp_ORR -> LogicalOp_ORR
 
 let translate_out_branchType = function
-      | ArmV8_embed_types.BranchType_CALL -> BranchType_CALL
-      | ArmV8_embed_types.BranchType_ERET -> BranchType_ERET
-      | ArmV8_embed_types.BranchType_DBGEXIT -> BranchType_DBGEXIT
-      | ArmV8_embed_types.BranchType_RET -> BranchType_RET
-      | ArmV8_embed_types.BranchType_JMP -> BranchType_JMP
-      | ArmV8_embed_types.BranchType_EXCEPTION -> BranchType_EXCEPTION
-      | ArmV8_embed_types.BranchType_UNKNOWN -> BranchType_UNKNOWN
+      | ArmV8_types.BranchType_CALL -> BranchType_CALL
+      | ArmV8_types.BranchType_ERET -> BranchType_ERET
+      | ArmV8_types.BranchType_DBGEXIT -> BranchType_DBGEXIT
+      | ArmV8_types.BranchType_RET -> BranchType_RET
+      | ArmV8_types.BranchType_JMP -> BranchType_JMP
+      | ArmV8_types.BranchType_EXCEPTION -> BranchType_EXCEPTION
+      | ArmV8_types.BranchType_UNKNOWN -> BranchType_UNKNOWN
 
 let translate_out_countOp = function
-    | ArmV8_embed_types.CountOp_CLZ -> CountOp_CLZ
-    | ArmV8_embed_types.CountOp_CLS -> CountOp_CLS
-    | ArmV8_embed_types.CountOp_CNT -> CountOp_CNT
+    | ArmV8_types.CountOp_CLZ -> CountOp_CLZ
+    | ArmV8_types.CountOp_CLS -> CountOp_CLS
+    | ArmV8_types.CountOp_CNT -> CountOp_CNT
 
 let translate_out_memBarrierOp = function
-    | ArmV8_embed_types.MemBarrierOp_DSB -> MemBarrierOp_DSB
-    | ArmV8_embed_types.MemBarrierOp_DMB -> MemBarrierOp_DMB
-    | ArmV8_embed_types.MemBarrierOp_ISB -> MemBarrierOp_ISB
+    | ArmV8_types.MemBarrierOp_DSB -> MemBarrierOp_DSB
+    | ArmV8_types.MemBarrierOp_DMB -> MemBarrierOp_DMB
+    | ArmV8_types.MemBarrierOp_ISB -> MemBarrierOp_ISB
 
 let translate_out_mBReqDomain = function
-    | ArmV8_embed_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable
-    | ArmV8_embed_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable
-    | ArmV8_embed_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable
-    | ArmV8_embed_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem
+    | ArmV8_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable
+    | ArmV8_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable
+    | ArmV8_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable
+    | ArmV8_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem
 
 let translate_out_mBReqTypes = function
-    | ArmV8_embed_types.MBReqTypes_Reads -> MBReqTypes_Reads
-    | ArmV8_embed_types.MBReqTypes_Writes -> MBReqTypes_Writes
-    | ArmV8_embed_types.MBReqTypes_All -> MBReqTypes_All
+    | ArmV8_types.MBReqTypes_Reads -> MBReqTypes_Reads
+    | ArmV8_types.MBReqTypes_Writes -> MBReqTypes_Writes
+    | ArmV8_types.MBReqTypes_All -> MBReqTypes_All
 
 let translate_out_systemHintOp = function
-    | ArmV8_embed_types.SystemHintOp_NOP -> SystemHintOp_NOP
-    | ArmV8_embed_types.SystemHintOp_YIELD -> SystemHintOp_YIELD
-    | ArmV8_embed_types.SystemHintOp_WFE -> SystemHintOp_WFE
-    | ArmV8_embed_types.SystemHintOp_WFI -> SystemHintOp_WFI
-    | ArmV8_embed_types.SystemHintOp_SEV -> SystemHintOp_SEV
-    | ArmV8_embed_types.SystemHintOp_SEVL -> SystemHintOp_SEVL
+    | ArmV8_types.SystemHintOp_NOP -> SystemHintOp_NOP
+    | ArmV8_types.SystemHintOp_YIELD -> SystemHintOp_YIELD
+    | ArmV8_types.SystemHintOp_WFE -> SystemHintOp_WFE
+    | ArmV8_types.SystemHintOp_WFI -> SystemHintOp_WFI
+    | ArmV8_types.SystemHintOp_SEV -> SystemHintOp_SEV
+    | ArmV8_types.SystemHintOp_SEVL -> SystemHintOp_SEVL
 
 let translate_out_accType = function
-    | ArmV8_embed_types.AccType_NORMAL  -> AccType_NORMAL
-    | ArmV8_embed_types.AccType_VEC  -> AccType_VEC
-    | ArmV8_embed_types.AccType_STREAM  -> AccType_STREAM
-    | ArmV8_embed_types.AccType_VECSTREAM  -> AccType_VECSTREAM
-    | ArmV8_embed_types.AccType_ATOMIC  -> AccType_ATOMIC
-    | ArmV8_embed_types.AccType_ORDERED  -> AccType_ORDERED
-    | ArmV8_embed_types.AccType_UNPRIV  -> AccType_UNPRIV
-    | ArmV8_embed_types.AccType_IFETCH  -> AccType_IFETCH
-    | ArmV8_embed_types.AccType_PTW  -> AccType_PTW
-    | ArmV8_embed_types.AccType_DC  -> AccType_DC
-    | ArmV8_embed_types.AccType_IC -> AccType_IC
-    | ArmV8_embed_types.AccType_AT -> AccType_AT
+    | ArmV8_types.AccType_NORMAL  -> AccType_NORMAL
+    | ArmV8_types.AccType_VEC  -> AccType_VEC
+    | ArmV8_types.AccType_STREAM  -> AccType_STREAM
+    | ArmV8_types.AccType_VECSTREAM  -> AccType_VECSTREAM
+    | ArmV8_types.AccType_ATOMIC  -> AccType_ATOMIC
+    | ArmV8_types.AccType_ORDERED  -> AccType_ORDERED
+    | ArmV8_types.AccType_UNPRIV  -> AccType_UNPRIV
+    | ArmV8_types.AccType_IFETCH  -> AccType_IFETCH
+    | ArmV8_types.AccType_PTW  -> AccType_PTW
+    | ArmV8_types.AccType_DC  -> AccType_DC
+    | ArmV8_types.AccType_IC -> AccType_IC
+    | ArmV8_types.AccType_AT -> AccType_AT
 
 let translate_out_memOp = function
-    | ArmV8_embed_types.MemOp_LOAD -> MemOp_LOAD
-    | ArmV8_embed_types.MemOp_STORE -> MemOp_STORE
-    | ArmV8_embed_types.MemOp_PREFETCH -> MemOp_PREFETCH
+    | ArmV8_types.MemOp_LOAD -> MemOp_LOAD
+    | ArmV8_types.MemOp_STORE -> MemOp_STORE
+    | ArmV8_types.MemOp_PREFETCH -> MemOp_PREFETCH
 
 
 let translate_out_moveWideOp = function
-    | ArmV8_embed_types.MoveWideOp_N -> MoveWideOp_N
-    | ArmV8_embed_types.MoveWideOp_Z -> MoveWideOp_Z
-    | ArmV8_embed_types.MoveWideOp_K -> MoveWideOp_K
+    | ArmV8_types.MoveWideOp_N -> MoveWideOp_N
+    | ArmV8_types.MoveWideOp_Z -> MoveWideOp_Z
+    | ArmV8_types.MoveWideOp_K -> MoveWideOp_K
 
 let translate_out_revOp = function
-    | ArmV8_embed_types.RevOp_RBIT -> RevOp_RBIT
-    | ArmV8_embed_types.RevOp_REV16 -> RevOp_REV16
-    | ArmV8_embed_types.RevOp_REV32 -> RevOp_REV32
-    | ArmV8_embed_types.RevOp_REV64 -> RevOp_REV64
+    | ArmV8_types.RevOp_RBIT -> RevOp_RBIT
+    | ArmV8_types.RevOp_REV16 -> RevOp_REV16
+    | ArmV8_types.RevOp_REV32 -> RevOp_REV32
+    | ArmV8_types.RevOp_REV64 -> RevOp_REV64
 
 let translate_out_pSTATEField = function
-    | ArmV8_embed_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet
-    | ArmV8_embed_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr
-    | ArmV8_embed_types.PSTATEField_SP -> PSTATEField_SP
+    | ArmV8_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet
+    | ArmV8_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr
+    | ArmV8_types.PSTATEField_SP -> PSTATEField_SP
 
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index f97c84a6..d94112ad 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -20,7 +20,7 @@ $include <flow.sail>
 $include <arith.sail>
 $include <option.sail>
 $include <vector_dec.sail>
-
+$include <regfp.sail>
 
 infix 7 >>
 infix 7 <<
@@ -67,15 +67,15 @@ overload pow2 = {pow2_atom, pow2_int}
 val cast cast_bool_bit : bool -> bit
 function cast_bool_bit(b) = 
   match b {
-    true => b0,
-    false => b1
+    true => b1,
+    false => b0
   }
 
 val cast cast_bit_bool : bit -> bool
 function cast_bit_bool (b) = 
   match b {
-    b0 => false,
-    b1 => true
+    bitzero => false,
+    bitone => true
   }
 
 
@@ -104,16 +104,16 @@ function neq_anything (x, y) = not_bool(x == y)
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
 
-val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
+val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
 overload operator + = {add_int, add_vec, add_vec_int}
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
+val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
   (int('n), int('m)) -> int('n - 'm)
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
-	       lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
+	       interpreter: "sub_nat", lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
             : (nat, nat) -> nat
 val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
@@ -124,9 +124,9 @@ overload operator - = {sub_int, sub_vec, sub_vec_int}
 /* function reg_index x = unsigned(x) */
 
 
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : 
+val quotient_nat = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : 
     forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> int(div('M,'N))
-val quotient = {ocaml: "quotient", lem: "integerDiv"} : 
+val quotient = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : 
     forall 'M 'N. (int('M), int('N)) -> int(div('M,'N))
 overload quot = {quotient_nat, quotient}
 
@@ -142,13 +142,13 @@ function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
 val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
+val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
 
 overload operator ^ = {xor_vec, int_power, concat_str}
 
 
 val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l)
-
+function mask(len, bv) = sail_mask(len, bv)
 
 overload operator % = {emod_int}
 overload operator / = {ediv_int}
@@ -165,4 +165,4 @@ function error(message) = {
 type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. int('O)}
 
 
-val appendL : forall ('a:Type). (list('a),list('a)) -> list('a)
+val appendL = {ocaml: "append", interpreter: "append_list", lem: "append_list"} : forall ('a:Type). (list('a),list('a)) -> list('a)
diff --git a/lib/regfp.sail b/lib/regfp.sail
index e9bcf807..de35d67a 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -124,7 +124,7 @@ val __write_mem
   = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
 val __excl_res
-  = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_res" }
+  = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
   : unit -> bool effect {exmem}
 val __barrier
   = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 33af1be7..12777506 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1457,7 +1457,10 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
         initial_check.ml. i.e. the rewriter should only encounter this
         case when re-writing those functions. *)
      wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ
-  | Typ_internal_unknown | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *)
+  | Typ_internal_unknown -> assert false
+  | Typ_bidir _ -> assert false
+  | Typ_fn _ -> assert false
+  | Typ_exist _ -> assert false (* Typ_exist should be re-written *)
 and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
@@ -2141,3 +2144,13 @@ let rec find_annot_defs sl = function
 
 let rec find_annot_ast sl (Defs defs) = find_annot_defs sl defs
 
+let string_of_lx lx =
+  let open Lexing in
+  Printf.sprintf "%s,%d,%d,%d" lx.pos_fname lx.pos_lnum lx.pos_bol lx.pos_cnum
+
+let rec simple_string_of_loc = function
+  | Parse_ast.Unknown -> "Unknown"
+  | Parse_ast.Unique (n, l) -> "Unique(" ^ string_of_int n ^ ", " ^ simple_string_of_loc l ^ ")"
+  | Parse_ast.Generated l -> "Generated(" ^ simple_string_of_loc l ^ ")"
+  | Parse_ast.Range (lx1,lx2) -> "Range(" ^ string_of_lx lx1 ^ "->" ^ string_of_lx lx2 ^ ")"
+  | Parse_ast.Documented (_,l) -> "Documented(_," ^ simple_string_of_loc l ^ ")"
diff --git a/src/ast_util.mli b/src/ast_util.mli
index cfbc26fe..c8f3cc5c 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -523,3 +523,5 @@ val subst_kids_typ_arg : nexp KBindings.t -> typ_arg -> typ_arg
 
 val quant_item_subst_kid : kid -> kid -> quant_item -> quant_item
 val typquant_subst_kid : kid -> kid -> typquant -> typquant
+
+val simple_string_of_loc : Parse_ast.l -> string
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 9acfeb26..db4f45f6 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -388,14 +388,14 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
                read_reg regname >>= fun v -> return (exp_of_value v)
             | "read_mem" ->
                begin match evaluated with
-               | [rk; addr; len] ->
+               | [rk; addrsize; addr; len] ->
                   read_mem (value_of_exp rk) (value_of_exp addr) (value_of_exp len) >>= fun v -> return (exp_of_value v)
                | _ ->
                   fail "Wrong number of parameters to read_mem intrinsic"
                end
             | "write_mem_ea" ->
                begin match evaluated with
-               | [wk; addr; len] ->
+               | [wk; addrsize; addr; len] ->
                   write_ea (value_of_exp wk) (value_of_exp addr) (value_of_exp len) >> wrap unit_exp
                | _ ->
                   fail "Wrong number of parameters to write_ea intrinsic"
@@ -409,7 +409,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
                end
             | "write_mem" ->
                begin match evaluated with
-               | [wk; addr; len; v] ->
+               | [wk; addrsize; addr; len; v] ->
                   write_mem (value_of_exp wk) (value_of_exp v) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b))
                | _ ->
                   fail "Wrong number of parameters to write_memv intrinsic"
diff --git a/src/libsail.mllib b/src/libsail.mllib
index 1a992391..b9d91834 100644
--- a/src/libsail.mllib
+++ b/src/libsail.mllib
@@ -51,7 +51,8 @@ Spec_analysis
 Specialize
 State
 ToFromInterp_backend
-ToFromInterp_lib
+ToFromInterp_lib_mword
+ToFromInterp_lib_bitlist
 Type_check
 Type_error
 Util
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 708749cc..5306e07c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1192,6 +1192,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
       | Id_aux ((Id "barrier_kind"),_) -> empty
       | Id_aux ((Id "trans_kind"),_) -> empty
       | Id_aux ((Id "instruction_kind"),_) -> empty
+      | Id_aux ((Id "cache_op_kind"),_) -> empty
       | Id_aux ((Id "regfp"),_) -> empty
       | Id_aux ((Id "niafp"),_) -> empty
       | Id_aux ((Id "diafp"),_) -> empty
diff --git a/src/sail.ml b/src/sail.ml
index daec1fdb..eff90fa3 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -95,6 +95,9 @@ let options = Arg.align ([
   ( "-tofrominterp_lem",
     Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.lem_mode],
     " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp");
+  ( "-tofrominterp_mwords",
+    Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.mword_mode],
+    " output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp");
   ( "-tofrominterp_output_dir",
     Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir),
     " set a custom directory to output embedding translation OCaml");
@@ -202,6 +205,9 @@ let options = Arg.align ([
   ( "-Oaarch64_fast",
     Arg.Set Jib_compile.optimize_aarch64_fast_struct,
     " apply ARMv8.5 specific optimizations (potentially unsound in general)");
+  ( "-Ofast_undefined",
+    Arg.Set Initial_check.opt_fast_undefined,
+    " turn on fast-undefined mode");
   ( "-static",
     Arg.Set C_backend.opt_static,
     " make generated C functions static");
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 61e62d76..13ed491b 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -1,5 +1,12 @@
 module Big_int = Nat_big_num
 
+(* for ToFromInterp_lib_foo *)
+module type BitType = sig
+  type t
+  val b0 : t
+  val b1 : t
+end
+
 type 'a return = { return : 'b . 'a -> 'b }
 type 'za zoption = | ZNone of unit | ZSome of 'za;;
 
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
index d65aaf3b..6b8fede4 100644
--- a/src/toFromInterp_backend.ml
+++ b/src/toFromInterp_backend.ml
@@ -57,10 +57,29 @@ open Pretty_print_common
 open Ocaml_backend
 
 let lem_mode = ref false
+let mword_mode = ref false
 
 let maybe_zencode s = if !lem_mode then String.uncapitalize_ascii s else zencode_string s
 let maybe_zencode_upper s = if !lem_mode then String.capitalize_ascii s else zencode_upper_string s
 
+let rec rewriteExistential (kids : kinded_id list) (Typ_aux (typ_aux, annot) as typ) =
+  print_endline (string_of_typ typ);
+  match typ_aux with
+  | Typ_tup typs -> Typ_aux (Typ_tup (List.map (rewriteExistential kids) typs), annot)
+  | Typ_exist _ -> Reporting.unreachable annot __POS__ "nested Typ_exist in rewriteExistential"
+  | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid, _)), _)])
+       when (string_of_id id = "atom" || string_of_id id = "int") ->
+              (* List.exists (fun k -> string_of_kid (kopt_kid k) = string_of_kid kid) kids -> *)
+     print_endline("*** rewriting to int - kid is '" ^ string_of_kid kid ^ "'" );
+     Typ_aux (Typ_id (mk_id "int"), annot)
+  | Typ_internal_unknown
+    | Typ_id _
+    | Typ_var _
+    | Typ_fn _
+    | Typ_bidir _
+    | Typ_app _ ->
+     typ
+
 let frominterp_typedef (TD_aux (td_aux, (l, _))) =
   let fromValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with
     | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs))])
@@ -79,20 +98,30 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
     | A_typ typ -> fromValueTyp typ ""
     | A_nexp nexp -> fromValueNexp nexp
     | A_order order -> string ("Order_" ^ (string_of_order order))
-    | _ -> string "TYP_ARG"
+    | A_bool _ -> parens (string "boolFromInterpValue")
   and fromValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with
     | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string ("FromInterpValue"); space; string arg_name])
     (* special case bit vectors for lem *)
     | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _);
                                          A_aux (A_order (Ord_aux (Ord_dec, _)), _);
                                          A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode ->
-       parens (separate space ([string (maybe_zencode "bitsFromInterpValue"); fromValueNexp len_nexp; string arg_name]))
+       parens (separate space ([string (maybe_zencode "bitsFromInterpValue"); string arg_name]))
     | Typ_app (typ_id, typ_args) ->
        assert (typ_args <> []);
-       parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name]))
+       if string_of_id typ_id = "bits" then
+         parens (separate space ([string "bitsFromInterpValue"] @ [string arg_name]))
+       else
+         parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name]))
     | Typ_var kid -> parens (separate space [fromValueKid kid; string arg_name])
     | Typ_fn _ -> parens (string "failwith \"fromValueTyp: Typ_fn arm unimplemented\"")
-    | _ -> parens (string "failwith \"fromValueTyp: type arm unimplemented\"")
+    | Typ_bidir _ -> parens (string "failwith \"fromValueTyp: Typ_bidir arm unimplemented\"")
+    | Typ_exist (kids, _, t) -> parens (fromValueTyp (rewriteExistential kids t) arg_name)
+    | Typ_tup typs -> parens (string ("match " ^ arg_name ^ " with V_tuple ") ^^
+                                brackets (separate (string ";" ^^ space)
+                                          (List.mapi (fun i _ -> string (arg_name ^ "_tup" ^ string_of_int i)) typs)) ^^
+                                  (string " -> ") ^^
+                                    parens (separate comma_sp (List.mapi (fun i t -> fromValueTyp t (arg_name ^ "_tup" ^ string_of_int i)) typs)))
+    | Typ_internal_unknown -> failwith "escaped Typ_internal_unknown"
   in 
   let fromValueVals ((Typ_aux (typ_aux, l)) as typ) = match typ_aux with
     | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i typ -> fromValueTyp typ ("v" ^ (string_of_int i))) typs))
@@ -147,13 +176,14 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
      end
   | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty
   | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty
+  | TD_abbrev (Id_aux (Id "bits", _), _, _) when !lem_mode -> empty
   | TD_abbrev (id, typq, typ_arg) ->
      begin
        let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
        (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *)
        let fromInterpValspec =
          (* HACK because of lem renaming *)
-         if string_of_id id = "opcode" then empty else
+         if string_of_id id = "opcode" || string_of_id id = "integer" then empty else
          match typ_arg with
          | A_aux (A_typ _, _) -> begin match typq with
                                  | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string "value"; arrow; string (maybe_zencode (string_of_id id))]
@@ -222,19 +252,30 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
     | A_typ typ -> toValueTyp typ ""
     | A_nexp nexp -> toValueNexp nexp
     | A_order order -> string ("Order_" ^ (string_of_order order))
-    | _ -> string "TYP_ARG" 
+    | A_bool _ -> parens (string "boolToInterpValue") 
   and toValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with
     | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"; space; string arg_name])
     (* special case bit vectors for lem *)
     | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _);
                                          A_aux (A_order (Ord_aux (Ord_dec, _)), _);
                                          A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode ->
-       parens (separate space ([string (maybe_zencode "bitsToInterpValue"); toValueNexp len_nexp; string arg_name]))
+       parens (separate space ([string (maybe_zencode "bitsToInterpValue"); string arg_name]))
     | Typ_app (typ_id, typ_args) ->
        assert (typ_args <> []);
-       parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name]))
+       if string_of_id typ_id = "bits" then
+         parens (separate space ([string "bitsToInterpValue"] @ [string arg_name]))
+       else
+         parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name]))
     | Typ_var kid -> parens (separate space [toValueKid kid; string arg_name])
-    | _ -> parens (string "failwith \"toValueTyp: type arm unimplemented\"")
+    | Typ_fn _ -> parens (string "failwith \"toValueTyp: Typ_fn arm unimplemented\"")
+    | Typ_bidir _ -> parens (string "failwith \"toValueTyp: Typ_bidir arm unimplemented\"")
+    | Typ_exist (kids, _, t) -> parens (toValueTyp (rewriteExistential kids t) arg_name)
+    | Typ_tup typs -> parens (string ("match " ^ arg_name ^ " with ") ^^
+                                parens (separate comma_sp (List.mapi (fun i _ -> string (arg_name ^ "_tup" ^ string_of_int i)) typs)) ^^
+                                  (string " -> V_tuple ") ^^
+                                    brackets (separate (string ";" ^^ space)
+                                          (List.mapi (fun i t -> toValueTyp t (arg_name ^ "_tup" ^ string_of_int i)) typs)))
+    | Typ_internal_unknown -> failwith "escaped Typ_internal_unknown"
   in
   let toValueVals ((Typ_aux (typ_aux, _)) as typ) = match typ_aux with
     | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i typ -> toValueTyp typ ("v" ^ (string_of_int i))) typs))])
@@ -284,13 +325,14 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
      end
   | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty
   | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty
+  | TD_abbrev (Id_aux (Id "bits", _), _, _) when !lem_mode -> empty
   | TD_abbrev (id, typq, typ_arg) ->
      begin
        let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
        (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *) 
        let toInterpValspec =
          (* HACK because of lem renaming *)
-         if string_of_id id = "opcode" then empty else
+         if string_of_id id = "opcode" || string_of_id id = "integer" then empty else
          match typ_arg with
          | A_aux (A_typ _, _) -> begin match typq with
                                  | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string (maybe_zencode (string_of_id id)); arrow; string "value"]
@@ -343,12 +385,13 @@ let tofrominterp_def def = match def with
 let tofrominterp_defs name (Defs defs) =
   (string "open Sail_lib;;" ^^ hardline)
   ^^ (string "open Value;;" ^^ hardline)
-  ^^ (string "open ToFromInterp_lib;;" ^^ hardline)
   ^^ (if !lem_mode then (string "open Sail2_instr_kinds;;" ^^ hardline) else empty)
   ^^ (string ("open " ^ String.capitalize_ascii name ^ ";;") ^^ hardline)
   ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_types;;") ^^ hardline) else empty)
   ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_extras;;") ^^ hardline) else empty)
   ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end)
+  ^^ (if !mword_mode then (string "include ToFromInterp_lib_mword" ^^ hardline) else empty)
+  ^^ (if not !mword_mode then (string "include ToFromInterp_lib_bitlist.Make(struct type t = Sail2_values.bitU0 let b0 = Sail2_values.B00 let b1 = Sail2_values.B10 end)" ^^ hardline) else empty)
   ^^ concat (List.map tofrominterp_def defs)
 
 let tofrominterp_pp_defs name f defs =
diff --git a/src/toFromInterp_lib_bitlist.ml b/src/toFromInterp_lib_bitlist.ml
new file mode 100644
index 00000000..d47beca3
--- /dev/null
+++ b/src/toFromInterp_lib_bitlist.ml
@@ -0,0 +1,142 @@
+(************************************************************)
+(* Support for toFromInterp                                 *)
+(************************************************************)
+
+open Sail_lib;;
+open Value;;
+
+module Make(BitT : BitType) = struct
+
+type vector_order =
+ | Order_inc
+ | Order_dec
+
+(* zencoded variants are for the OCaml backend, non-zencoded are for the Lem backend compiled to OCaml.
+   Sometimes they're just aliased. *)
+
+let zunitFromInterpValue v = match v with
+  | V_unit -> ()
+  | _ -> failwith "invalid interpreter value for unit"
+
+let zunitToInterpValue () = V_unit
+
+let unitFromInterpValue = zunitFromInterpValue
+let unitToInterpValue = zunitToInterpValue
+
+let zatomFromInterpValue typq_'n v = match v with
+  | V_int i when typq_'n = i -> i
+  | _ -> failwith "invalid interpreter value for atom"
+
+let zatomToInterpValue typq_'n v =
+  assert (typq_'n = v);
+  V_int v
+
+let atomFromInterpValue = zatomFromInterpValue
+let atomToInterpValue = zatomToInterpValue 
+
+let zintFromInterpValue v = match v with
+  | V_int i -> i
+  | _ -> failwith "invalid interpreter value for int"
+
+let zintToInterpValue v = V_int v
+
+let intFromInterpValue = zintFromInterpValue
+let intToInterpValue = zintToInterpValue 
+
+let znatFromInterpValue v = match v with
+  | V_int i when i >= Big_int.zero -> i
+  | _ -> failwith "invalid interpreter value for nat"
+
+let znatToInterpValue v =
+  assert (v >= Big_int.zero);
+  V_int v
+
+let natFromInterpValue = znatFromInterpValue
+let natToInterpValue = znatToInterpValue 
+
+let zrangeFromInterpValue low high v = match v with
+  | V_int i when i >= low && i <= high -> i
+  | _ -> failwith (Printf.sprintf "invalid interpreter value for range(%s, %s)" (Big_int.to_string low) (Big_int.to_string high))
+
+let zrangeToInterpValue low high v =
+  assert (v >= low && v <= high);
+  V_int v
+
+let rangeFromInterpValue = zrangeFromInterpValue
+let rangeToInterpValue = zrangeToInterpValue
+
+
+let zboolFromInterpValue v = match v with
+  | V_bool b -> b
+  | _ -> failwith "invalid interpreter value for bool"
+
+let zboolToInterpValue v = V_bool v
+
+let boolFromInterpValue = zboolFromInterpValue
+let boolToInterpValue = zboolToInterpValue 
+
+let zstringFromInterpValue v = match v with
+  | V_string s -> s
+  | _ -> failwith "invalid interpreter value for string"
+
+let zstringToInterpValue v = V_string v
+
+let stringFromInterpValue = zstringFromInterpValue
+let stringToInterpValue = zstringToInterpValue 
+
+let zlistFromInterpValue typq_'a v = match v with
+  | V_list vs -> List.map typq_'a vs
+  | _ -> failwith "invalid interpreter value for list"
+
+let zlistToInterpValue typq_'a v = V_list (List.map typq_'a v)
+
+let listFromInterpValue = zlistFromInterpValue
+let listToInterpValue = zlistToInterpValue 
+
+let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with
+  | V_vector vs ->
+     assert (Big_int.of_int (List.length vs) = typq_'n);
+     List.map typq_'a vs
+  | _ -> failwith "invalid interpreter value for vector"
+
+let zvectorToInterpValue typq_'n typq_'ord typq_'a v =
+  assert (Big_int.of_int (List.length v) = typq_'n);
+  V_vector (List.map typq_'a v)
+
+let vectorFromInterpValue = zvectorFromInterpValue
+let vectorToInterpValue = zvectorToInterpValue 
+
+let zbitFromInterpValue v = match v with
+  | V_bit b -> (match b with
+                | Sail_lib.B0 -> BitT.b0
+                | Sail_lib.B1 -> BitT.b1)
+  | _ -> failwith "invalid interpreter value for bit"
+
+let zbitToInterpValue v = V_bit (match v with
+                                 | b when b = BitT.b0 -> Sail_lib.B0
+                                 | b when b = BitT.b1 -> Sail_lib.B1
+                                 | _ -> failwith "invalid BitT (usually bitU) value for bit")
+
+let bitFromInterpValue = zbitFromInterpValue
+let bitToInterpValue = zbitToInterpValue
+
+let optionFromInterpValue typq_'a v = match v with
+  | V_ctor ("None", [v0]) -> None
+  | V_ctor ("Some", [v0]) -> Some (typq_'a v0)
+  | _ -> failwith "invalid interpreter value for option"
+
+let optionToInterpValue typq_'a v = match v with
+  | None -> V_ctor ("None", [(unitToInterpValue ())])
+  | Some (v0) -> V_ctor ("Some", [(typq_'a v0)])
+
+
+let bitsFromInterpValue v = match v with
+  | V_vector vs ->
+     List.map bitFromInterpValue vs
+  | _ -> failwith "invalid interpreter value for bits"
+
+let bitsToInterpValue v =
+  V_vector (List.map bitToInterpValue v)
+
+
+end
diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib_mword.ml
index c29fcd84..fb937f11 100644
--- a/src/toFromInterp_lib.ml
+++ b/src/toFromInterp_lib_mword.ml
@@ -52,6 +52,17 @@ let znatToInterpValue v =
 let natFromInterpValue = znatFromInterpValue
 let natToInterpValue = znatToInterpValue 
 
+let zrangeFromInterpValue low high v = match v with
+  | V_int i when i >= low && i <= high -> i
+  | _ -> failwith (Printf.sprintf "invalid interpreter value for range(%s, %s)" (Big_int.to_string low) (Big_int.to_string high))
+
+let zrangeToInterpValue low high v =
+  assert (v >= low && v <= high);
+  V_int v
+
+let rangeFromInterpValue = zrangeFromInterpValue
+let rangeToInterpValue = zrangeToInterpValue
+
 
 let zboolFromInterpValue v = match v with
   | V_bool b -> b
@@ -112,15 +123,13 @@ let optionToInterpValue typq_'a v = match v with
   | Some (v0) -> V_ctor ("Some", [(typq_'a v0)])
 
 
-let bitsFromInterpValue typq_'n v = match v with
+let bitsFromInterpValue v = match v with
   | V_vector vs ->
-     assert (Big_int.of_int (List.length vs) = typq_'n);
      Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs)
   | _ -> failwith "invalid interpreter value for bits"
 
-let bitsToInterpValue typq_'n v =
+let bitsToInterpValue v =
   let bs = Lem.bitlistFromWord v in
-  assert (Big_int.of_int (List.length bs) = typq_'n);
   V_vector (List.map (fun b -> Sail_lib.bit_of_bool b |> bitToInterpValue) bs)
 
 
diff --git a/src/value.ml b/src/value.ml
index 6ccecac0..6c2e0839 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -170,6 +170,10 @@ let coerce_tuple = function
   | V_tuple vs -> vs
   | _ -> assert false
 
+let coerce_list = function
+  | V_list vs -> vs
+  | _ -> assert false
+
 let coerce_listlike = function
   | V_tuple vs -> vs
   | V_list vs -> vs
@@ -282,6 +286,10 @@ let value_append = function
   | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2)
   | _ -> failwith "value append"
 
+let value_append_list = function
+  | [v1; v2] -> V_list (coerce_list v1 @ coerce_list v2)
+  | _ -> failwith "value_append_list"
+
 let value_slice = function
   | [v1; v2; v3] -> V_vector (Sail_lib.slice (coerce_gv v1, coerce_int v2, coerce_int v3))
   | _ -> failwith "value slice"
@@ -647,6 +655,7 @@ let primops =
       ("update_subrange", value_update_subrange);
       ("slice", value_slice);
       ("append", value_append);
+      ("append_list", value_append_list);
       ("not", value_not);
       ("not_vec", value_not_vec);
       ("and_vec", value_and_vec);