move type definitions that both interpreter and shallow embedding use to sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome

17 files changed, 1710 insertions, 1656 deletions

diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
index fd0fc17b..abab2163 100644
--- a/src/gen_lib/armv8_extras.lem
+++ b/src/gen_lib/armv8_extras.lem
@@ -1,31 +1,53 @@
 open import Pervasives
-open import State
+open import Sail_impl_base
+open import Vector
 open import Sail_values
+open import Prompt
 
-let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
-let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
-let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
-let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
-let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
-
-let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
-
-let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
-
-let wMem_Val_NORMAL (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return ()
-let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O
-
-let DataMemoryBarrier_Reads () = return ()
-let DataMemoryBarrier_Writes () = return ()
-let DataMemoryBarrier_All () = return ()
-let DataSynchronizationBarrier_Reads () = return ()
-let DataSynchronizationBarrier_Writes () = return ()
-let DataSynchronizationBarrier_All () = return ()
-let InstructionSynchronizationBarrier () = return ()
+val rMem_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_STREAM         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ATOMICL        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+
+let rMem_NORMAL (addr,size)         = read_memory Read_plain addr size
+let rMem_STREAM (addr,size)         = read_memory Read_stream addr size
+let rMem_ORDERED (addr,size)        = read_memory Read_acquire addr size
+let rMem_ATOMIC (addr,size)         = read_memory Read_exclusive addr size
+let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size
+
+val wMem_Addr_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ATOMIC         : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit
+
+let wMem_Addr_NORMAL (addr,size)         = write_memory_ea Write_plain addr size
+let wMem_Addr_ORDERED (addr,size)        = write_memory_ea Write_release addr size
+let wMem_Addr_ATOMIC (addr,size)         = write_memory_ea Write_exclusive addr size
+let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size
+
+
+val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit
+val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU
+
+let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return ()
+(* in ARM the status returned is inversed *)
+let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I)
+
+
+val DataMemoryBarrier_Reads            : forall 'e. unit -> M 'e unit
+val DataMemoryBarrier_Writes           : forall 'e. unit -> M 'e unit
+val DataMemoryBarrier_All              : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_Reads   : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_Writes  : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_All     : forall 'e. unit -> M 'e unit
+val InstructionSynchronizationBarrier  : forall 'e. unit -> M 'e unit
+
+let DataMemoryBarrier_Reads ()           = barrier DMB_LD
+let DataMemoryBarrier_Writes ()          = barrier DMB_ST
+let DataMemoryBarrier_All ()             = barrier DMB
+let DataSynchronizationBarrier_Reads ()  = barrier DSB_LD
+let DataSynchronizationBarrier_Writes () = barrier DSB_ST
+let DataSynchronizationBarrier_All ()    = barrier DSB
+let InstructionSynchronizationBarrier () = barrier Isync
 
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index e08da230..2e255db7 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -1,49 +1,47 @@
 open import Pervasives
+open import Sail_impl_base
 open import Vector
-open import State
 open import Sail_values
+open import Prompt
 
-(*
-let rec countLeadingZeros_helper bits =  
-((match bits with
-    | (Interp.V_lit (L_aux( L_zero, _)))::bits -> 
-      let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
-      Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
-    | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
-))
-let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
-  | [Interp.V_track( v, r);Interp.V_track( v2, r2)] -> 
-    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
-  | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
-  | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
-  | [Interp.V_unknown;_] -> Interp.V_unknown
-  | [_;Interp.V_unknown] -> Interp.V_unknown
-  | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] -> 
-    countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
-))
- *)
-
-let MEMr (addr,l) = read_memory (unsigned addr) l
-let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
-
-let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
-let MEMw_EA_cond (addr,l) = write_writeEA (unsigned addr) l
-                                        
-let MEMw (addr,l,value) = write_memory (unsigned addr) l value
-let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return I
-
-let I_Sync () = return ()
-let H_Sync () = return ()
-let LW_Sync () = return ()
-let EIEIO_Sync () = return ()
-
-let recalculate_dependency () = return ()
+val MEMr         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+
+let MEMr (addr,size) = read_memory Read_plain addr size
+let MEMr_reserve (addr,size) = read_memory Read_reserve addr size
+
+
+val MEMw_EA      : forall 'e. (vector bitU * integer) -> M 'e unit
+val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit
+                                                           
+let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size
+let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size
+
+
+val MEMw             : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit
+val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU
+
+let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return ()
+let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b)
+
+
+val I_Sync     : forall 'e unit -> M 'e unit
+val H_Sync     : forall 'e unit -> M 'e unit
+val LW_Sync    : forall 'e unit -> M 'e unit
+val EIEIO_Sync : forall 'e unit -> M 'e unit
+
+let I_Sync ()     = barrier Isync
+let H_Sync ()     = barrier Sync
+let LW_Sync ()    = barrier LwSync
+let EIEIO_Sync () = barrier Eieio
+
+let recalculate_dependency () = footprint
 
 let trap () = exit "error"
 (* this needs to change, but for that we'd have to make the type checker know about trap 
  * as an effect *)
 
-val countLeadingZeroes : vector bit * integer -> integer
+val countLeadingZeroes : vector bitU * integer -> integer
 let countLeadingZeroes (Vector bits _ _ ,n)  = 
   let (_,bits) = List.splitAt (natFromInteger n) bits in
   integerFromNat (List.length (takeWhile ((=) O) bits))
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index e1e8658e..02a83d8a 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,251 +1,134 @@
 open import Pervasives_extra
+open import Sail_impl_base
 open import Vector
+open import Sail_values
 open import Arch
 
-let compose f g x = f (g x)
-
-type end_flag =
-  | E_big_endian
-  | E_little_endian
-
-type direction = 
-  | D_increasing
-  | D_decreasing
-
-type register_value = <| 
-    rv_bits: list bit (* MSB first, smallest index number *); 
-    rv_dir: direction; 
-    rv_start: nat ;
-    rv_start_internal: nat; 
-    (*when dir is increasing, rv_start = rv_start_internal. 
-      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
-    |>
-
-type byte = list bit (* of length 8 *)  (*MSB first everywhere*)
-
-type address = integer
-type address_lifted = address
-
-type memory_value = list byte
-(* the list is of length >=1 *)
-(* for both big-endian (Power) and little-endian (ARM), the head of the
-     list is the byte stored at the lowest address *)
-(* for big-endian Power the head of the list is the most-significant
-   byte, in both the interpreter and machineDef* code. *)
-(* For little-endian ARM, the head of the list is the
-   least-significant byte in machineDef* code and the
-   most-significant byte in interpreter code, with the switch over
-   (a list-reverse) being done just inside the interpreter interface*)
-(* In other words, in the machineDef* code the lowest-address byte is first,
-   and in the interpreter code the most-significant byte is first *)
-
-type opcode = Opcode of list byte (* of length 4 *)
-
-type read_kind =
-  (* common reads *)
-  | Read_plain
-  (* Power reads *)
-  | Read_reserve
-  (* AArch64 reads *)
-  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
-
-type write_kind =
-  (* common writes *)
-  | Write_plain
-  (* Power writes *)
-  | Write_conditional
-  (* AArch64 writes *)
-  | Write_release | Write_exclusive | Write_exclusive_release
-
-type barrier_kind =
-  (* Power barriers *)
-  | Sync | LwSync | Eieio | Isync
-  (* AArch64 barriers *)
-  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
-
-type slice = (nat * nat)
-
-type reg_name = 
-  (* Name of the register, accessing the entire register, the start and size of this register, 
-   * and its direction *)
-  | Reg of string * nat * nat * direction
-                                  
-  (* Name of the register, accessing from the bit indexed by the first
-   * to the bit indexed by the second integer of the slice, inclusive. For
-   * machineDef* the first is a smaller number or equal to the second.  *)
-  | Reg_slice of string * nat * direction * slice 
-                                              
-  (* Name of the register, start and direction, and name of the field of the register
-   * accessed. The slice specifies where this field is in the register*)
-  | Reg_field of string * nat * direction * string * slice 
-
-  (* The first four components are as in Reg_field; the final slice
-   * specifies a part of the field, indexed w.r.t. the register as a whole *)
-  | Reg_f_slice of string * nat * direction * string * slice * slice 
-
-type outcome 'e 'a =
-  (* Request to read memory, value is location to read followed by registers that location depended 
-   * on when mode.track_values, integer is size to read, followed by registers that were used in 
-   * computing that size *)
-  (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
-  | Read_mem of read_kind * address_lifted * nat * (memory_value -> outcome 'e 'a)
-                    
-  (* Request to write memory, first value and dependent registers is location, second is the value 
-   * to write *)
-  | Write_mem of write_kind * address_lifted * nat * memory_value * (bool -> outcome 'e 'a)
-                                             
-  (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
-  | Write_ea of write_kind * address_lifted * nat * outcome 'e 'a
-                                                                              
-  (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
-   * ea signal *)
-  | Write_memv of memory_value * (bool -> outcome 'e 'a)
-                                                           
-  (* Request a memory barrier *)
-  (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
-   * need that *)
-  | Barrier of barrier_kind * outcome 'e 'a
-                                
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome 'e 'a
-                   
-  (* Request to read register *)
-  | Read_reg of reg_name * (register_value -> outcome 'e 'a)
-                             
-  (* Request to write register *)
-  | Write_reg of reg_name * register_value * outcome 'e 'a
-                                               
-  (* List of instruction states to be run in parrallel, any order permitted.
-     Expects concurrency model to choose an order: a permutation of the original list *)
-  | Nondet_choice of unit
-                                                
-  (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
-   * provide a handler. *)
-  | Escape of 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
-
-  (* Stop for incremental stepping, function can be used to display function call data *)
-  | Done of 'a
-
-type M 'e 'a = outcome 'e 'a
-
-val return : forall 'e 'a. 'a -> M 'e 'a
+val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a
 let return a = Done a
 
-val (>>=) : forall 'e 'a 'b. M 'e 'a -> ('a -> M 'e 'b) -> M 'e 'b
-let rec (>>=) m f = match m with
-  | Done a -> f a
-  | Read_mem rk addr sz k ->    Read_mem rk addr sz    (fun v -> (k v) >>= f)
-  | Write_mem wk addr sz v k -> Write_mem wk addr sz v (fun b -> (k b) >>= f)
-  | Write_ea wk addr sz k ->    Write_ea wk addr sz    (k >>= f)
-  | Write_memv v k ->           Write_memv v           (fun b -> (k b) >>= f)
-  | Barrier bk k ->             Barrier bk             (k >>= f)
-  | Footprint k ->              Footprint              (k >>= f)
-  | Read_reg reg k ->           Read_reg reg           (fun v -> (k v) >>= f)
-  | Write_reg reg v k ->        Write_reg reg v        (k >>= f)
-  | Nondet_choice () ->         Nondet_choice ()
-  | Escape e ->                 Escape e
-  end
-
-val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
-let (>>) m n = m >>= fun _ -> n
-
-val exit : forall 'a 'e. 'e -> M 'e 'a
-let exit = Escape
-
-val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
-let rec byte_chunks n list = match (n,list) with
-  | (0,_) -> []
-  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
-  | _ -> failwith "byte_chunks not given enough bits"
+val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b
+let rec bind m f = match m with
+  | Done a ->              f a 
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s  in (bind o f,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s  in (bind o f,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s  in (bind o f,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s  in (bind o f,opt))
+  | Escape o_s  ->         Escape o_s
 end
 
-val bitvFromBytes : list byte -> vector bit
-let bitvFromBytes v = Vector (foldl (++) [] v) 0 defaultDir
 
-let dir is_inc = if is_inc then D_increasing else D_decreasing
+type M 'e 'a = Sail_impl_base.outcome unit 'e 'a
 
-val bitvFromRegisterValue : register_value -> vector bit
-let bitvFromRegisterValue v =
-  Vector (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+let (>>=) = bind
+val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
+let (>>) m n = m >>= fun _ -> n
 
-val registerValueFromBitv : vector bit -> register -> register_value
-let registerValueFromBitv (Vector bits start is_inc) reg = 
-  let start = natFromInteger start in
-  <| rv_bits = bits;
-     rv_dir = dir is_inc;
-     rv_start_internal = start;
-     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+val exit : forall 'a 'e. 'e -> M 'e 'a
+let exit e = Escape (Just (return e,Nothing))
 
-val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (vector bit)
+val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU)
 let read_memory rk addr sz =
+  let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
-  Read_mem rk addr sz (compose Done bitvFromBytes)
-
-val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool
-let write_memory wk addr sz (Vector v _ _) =
+  let k memory_value =
+    let bitv = bitv_of_byte_lifteds memory_value in
+    (Done bitv,Nothing) in
+  Read_mem (rk,addr,sz) k
+
+val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer  -> M 'e unit
+let write_memory_ea wk addr sz =
+  let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
-  Write_mem wk addr sz (byte_chunks sz v) Done
+  Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val read_reg_range : forall 'e. register -> (integer * integer) -> M 'e (vector bit)
-let read_reg_range reg (i,j) =
-  let (i,j) = (natFromInteger i,natFromInteger j) in
-  let start = natFromInteger (start_index_reg reg) in
-  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
+val write_memory_val : forall 'e. vector bitU -> M 'e bool
+let write_memory_val v =
+  let v = byte_lifteds_of_bitv v in
+  let k successful = (return successful,Nothing) in
+  Write_memv v k
 
-val write_reg_range : forall 'e. register -> (integer * integer) -> vector bit -> M 'e unit
-let write_reg_range reg (i,j) v =
-  let rv = registerValueFromBitv v reg in
-  let start = natFromInteger (start_index_reg reg) in
+
+val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU)
+let read_reg_range reg i j =
   let (i,j) = (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Write_reg reg rv (Done ())
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_bit : forall 'e. register -> integer -> M 'e bit
+val read_reg_bit : forall 'e. register -> integer -> M 'e bitU
 let read_reg_bit reg i = 
-  let i = natFromInteger i in
-  let start = natFromInteger (start_index_reg reg) in
-  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
-  Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
+  read_reg_range reg i i >>= fun v -> return (access v i)
 
-val write_reg_bit : forall 'e. register -> integer -> bit -> M 'e unit
-let write_reg_bit reg i bit = write_reg_range reg (i,i) (Vector [bit] 0 true)
-
-val read_reg : forall 'e. register -> M 'e (vector bit)
+val read_reg : forall 'e. register -> M 'e (vector bitU)
 let read_reg reg =
   let start = natFromInteger (start_index_reg reg) in
   let sz = natFromInteger (length_reg reg) in
   let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
-
-val write_reg : forall 'e. register -> vector bit -> M 'e unit
-let write_reg reg v =
-  let rv = registerValueFromBitv v reg in
-  let start = natFromInteger (start_index_reg reg) in
-  let sz = natFromInteger (length_reg reg) in
-  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
-  Write_reg reg rv (Done ())
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU)
 let read_reg_field reg rfield = 
   let (i,j) =
     let (i,j) = field_indices rfield in
     (natFromInteger i,natFromInteger j) in
   let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
-
-val write_reg_field : forall 'e. register -> register_field -> vector bit -> M 'e unit
-let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bitU
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e unit
+
+
+val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit
+let write_reg_range reg i j v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Write_reg (reg,rv) (Done (),Nothing)
+
+val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit
+let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)
+
+val write_reg : forall 'e. register -> vector bitU -> M 'e unit
+let write_reg reg v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Write_reg (reg,rv) (Done (),Nothing)
+
+val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit
+let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
+
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> M 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
-val foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
+
+val barrier : forall 'e. barrier_kind -> M 'e unit
+let barrier bk = Barrier bk (Done (), Nothing)
+
+
+val footprint : forall 'e. M 'e unit
+let footprint = Footprint (Done (),Nothing)
+
+
+val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
@@ -254,8 +137,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
+val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 46c3a10c..98b68e1b 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,10 +1,36 @@
 open import Pervasives_extra
+open import Sail_impl_base
 open import Vector
 open import Arch
 
 type i = integer
 type n = natural
 
+let to_bool = function
+  | O -> false
+  | I  -> true
+  | Undef -> failwith "to_bool applied to Undef"
+  end
+
+
+let bit_lifted_of_bitU = function
+  | O -> Bitl_zero
+  | I -> Bitl_one
+  | Undef -> Bitl_undef
+  end
+
+let bitU_of_bit = function
+  | Bitc_zero -> O
+  | Bitc_one  -> I
+  end
+
+let bitU_of_bit_lifted = function
+  | Bitl_zero -> O
+  | Bitl_one  -> I
+  | Bitl_undef -> Undef
+  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
+  end
+
 let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
 let most_significant = function
@@ -27,7 +53,7 @@ let pow m n = m ** (natFromInteger n)
 let bitwise_not (Vector bs start is_inc) =
   Vector (List.map bitwise_not_bit bs) start is_inc
 
-val is_one : integer -> bit
+val is_one : integer -> bitU
 let is_one i =
   if i = 1 then I else O
 
@@ -39,22 +65,22 @@ let bitwise_binop_bit op = function
   | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
   end
 
-val bitwise_and_bit : bit * bit -> bit
+val bitwise_and_bit : bitU * bitU -> bitU
 let bitwise_and_bit = bitwise_binop_bit (&&)
 
-val bitwise_or_bit : bit * bit -> bit
+val bitwise_or_bit : bitU * bitU -> bitU
 let bitwise_or_bit = bitwise_binop_bit (||)
 
-val bitwise_xor_bit : bit * bit -> bit
+val bitwise_xor_bit : bitU * bitU -> bitU
 let bitwise_xor_bit = bitwise_binop_bit xor
 
-val (&.) : bit -> bit -> bit
+val (&.) : bitU -> bitU -> bitU
 let (&.) x y = bitwise_and_bit (x,y)
 
-val (|.) : bit -> bit -> bit
+val (|.) : bitU -> bitU -> bitU
 let (|.) x y = bitwise_or_bit (x,y)
 
-val (+.) : bit -> bit -> bit
+val (+.) : bitU -> bitU -> bitU
 let (+.) x y = bitwise_xor_bit (x,y)
 
 let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
@@ -474,7 +500,7 @@ let make_indexed_vector entries default start length =
   let length = natFromInteger length in
   Vector (List.foldl replace (replicate length default) entries) start defaultDir
 
-val make_bit_vector_undef : integer -> vector bit
+val make_bit_vector_undef : integer -> vector bitU
 let make_bitvector_undef length =
   Vector (replicate (natFromInteger length) Undef) 0 true
 
@@ -485,6 +511,55 @@ let mask (n,Vector bits start dir) =
   Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
 
 
+let bit_of_bit_lifted = function
+  | Bitl_zero -> O
+  | Bitl_one  -> I
+  | Bitl_undef -> Undef
+  | _ -> failwith "bit_of_bit_lifted: unexpected Bitl_unknown"
+end
+
+val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
+let rec byte_chunks n list = match (n,list) with
+  | (0,_) -> []
+  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
+  | _ -> failwith "byte_chunks not given enough bits"
+end
+
+
+val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> vector bitU
+let bitv_of_byte_lifteds v =
+  Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 defaultDir
+
+val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
+let byte_lifteds_of_bitv (Vector bits length is_inc) = 
+  let bits = List.map bit_lifted_of_bitU bits in
+  byte_lifteds_of_bit_lifteds bits
+
+val address_lifted_of_bitv : vector bitU -> address_lifted
+let address_lifted_of_bitv v =
+  Address_lifted (byte_lifteds_of_bitv v) Nothing
+
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+
+val bitvFromRegisterValue : register_value -> vector bitU
+let bitvFromRegisterValue v =
+  Vector (List.map bitU_of_bit_lifted v.rv_bits)
+         (integerFromNat (v.rv_start))
+         (v.rv_dir = D_increasing)
+
+
+val registerValueFromBitv : vector bitU -> register -> register_value
+let registerValueFromBitv (Vector bits start is_inc) reg = 
+  let start = natFromInteger start in
+  <| rv_bits = List.map bit_lifted_of_bitU bits;
+     rv_dir = dir is_inc;
+     rv_start_internal = start;
+     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+
+
+
 
 
 class (ToNatural 'a)
@@ -533,4 +608,9 @@ let rec foreach_dec (i,stop,by) vars body =
        foreach_dec (i - by,stop,by) vars body
   else vars
 
-
+let assert' b msg_opt =
+  let msg = match msg_opt with
+  | Just msg -> msg
+  | Nothing  -> "unspecified error"
+  end in
+  if to_bool b then failwith msg else ()
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 5fc59207..1e7b9db4 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -6,7 +6,7 @@ open import Sail_values
 (* 'a is result type, 'e is error type *)
 type State 's 'e 'a = 's -> (either 'a 'e * 's)
 
-type memstate = map integer (list bit)
+type memstate = map integer (list bitU)
 
 type state =
   <| regstate : regstate;
@@ -39,13 +39,6 @@ let (>>) m n = m >>= fun _ -> n
 val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
 let exit e s = (Right e,s)
 
-let assert' b msg_opt =
-  let msg = match msg_opt with
-  | Just msg -> msg
-  | Nothing  -> "unspecified error"
-  end in
-  if to_bool b then failwith msg else ()
-
 val read_writeEA : forall 'e. unit -> State state 'e (integer * integer)
 let read_writeEA () s = (Left s.writeEA,s)
 
@@ -61,82 +54,82 @@ let rec byte_chunks n l =
     | _ -> failwith "byte_chunks not given enough bits"
     end
 
-val read_regstate : state -> register -> vector bit
+val read_regstate : state -> register -> vector bitU
 let read_regstate s = read_regstate_aux s.regstate
 
-val write_regstate : state -> register -> vector bit -> state
+val write_regstate : state -> register -> vector bitU -> state
 let write_regstate s reg v = <| s with regstate = (write_regstate_aux s.regstate reg v) |>
 
-val read_memstate : memstate -> integer -> list bit
+val read_memstate : memstate -> integer -> list bitU
 let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s
 
-val write_memstate : memstate -> (integer * list bit) -> memstate
+val write_memstate : memstate -> (integer * list bitU) -> memstate
 let write_memstate s (addr,bits) = Map.insert addr bits s
 
-val read_memory : forall 'e. integer -> integer -> State state 'e (vector bit)
+val read_memory : forall 'e. integer -> integer -> State state 'e (vector bitU)
 let read_memory addr l s =
   let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in
   (Left (Vector (foldl (++) [] bytes) 0 defaultDir),s)
 
-val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit
+val write_memory : forall 'e. integer -> integer -> vector bitU -> State state 'e unit
 let write_memory addr l (Vector bits _ _) s =
   let addrs = List.map ((+) addr) (ints l) in
   let bytes = byte_chunks l bits in
   (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>)
 
-val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bit)
+val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bitU)
 let read_reg_range reg i j s =
   let v = slice (read_regstate s reg) i j in
   (Left v,s)
 
-val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bit
+val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bitU
 let read_reg_bit reg i s =
   let v = access (read_regstate s reg) i in
   (Left v,s)
 
-val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> State state 'e unit
+val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bitU -> State state 'e unit
 let write_reg_range reg i j v s =
   let v' = update (read_regstate s reg) i j v in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> State state 'e unit
+val write_reg_bit : forall 'e. register -> integer (*nat*) -> bitU -> State state 'e unit
 let write_reg_bit reg i bit s =
   let v = read_regstate s reg in
   let v' = update_pos v i bit in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val read_reg : forall 'e. register -> State state 'e (vector bit)
+val read_reg : forall 'e. register -> State state 'e (vector bitU)
 let read_reg reg s =
   let v = read_regstate s reg in
   (Left v,s)
 
-val write_reg : forall 'e. register -> vector bit -> State state 'e unit
+val write_reg : forall 'e. register -> vector bitU -> State state 'e unit
 let write_reg reg v s =
   let s' = write_regstate s reg v in
   (Left (),s')
 
-val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bitU)
 let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
 
-val write_reg_field : forall 'e. register -> register_field -> vector bit -> State state 'e unit
+val write_reg_field : forall 'e. register -> register_field -> vector bitU -> State state 'e unit
 let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
 
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bitU
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> State state 'e unit
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> State state 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
 val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer ->
-                            vector bit -> State state 'e unit
+                            vector bitU -> State state 'e unit
 let write_reg_field_range reg rfield i j v =
   let (i',j') = field_indices rfield in
   write_reg_range reg i' j' v
 
 val write_reg_field_bit : forall 'e. register -> register_field -> integer ->
-                            bit -> State state 'e unit
+                            bitU -> State state 'e unit
 let write_reg_field_bit reg rfield i v =
   let (i',_) = field_indices rfield in
   write_reg_bit reg (i + i') v
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index b2d68132..6acb4aa0 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,7 @@
 open import Pervasives_extra
 
-type bit = O | I | Undef
+(* this is here to avoid circular dependencies when Sail_values imports Arch.lem *)
+type bitU = O | I | Undef
 
 (* element list * start * has increasing direction *)
 type vector 'a = Vector of list 'a * integer * bool
@@ -11,11 +12,6 @@ let rec nth xs (n : integer) =
   | _ -> failwith "nth applied to empty list"
   end
 
-let to_bool = function
-  | O -> false
-  | I  -> true
-  | Undef -> failwith "to_bool applied to Undef"
-  end
 
 let get_start (Vector _ s _) = s
 let length (Vector bs _ _) = integerFromNat (length bs)
diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index 9aa5f97e..467a15ea 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -1,3 +1,4 @@
+Sail_impl_base
 Interp_ast
 Interp_utilities
 Instruction_extractor
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 73845fee..074f3bc4 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -2,7 +2,7 @@ open import Interp_ast
 open import Interp_utilities
 open import Pervasives
 
-type instr_parm_typ = 
+type instr_param_typ = 
 | IBit
 | IBitvector of maybe nat
 | IRange of maybe nat
@@ -10,7 +10,7 @@ type instr_parm_typ =
 | IOther
 
 type instruction_form = 
-|  Instr_form of string * list (string * instr_parm_typ) * list base_effect
+|  Instr_form of string * list (string * instr_param_typ) * list base_effect
 |  Skipped 
 
 val extract_instructions : string -> defs tannot -> list instruction_form
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 23d5c021..cbde6e8b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -7,6 +7,7 @@ open import Show_extra (* for 'show' to convert nat to string) *)
 open import String_extra (* for chr *)
 import Assert_extra (*For failwith when partiality is known to be unreachable*)
 
+open import Sail_impl_base
 open import Interp_ast
 open import Interp_utilities
 open import Instruction_extractor
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 483968ca..f4904669 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -2,10 +2,11 @@ import Interp
 import Interp_lib
 import Instruction_extractor
 import Set_extra
-open import Interp_ast
-open import Interp_interface
 open import Pervasives
 open import Assert_extra
+open import Interp_ast
+open import Sail_impl_base
+open import Interp_interface
 
 val intern_reg_value : register_value -> Interp.value
 val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value
@@ -126,7 +127,7 @@ let intern_ifield_value direction v =
 let num_to_bits size kind num =
 (* num_to_bits needed in src_power_get/trans_sail.gen - 
    rather than reengineer the generation, we include a wrapper here *) 
-  Interp_interface.bit_list_of_integer size num
+  Sail_impl_base.bit_list_of_integer size num
 
 let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
@@ -750,7 +751,7 @@ let rec interp_to_outcome mode context thunk =
             else Error "Memory address for write is not 64 bits"
           | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm)
         | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
-          (match List.lookup i mem_write_vals with
+           (match List.lookup i mem_write_vals with
             | (Just (MV parmf return)) -> 
               let (value, v_tracking) = 
                 match (Interp.detaint write_val) with
@@ -821,6 +822,52 @@ let interp mode (IState interp_state context) =
     | (o,_) -> o
 end 
 
+val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit unit
+val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit unit
+let rec outcome_to_outcome mode = function
+  | Interp_interface.Read_mem rk addr size _ k ->
+     Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v))
+  | Interp_interface.Write_mem rk addr size _ mv _ k ->
+     failwith "Write_mem not supported anymore"
+  | Interp_interface.Write_ea wk addr size _ state ->
+     Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state)
+  | Interp_interface.Write_memv _ mv _ k ->
+     Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v))
+  | Interp_interface.Barrier bk state ->
+     Sail_impl_base.Barrier bk (state_to_outcome_s mode state)
+  | Interp_interface.Footprint state ->
+     Sail_impl_base.Footprint (state_to_outcome_s mode state)
+  | Interp_interface.Read_reg r k ->
+     Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v))
+  | Interp_interface.Write_reg r rv state ->
+     Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state)
+  | Interp_interface.Nondet_choice _ _ ->
+     failwith "Nondet_choice not supported yet"
+  | Interp_interface.Escape maybestate _ ->
+     Sail_impl_base.Escape (Maybe.map (state_to_outcome_s mode) maybestate)
+  | Interp_interface.Fail maybestring ->
+     Sail_impl_base.Fail maybestring
+  | Interp_interface.Internal maybestring maybeprint state ->
+     Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state)
+  | Interp_interface.Analysis_non_det _ _ ->
+     failwith "Analysis_non_det outcome returned"
+  | Interp_interface.Done ->
+     Sail_impl_base.Done ()
+  | Interp_interface.Error message ->
+     failwith ("Interpreter error: " ^ message)
+end
+
+and state_to_outcome_s mode state = 
+  let next_outcome' = interp mode state in
+  let next_outcome = outcome_to_outcome mode next_outcome' in
+  (next_outcome, Just state)
+
+
+let initial_outcome_s_of_instruction context mode instruction =
+  let state = instruction_to_istate context instruction in
+  let initial_outcome' = interp mode state in
+  (outcome_to_outcome mode initial_outcome',Just state)
+
 
 (*Update slice potentially here*)
 let reg_size = function
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 18ec74a2..cf8c51a2 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -12,6 +12,7 @@ and change
 *)
 
 
+open import Sail_impl_base
 import Interp
 open import Interp_ast
 open import Pervasives
@@ -19,21 +20,6 @@ open import Num
 
 open import Assert_extra
 
-(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
-instance forall 'a. Ord 'a => (Ord (maybe 'a))
-  let compare = maybeCompare compare
-  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
-  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
-  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
-  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
-end
-
-type word8 = nat (* bounded at a byte, for when lem supports it*)
-
-type end_flag =
-  | E_big_endian
-  | E_little_endian
-
 type interpreter_state = Interp.stack (*Deem abstract*)
 (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
 type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
@@ -42,402 +28,7 @@ type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |>
 val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode
 val tracking_dependencies : interp_mode -> bool
 
-(** basic values *)
-
-type bit =
-  | Bitc_zero
-  | Bitc_one
-
-type bit_lifted = 
-  | Bitl_zero
-  | Bitl_one
-  | Bitl_undef
-  | Bitl_unknown
-
-type direction = 
-  | D_increasing
-  | D_decreasing
-
-type register_value = <| 
-    rv_bits: list bit_lifted (* MSB first, smallest index number *); 
-    rv_dir: direction; 
-    rv_start: nat ;
-    rv_start_internal: nat; 
-    (*when dir is increasing, rv_start = rv_start_internal. 
-      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
-    |>
-
-type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*)
-
-type instruction_field_value = list bit
-
-type byte = Byte of list bit (* of length 8 *)  (*MSB first everywhere*) 
-
-type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer
-(* for both values of end_flag, MSBy first *)
-
-type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*)
-
-type memory_value = list memory_byte
-(* the list is of length >=1 *)
-(* for both big-endian (Power) and little-endian (ARM), the head of the
-     list is the byte stored at the lowest address *)
-(* for big-endian Power the head of the list is the most-significant
-   byte, in both the interpreter and machineDef* code. *)
-(* For little-endian ARM, the head of the list is the
-   least-significant byte in machineDef* code and the
-   most-significant byte in interpreter code, with the switch over
-   (a list-reverse) being done just inside the interpreter interface*)
-(* In other words, in the machineDef* code the lowest-address byte is first,
-   and in the interpreter code the most-significant byte is first *)
-
-
-
-(* not sure which of these is more handy yet *)
-type address = Address of list byte (* of length 8 *) * integer
-(* type address = Address of integer *)
-
-type opcode = Opcode of list byte (* of length 4 *)
-
-(** typeclass instantiations *)
-
-let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
-  match (b1,b2) with
-  | (Bitc_zero, Bitc_zero) -> EQ
-  | (Bitc_one, Bitc_one) -> EQ
-  | (Bitc_zero, _) -> LT
-  | (_,_) -> GT
-  end
-let inline {ocaml} bitCompare = defaultCompare
-
-let ~{ocaml} bitLess b1 b2      = bitCompare b1 b2 =  LT
-let ~{ocaml} bitLessEq b1 b2    = bitCompare b1 b2 <> GT
-let ~{ocaml} bitGreater b1 b2   = bitCompare b1 b2 =  GT
-let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
-
-let inline {ocaml} bitLess      = defaultLess
-let inline {ocaml} bitLessEq    = defaultLessEq
-let inline {ocaml} bitGreater   = defaultGreater
-let inline {ocaml} bitGreaterEq = defaultGreaterEq
-
-instance (Ord bit)
-  let compare = bitCompare
-  let (<)  = bitLess
-  let (<=) = bitLessEq
-  let (>)  = bitGreater
-  let (>=) = bitGreaterEq
-end
-
-let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
-  match (bl1,bl2) with
-  | (Bitl_zero, Bitl_zero) -> EQ
-  | (Bitl_one, Bitl_one) -> EQ
-  | (Bitl_undef,Bitl_undef) -> EQ
-  | (Bitl_unknown,Bitl_unknown) -> EQ
-  | (Bitl_zero,_) -> LT
-  | (Bitl_one, _) -> LT
-  | (Bitl_undef, _) -> LT
-  | (_,_) -> GT
-  end
-let inline {ocaml} bit_liftedCompare = defaultCompare
-
-let ~{ocaml} bit_liftedLess b1 b2      = bit_liftedCompare b1 b2 =  LT
-let ~{ocaml} bit_liftedLessEq b1 b2    = bit_liftedCompare b1 b2 <> GT
-let ~{ocaml} bit_liftedGreater b1 b2   = bit_liftedCompare b1 b2 =  GT
-let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} bit_liftedLess      = defaultLess
-let inline {ocaml} bit_liftedLessEq    = defaultLessEq
-let inline {ocaml} bit_liftedGreater   = defaultGreater
-let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord bit_lifted)
-  let compare = bit_liftedCompare
-  let (<)  = bit_liftedLess
-  let (<=) = bit_liftedLessEq
-  let (>)  = bit_liftedGreater
-  let (>=) = bit_liftedGreaterEq
-end
-
-let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
-let inline {ocaml} byte_liftedCompare = defaultCompare
-
-let ~{ocaml} byte_liftedLess b1 b2      = byte_liftedCompare b1 b2 =  LT
-let ~{ocaml} byte_liftedLessEq b1 b2    = byte_liftedCompare b1 b2 <> GT
-let ~{ocaml} byte_liftedGreater b1 b2   = byte_liftedCompare b1 b2 =  GT
-let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} byte_liftedLess      = defaultLess
-let inline {ocaml} byte_liftedLessEq    = defaultLessEq
-let inline {ocaml} byte_liftedGreater   = defaultGreater
-let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord byte_lifted)
-  let compare = byte_liftedCompare
-  let (<)  = byte_liftedLess
-  let (<=) = byte_liftedLessEq
-  let (>)  = byte_liftedGreater
-  let (>=) = byte_liftedGreaterEq
-end
-
-let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2
-let inline {ocaml} byteCompare = defaultCompare
-
-let ~{ocaml} byteLess b1 b2      = byteCompare b1 b2 =  LT
-let ~{ocaml} byteLessEq b1 b2    = byteCompare b1 b2 <> GT
-let ~{ocaml} byteGreater b1 b2   = byteCompare b1 b2 =  GT
-let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT
-
-let inline {ocaml} byteLess      = defaultLess
-let inline {ocaml} byteLessEq    = defaultLessEq
-let inline {ocaml} byteGreater   = defaultGreater
-let inline {ocaml} byteGreaterEq = defaultGreaterEq
-
-instance (Ord byte)
-  let compare = byteCompare
-  let (<)  = byteLess
-  let (<=) = byteLessEq
-  let (>)  = byteGreater
-  let (>=) = byteGreaterEq
-end
-
-let (*~{ocaml}*) addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
-(*let inline {ocaml} addressCompare = defaultCompare*)
-
-let ~{ocaml} addressLess b1 b2      = addressCompare b1 b2 =  LT
-let ~{ocaml} addressLessEq b1 b2    = addressCompare b1 b2 <> GT
-let ~{ocaml} addressGreater b1 b2   = addressCompare b1 b2 =  GT
-let ~{ocaml} addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT
-
-let inline {ocaml} addressLess      = defaultLess
-let inline {ocaml} addressLessEq    = defaultLessEq
-let inline {ocaml} addressGreater   = defaultGreater
-let inline {ocaml} addressGreaterEq = defaultGreaterEq
-
-instance (Ord address)
-  let compare = addressCompare
-  let (<)  = addressLess
-  let (<=) = addressLessEq
-  let (>)  = addressGreater
-  let (>=) = addressGreaterEq
-end
-
-let {coq} addressEqual a1 a2 = (addressCompare a1 a2) = EQ
-let inline ~{coq} addressEqual = unsafe_structural_equality
-
-let {coq} addressInequal a1 a2 = not (addressEqual a1 a2)
-let inline ~{coq} addressInequal = unsafe_structural_inequality
-
-instance  (Eq address)
-  let (=)  = addressEqual
-  let (<>) = addressInequal
-end
-
-let ~{ocaml} directionCompare d1 d2 =
-  match (d1, d2) with
-  | (D_decreasing, D_increasing) -> GT
-  | (D_increasing, D_decreasing) -> LT
-  | _ -> EQ
-  end
-let inline {ocaml} directionCompare = defaultCompare
-
-let ~{ocaml} directionLess b1 b2      = directionCompare b1 b2 =  LT
-let ~{ocaml} directionLessEq b1 b2    = directionCompare b1 b2 <> GT
-let ~{ocaml} directionGreater b1 b2   = directionCompare b1 b2 =  GT
-let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT
-
-let inline {ocaml} directionLess      = defaultLess
-let inline {ocaml} directionLessEq    = defaultLessEq
-let inline {ocaml} directionGreater   = defaultGreater
-let inline {ocaml} directionGreaterEq = defaultGreaterEq
 
-instance (Ord direction)
-  let compare = directionCompare
-  let (<)  = directionLess
-  let (<=) = directionLessEq
-  let (>)  = directionGreater
-  let (>=) = directionGreaterEq
-end
-
-let ~{ocaml} register_valueCompare rv1 rv2 =
-  compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal)
-          (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal)
-let inline {ocaml} register_valueCompare = defaultCompare
-
-let ~{ocaml} register_valueLess b1 b2      = register_valueCompare b1 b2 =  LT
-let ~{ocaml} register_valueLessEq b1 b2    = register_valueCompare b1 b2 <> GT
-let ~{ocaml} register_valueGreater b1 b2   = register_valueCompare b1 b2 =  GT
-let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT
-
-let inline {ocaml} register_valueLess      = defaultLess
-let inline {ocaml} register_valueLessEq    = defaultLessEq
-let inline {ocaml} register_valueGreater   = defaultGreater
-let inline {ocaml} register_valueGreaterEq = defaultGreaterEq
-
-instance (Ord register_value)
-  let compare = register_valueCompare
-  let (<)  = register_valueLess
-  let (<=) = register_valueLessEq
-  let (>)  = register_valueGreater
-  let (>=) = register_valueGreaterEq
-end
-
-let ~{ocaml} address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) =
-  compare (b1,i1) (b2,i2)
-let inline {ocaml} address_liftedCompare = defaultCompare
-
-let ~{ocaml} address_liftedLess b1 b2      = address_liftedCompare b1 b2 =  LT
-let ~{ocaml} address_liftedLessEq b1 b2    = address_liftedCompare b1 b2 <> GT
-let ~{ocaml} address_liftedGreater b1 b2   = address_liftedCompare b1 b2 =  GT
-let ~{ocaml} address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} address_liftedLess      = defaultLess
-let inline {ocaml} address_liftedLessEq    = defaultLessEq
-let inline {ocaml} address_liftedGreater   = defaultGreater
-let inline {ocaml} address_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord address_lifted)
-  let compare = address_liftedCompare
-  let (<)  = address_liftedLess
-  let (<=) = address_liftedLessEq
-  let (>)  = address_liftedGreater
-  let (>=) = address_liftedGreaterEq
-end
-
-(* Registers *)
-type slice = (nat * nat)
-
-type reg_name = 
-| Reg of string * nat * nat * direction
-(*Name of the register, accessing the entire register, the start and size of this register, and its direction *)
-
-| Reg_slice of string * nat * direction * slice 
-(* Name of the register, accessing from the bit indexed by the first
-to the bit indexed by the second integer of the slice, inclusive. For
-machineDef* the first is a smaller number or equal to the second, adjusted
-to reflect the correct span direction in the interpreter side.  *)
-
-| Reg_field of string * nat * direction * string * slice 
-(*Name of the register, start and direction, and name of the field of the register
-accessed. The slice specifies where this field is in the register*)
-
-| Reg_f_slice of string * nat * direction * string * slice * slice 
-(* The first four components are as in Reg_field; the final slice
-specifies a part of the field, indexed w.r.t. the register as a whole *)
-
-let register_base_name : reg_name -> string = function
-  | Reg s _ _ _             -> s
-  | Reg_slice s _ _ _       -> s
-  | Reg_field s _ _ _ _     -> s
-  | Reg_f_slice s _ _ _ _ _ -> s
-  end
-
-let slice_of_reg_name : reg_name -> slice = function
-  | Reg _ start width D_increasing -> (start, start + width -1)
-  | Reg _ start width D_decreasing -> (start - width - 1, start)
-  | Reg_slice _ _ _ sl             -> sl
-  | Reg_field _ _ _ _ sl           -> sl
-  | Reg_f_slice _ _ _ _ _ sl       -> sl
-  end
-
-let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = 
-  register_base_name r = register_base_name r' &&
-  let (i1,  i2)  = slice_of_reg_name r in
-  let (i1', i2') = slice_of_reg_name r' in
-  i1' <= i2 && i2' >= i1
-
-
-let reg_nameCompare r1 r2 = 
-  compare (register_base_name r1,slice_of_reg_name r1)
-          (register_base_name r2,slice_of_reg_name r2)
-
-let reg_nameLess b1 b2      = reg_nameCompare b1 b2 =  LT
-let reg_nameLessEq b1 b2    = reg_nameCompare b1 b2 <> GT
-let reg_nameGreater b1 b2   = reg_nameCompare b1 b2 =  GT
-let reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT
-
-instance (Ord reg_name)
-  let compare = reg_nameCompare
-  let (<)  = reg_nameLess
-  let (<=) = reg_nameLessEq
-  let (>)  = reg_nameGreater
-  let (>=) = reg_nameGreaterEq
-end
-
-let reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ
-let reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2)
-
-instance  (Eq reg_name)
-  let (=)  = reg_nameEqual
-  let (<>) = reg_nameInequal
-end
-
-instance (SetType reg_name)
-  let setElemCompare = reg_nameCompare
-end
-
-let direction_of_reg_name r = match r with
-  | Reg _ _ _ d -> d
-  | Reg_slice _ _ d _ -> d
-  | Reg_field _ _ d _ _ -> d
-  | Reg_f_slice _ _ d _ _ _ -> d
- end
-
-let start_of_reg_name r = match r with
-  | Reg _ start _ _ -> start
-  | Reg_slice _ start _ _ -> start
-  | Reg_field _ start _ _ _ -> start
-  | Reg_f_slice _ start _ _ _ _ -> start
-end
-
-(* Data structures for building up instructions *)
-
-type read_kind =
-  (* common reads *)
-  Read_plain
-  | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
-  (* Power reads *)
-  | Read_reserve
-  (* AArch64 reads *)
-  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
-
-instance (Show read_kind)
-  let show = function
-    | Read_plain -> "Read_plain"
-    | Read_tag -> "Read_tag"
-    | Read_reserve -> "Read_reserve"
-    | Read_acquire -> "Read_acquire"
-    | Read_exclusive -> "Read_exclusive"
-    | Read_exclusive_acquire -> "Read_exclusive_acquire"
-    | Read_stream -> "Read_stream"
-  end
-end
-
-type write_kind =
-  (* common writes *)
-    Write_plain
-  | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
-  (* Power writes *)
-  | Write_conditional
-  (* AArch64 writes *)
-  | Write_release | Write_exclusive | Write_exclusive_release
-
-type barrier_kind =
-  (* Power barriers *)
-  Sync | LwSync | Eieio | Isync
-  (* AArch64 barriers *)
-  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
-
-type instruction_kind = 
-  | IK_barrier of barrier_kind 
-  | IK_mem_read of read_kind 
-  | IK_mem_write of write_kind
-(* SS reinstating cond_branches
-at present branches are not distinguished in the instruction_kind;
-they just have particular nias (and will be IK_simple *)
-  | IK_cond_branch 
-(*  | IK_uncond_branch *)
-  | IK_simple
 
 (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
 type external_functions = list (string * (Interp.value -> Interp.value))
@@ -485,7 +76,7 @@ type outcome =
 (* List of instruciton states to be run in parrallel, any order permitted *)
 | Nondet_choice of list instruction_state * instruction_state
 (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler 
-   The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp*)
+   The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp *)
 | Escape of maybe instruction_state * instruction_state
 (*Result of a failed assert with possible error message to report*)
 | Fail of maybe string
@@ -511,277 +102,6 @@ type event =
 | E_escape
 | E_error of string 
 
-(* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*)
-
-let ~{ocaml} read_kindCompare rk1 rk2 =
-  match (rk1, rk2) with
-  | (Read_plain, Read_plain)             -> EQ
-  | (Read_plain, Read_reserve)           -> LT
-  | (Read_plain, Read_acquire)           -> LT
-  | (Read_plain, Read_exclusive)         -> LT
-  | (Read_plain, Read_exclusive_acquire) -> LT
-  | (Read_plain, Read_stream)            -> LT
-
-  | (Read_reserve, Read_plain)             -> GT
-  | (Read_reserve, Read_reserve)           -> EQ
-  | (Read_reserve, Read_acquire)           -> LT
-  | (Read_reserve, Read_exclusive)         -> LT
-  | (Read_reserve, Read_exclusive_acquire) -> LT
-  | (Read_reserve, Read_stream)            -> LT
-
-  | (Read_acquire, Read_plain)             -> GT
-  | (Read_acquire, Read_reserve)           -> GT
-  | (Read_acquire, Read_acquire)           -> EQ
-  | (Read_acquire, Read_exclusive)         -> LT
-  | (Read_acquire, Read_exclusive_acquire) -> LT
-  | (Read_acquire, Read_stream)            -> LT
-
-  | (Read_exclusive, Read_plain)             -> GT
-  | (Read_exclusive, Read_reserve)           -> GT
-  | (Read_exclusive, Read_acquire)           -> GT
-  | (Read_exclusive, Read_exclusive)         -> EQ
-  | (Read_exclusive, Read_exclusive_acquire) -> LT
-  | (Read_exclusive, Read_stream)            -> LT
-
-  | (Read_exclusive_acquire, Read_plain)             -> GT
-  | (Read_exclusive_acquire, Read_reserve)           -> GT
-  | (Read_exclusive_acquire, Read_acquire)           -> GT
-  | (Read_exclusive_acquire, Read_exclusive)         -> GT
-  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
-  | (Read_exclusive_acquire, Read_stream)            -> GT
-
-  | (Read_stream, Read_plain)             -> GT
-  | (Read_stream, Read_reserve)           -> GT
-  | (Read_stream, Read_acquire)           -> GT
-  | (Read_stream, Read_exclusive)         -> GT
-  | (Read_stream, Read_exclusive_acquire) -> GT
-  | (Read_stream, Read_stream)            -> EQ
-  end
-let inline {ocaml} read_kindCompare = defaultCompare
-
-let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
-let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
-let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
-let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
-
-let inline {ocaml} read_kindLess      = defaultLess
-let inline {ocaml} read_kindLessEq    = defaultLessEq
-let inline {ocaml} read_kindGreater   = defaultGreater
-let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
-
-instance (Ord read_kind)
-  let compare = read_kindCompare
-  let (<)  = read_kindLess
-  let (<=) = read_kindLessEq
-  let (>)  = read_kindGreater
-  let (>=) = read_kindGreaterEq
-end
-
-let ~{ocaml} write_kindCompare wk1 wk2 =
-  match (wk1, wk2) with
-  | (Write_plain, Write_plain)             -> EQ
-  | (Write_plain, Write_conditional)       -> LT
-  | (Write_plain, Write_release)           -> LT
-  | (Write_plain, Write_exclusive)         -> LT
-  | (Write_plain, Write_exclusive_release) -> LT
-
-  | (Write_conditional, Write_plain)             -> GT
-  | (Write_conditional, Write_conditional)       -> EQ
-  | (Write_conditional, Write_release)           -> LT
-  | (Write_conditional, Write_exclusive)         -> LT
-  | (Write_conditional, Write_exclusive_release) -> LT
-
-  | (Write_release, Write_plain)             -> GT
-  | (Write_release, Write_conditional)       -> GT
-  | (Write_release, Write_release)           -> EQ
-  | (Write_release, Write_exclusive)         -> LT
-  | (Write_release, Write_exclusive_release) -> LT
-
-  | (Write_exclusive, Write_plain)             -> GT
-  | (Write_exclusive, Write_conditional)       -> GT
-  | (Write_exclusive, Write_release)           -> GT
-  | (Write_exclusive, Write_exclusive)         -> EQ
-  | (Write_exclusive, Write_exclusive_release) -> LT
-
-  | (Write_exclusive_release, Write_plain)             -> GT
-  | (Write_exclusive_release, Write_conditional)       -> GT
-  | (Write_exclusive_release, Write_release)           -> GT
-  | (Write_exclusive_release, Write_exclusive)         -> GT
-  | (Write_exclusive_release, Write_exclusive_release) -> EQ
-  end
-let inline {ocaml} write_kindCompare = defaultCompare
-
-let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
-let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
-let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
-let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
-
-let inline {ocaml} write_kindLess      = defaultLess
-let inline {ocaml} write_kindLessEq    = defaultLessEq
-let inline {ocaml} write_kindGreater   = defaultGreater
-let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
-
-instance (Ord write_kind)
-  let compare = write_kindCompare
-  let (<)  = write_kindLess
-  let (<=) = write_kindLessEq
-  let (>)  = write_kindGreater
-  let (>=) = write_kindGreaterEq
-end
-
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  match (bk1, bk2) with
-  | (Sync, Sync)   -> EQ
-  | (Sync, LwSync) -> LT
-  | (Sync, Eieio)  -> LT
-  | (Sync, Isync)  -> LT
-  | (Sync, DMB)    -> LT
-  | (Sync, DMB_ST) -> LT
-  | (Sync, DMB_LD) -> LT
-  | (Sync, DSB)    -> LT
-  | (Sync, DSB_ST) -> LT
-  | (Sync, DSB_LD) -> LT
-  | (Sync, ISB)    -> LT
-
-  | (LwSync, Sync)   -> GT
-  | (LwSync, LwSync) -> EQ
-  | (LwSync, Eieio)  -> LT
-  | (LwSync, Isync)  -> LT
-  | (LwSync, DMB)    -> LT
-  | (LwSync, DMB_ST) -> LT
-  | (LwSync, DMB_LD) -> LT
-  | (LwSync, DSB)    -> LT
-  | (LwSync, DSB_ST) -> LT
-  | (LwSync, DSB_LD) -> LT
-  | (LwSync, ISB)    -> LT
-
-  | (Eieio, Sync)   -> GT
-  | (Eieio, LwSync) -> GT
-  | (Eieio, Eieio)  -> EQ
-  | (Eieio, Isync)  -> LT
-  | (Eieio, DMB)    -> LT
-  | (Eieio, DMB_ST) -> LT
-  | (Eieio, DMB_LD) -> LT
-  | (Eieio, DSB)    -> LT
-  | (Eieio, DSB_ST) -> LT
-  | (Eieio, DSB_LD) -> LT
-  | (Eieio, ISB)    -> LT
-
-  | (Isync, Sync)   -> GT
-  | (Isync, LwSync) -> GT
-  | (Isync, Eieio)  -> GT
-  | (Isync, Isync)  -> EQ
-  | (Isync, DMB)    -> LT
-  | (Isync, DMB_ST) -> LT
-  | (Isync, DMB_LD) -> LT
-  | (Isync, DSB)    -> LT
-  | (Isync, DSB_ST) -> LT
-  | (Isync, DSB_LD) -> LT
-  | (Isync, ISB)    -> LT
-
-  | (DMB, Sync)   -> GT
-  | (DMB, LwSync) -> GT
-  | (DMB, Eieio)  -> GT
-  | (DMB, ISync)  -> GT
-  | (DMB, DMB)    -> EQ
-  | (DMB, DMB_ST) -> LT
-  | (DMB, DMB_LD) -> LT
-  | (DMB, DSB)    -> LT
-  | (DMB, DSB_ST) -> LT
-  | (DMB, DSB_LD) -> LT
-  | (DMB, ISB)    -> LT
-
-  | (DMB_ST, Sync)   -> GT
-  | (DMB_ST, LwSync) -> GT
-  | (DMB_ST, Eieio)  -> GT
-  | (DMB_ST, ISync)  -> GT
-  | (DMB_ST, DMB)    -> GT
-  | (DMB_ST, DMB_ST) -> EQ
-  | (DMB_ST, DMB_LD) -> LT
-  | (DMB_ST, DSB)    -> LT
-  | (DMB_ST, DSB_ST) -> LT
-  | (DMB_ST, DSB_LD) -> LT
-  | (DMB_ST, ISB)    -> LT
-
-  | (DMB_LD, Sync)   -> GT
-  | (DMB_LD, LwSync) -> GT
-  | (DMB_LD, Eieio)  -> GT
-  | (DMB_LD, ISync)  -> GT
-  | (DMB_LD, DMB)    -> GT
-  | (DMB_LD, DMB_ST) -> GT
-  | (DMB_LD, DMB_LD) -> EQ
-  | (DMB_LD, DSB)    -> LT
-  | (DMB_LD, DSB_ST) -> LT
-  | (DMB_LD, DSB_LD) -> LT
-  | (DMB_LD, ISB)    -> LT
-
-  | (DSB, Sync)   -> GT
-  | (DSB, LwSync) -> GT
-  | (DSB, Eieio)  -> GT
-  | (DSB, ISync)  -> GT
-  | (DSB, DMB)    -> GT
-  | (DSB, DMB_ST) -> GT
-  | (DSB, DMB_LD) -> GT
-  | (DSB, DSB)    -> EQ
-  | (DSB, DSB_ST) -> LT
-  | (DSB, DSB_LD) -> LT
-  | (DSB, ISB)    -> LT
-
-  | (DSB_ST, Sync)   -> GT
-  | (DSB_ST, LwSync) -> GT
-  | (DSB_ST, Eieio)  -> GT
-  | (DSB_ST, ISync)  -> GT
-  | (DSB_ST, DMB)    -> GT
-  | (DSB_ST, DMB_ST) -> GT
-  | (DSB_ST, DMB_LD) -> GT
-  | (DSB_ST, DSB)    -> GT
-  | (DSB_ST, DSB_ST) -> EQ
-  | (DSB_ST, DSB_LD) -> LT
-  | (DSB_ST, ISB)    -> LT
-
-  | (DSB_LD, Sync)   -> GT
-  | (DSB_LD, LwSync) -> GT
-  | (DSB_LD, Eieio)  -> GT
-  | (DSB_LD, ISync)  -> GT
-  | (DSB_LD, DMB)    -> GT
-  | (DSB_LD, DMB_ST) -> GT
-  | (DSB_LD, DMB_LD) -> GT
-  | (DSB_LD, DSB)    -> GT
-  | (DSB_LD, DSB_ST) -> GT
-  | (DSB_LD, DSB_LD) -> EQ
-  | (DSB_LD, ISB)    -> LT
-                          
-  | (ISB, Sync)   -> GT
-  | (ISB, LwSync) -> GT
-  | (ISB, Eieio)  -> GT
-  | (ISB, ISync)  -> GT
-  | (ISB, DMB)    -> GT
-  | (ISB, DMB_ST) -> GT
-  | (ISB, DMB_LD) -> GT
-  | (ISB, DSB)    -> GT
-  | (ISB, DSB_ST) -> GT
-  | (ISB, DSB_LD) -> GT
-  | (ISB, ISB)    -> EQ
-  end
-let inline {ocaml} barrier_kindCompare = defaultCompare
-
-let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
-let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
-let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
-let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
-
-let inline {ocaml} barrier_kindLess      = defaultLess
-let inline {ocaml} barrier_kindLessEq    = defaultLessEq
-let inline {ocaml} barrier_kindGreater   = defaultGreater
-let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
-
-instance (Ord barrier_kind)
-  let compare = barrier_kindCompare
-  let (<)  = barrier_kindLess
-  let (<=) = barrier_kindLessEq
-  let (>)  = barrier_kindGreater
-  let (>=) = barrier_kindGreaterEq
-end
 
 let ~{ocaml} eventCompare e1 e2 = 
   match (e1,e2) with
@@ -830,74 +150,12 @@ instance (SetType event)
   let setElemCompare = compare
 end
 
+
 (* Functions to build up the initial state for interpretation *)
 val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context 
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
-(*Type representint the constructor parameters in instruction, other is a type not representable externally*)
-type instr_parm_typ = 
-  | Bit (*A single bit, represented as a one element Bitvector as a value*)
-  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
-  | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *)
-  | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
-  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-
-let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
-  | (Bit,Bit) -> true
-  | (Bvector i1,Bvector i2) -> i1 = i2
-  | (Range i1,Range i2) -> i1 = i2
-  | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
-  | (Other,Other) -> true
-  | _ -> false
-end
-let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality
-
-let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality
-
-instance (Eq instr_parm_typ) 
-  let (=) = instr_parm_typEqual
-  let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-end 
-
-let instr_parm_typShow ip = match ip with
-  | Bit -> "Bit"
-  | Bvector i -> "Bvector " ^ show i
-  | Range i -> "Range " ^ show i
-  | Enum s i -> "Enum " ^ s ^ " " ^ show i
-  | Other -> "Other"
- end
-
-instance (Show instr_parm_typ)
-let show = instr_parm_typShow
-end
-
-(*A representation of the AST node for each instruction in the spec, with concrete values from this call,
-  and the potential static effects from the funcl clause for this instruction 
-  Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
-*)
-type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
-
-let {coq} instructionEqual i1 i2 = match (i1,i2) with
-  | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
-end
-let inline ~{coq} instructionEqual = unsafe_structural_equality
-
-let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2)
-let inline ~{coq} instructionInequal = unsafe_structural_inequality
-
-type v_kind = Bitv | Bytev
-
-type decode_error = 
-  | Unsupported_instruction_error of instruction
-  | Not_an_instruction_error of opcode
-  | Internal_error of string
-
-type instruction_or_decode_error =
-  | IDE_instr of instruction
-  | IDE_decode_error of decode_error
-
 (** propose to remove the following type and use the above instead *)
 type i_state_or_error =
   | Instr of instruction * instruction_state
@@ -930,553 +188,14 @@ val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_
 (* As above, but will request register reads: outcome will only be rreg, done, or error *)
 val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 
 
-
-(** operations and coercions on basic values *)
-
-val word8_to_bitls : word8 -> list bit_lifted
-val bitls_to_word8 : list bit_lifted -> word8
-
-val integer_of_word8_list : list word8 -> integer
-val word8_list_of_integer : integer -> integer -> list word8 
-
-val concretizable_bitl : bit_lifted -> bool
-val concretizable_bytl : byte_lifted -> bool
-val concretizable_bytls : list byte_lifted -> bool
-
-let concretizable_bitl = function
-  | Bitl_zero -> true
-  | Bitl_one -> true
-  | Bitl_undef -> false
-  | Bitl_unknown -> false
-end 
-
-let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs
-let concretizable_bytls = List.all concretizable_bytl
-
-(* constructing values *)
-
-val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value
-let build_register_value bs dir width start_index =
-  <| rv_bits = bs;
-     rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
-     rv_start_internal = start_index; 
-     rv_start = if dir = D_increasing 
-       then start_index 
-       else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *)
-  |>
-
-val register_value : bit_lifted -> direction -> nat -> nat -> register_value
-let register_value b dir width start_index = 
-  build_register_value (List.replicate width b) dir width start_index
-
-val register_value_zeros : direction -> nat -> nat -> register_value
-let register_value_zeros dir width start_index = 
-  register_value Bitl_zero dir width start_index
-
-val register_value_ones : direction -> nat -> nat -> register_value
-let register_value_ones dir width start_index = 
-  register_value Bitl_one dir width start_index
-
-val byte_lifted_undef : byte_lifted
-let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef)
-
-val byte_lifted_unknown : byte_lifted
-let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown)
-  
-val memory_value_unknown : nat (*the number of bytes*) -> memory_value
-let memory_value_unknown (width:nat) : memory_value = 
-  List.replicate width byte_lifted_unknown 
-
-val memory_value_undef : nat (*the number of bytes*) -> memory_value
-let memory_value_undef (width:nat) : memory_value = 
-  List.replicate width byte_lifted_undef 
-
-(* lengths *)  
-
-val memory_value_length : memory_value -> nat
-let memory_value_length (mv:memory_value) = List.length mv
-
-
-(* aux fns *)
-
-val maybe_all : forall 'a.  list (maybe 'a) -> maybe (list 'a)
-let rec maybe_all' xs acc = 
-  match xs with
-  | [] -> Just (List.reverse acc)
-  | Nothing :: _ -> Nothing
-  | (Just y)::xs' -> maybe_all' xs' (y::acc)
-  end
-let maybe_all xs = maybe_all' xs [] 
-
-(** coercions *)
-
-(* bits and bytes *)
-
-let bit_to_bool = function (* TODO: rename bool_of_bit *)
-  | Bitc_zero -> false
-  | Bitc_one -> true
-end
-
-
-val bit_lifted_of_bit : bit -> bit_lifted
-let bit_lifted_of_bit b = 
-  match b with
-  | Bitc_zero -> Bitl_zero
-  | Bitc_one -> Bitl_one
-  end
-
-val bit_of_bit_lifted : bit_lifted -> maybe bit
-let bit_of_bit_lifted bl =
-  match bl with
-  | Bitl_zero -> Just Bitc_zero
-  | Bitl_one -> Just Bitc_one
-  | Bitl_undef -> Nothing
-  | Bitl_unknown -> Nothing
-  end
-
-
-val byte_lifted_of_byte : byte -> byte_lifted
-let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs)
-
-val byte_of_byte_lifted : byte_lifted -> maybe byte
-let byte_of_byte_lifted bl = 
-  match bl with
-  | Byte_lifted bls -> 
-      match maybe_all (List.map bit_of_bit_lifted bls) with
-      | Nothing -> Nothing
-      | Just bs -> Just (Byte bs)
-      end
-  end
-
-
-val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*)
-let rec bytes_of_bits bits = match bits with
-  | [] -> []
-  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
-    (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits)
-  | _ -> failwith "bytes_of_bits not given bits divisible by 8"
-end
-
-val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*)
-let rec byte_lifteds_of_bit_lifteds bits = match bits with
-  | [] -> []
-  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
-    (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits)
-  | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8"
-end
-
-
-val byte_of_memory_byte : memory_byte -> maybe byte
-let byte_of_memory_byte = byte_of_byte_lifted
-
-val memory_byte_of_byte : byte -> memory_byte
-let memory_byte_of_byte = byte_lifted_of_byte
-
-
-(* to and from nat *)
-
-(* this natFromBoolList could move to the Lem word.lem library *)
-val natFromBoolList : list bool -> nat
-let rec natFromBoolListAux (acc : nat) (bl : list bool) = 
-  match bl with 
-    | [] -> acc
-    | (true :: bl') -> natFromBoolListAux ((acc * 2) + 1) bl'
-    | (false :: bl') -> natFromBoolListAux (acc * 2) bl'
-  end
-let natFromBoolList bl = 
-  natFromBoolListAux 0 (List.reverse bl)
-
-
-val nat_of_bit_list : list bit -> nat 
-let nat_of_bit_list b =
-  natFromBoolList (List.reverse (List.map bit_to_bool b))
-  (* natFromBoolList takes a list with LSB first, for consistency with rest of Lem word library, so we reverse it. twice. *)
-
-
-(* to and from integer *)
-
-val integer_of_bit_list : list bit -> integer 
-let integer_of_bit_list b =
-  integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
-  (* integerFromBoolList takes a list with LSB first, so we reverse it *)
-
-val bit_list_of_integer : nat -> integer -> list bit 
-let bit_list_of_integer len b = 
-  List.map (fun b -> if b then Bitc_one else Bitc_zero) 
-    (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b)))
-
-val integer_of_byte_list : list byte -> integer 
-let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
-
-val byte_list_of_integer : nat -> integer -> list byte 
-let byte_list_of_integer (len:nat) (a:integer):list byte = 
-  let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
-
-
-val integer_of_address : address -> integer 
-let integer_of_address (a:address):integer = 
-  match a with
-  | Address bs i -> i 
-  end
-
-val address_of_integer : integer -> address 
-let address_of_integer (i:integer):address =
-  Address (byte_list_of_integer 8 i) i
-
-(* to and from signed-integer *)
-
-val signed_integer_of_bit_list : list bit -> integer
-let signed_integer_of_bit_list b =
-  match b with
-  | [] -> failwith "empty bit list"
-  | Bitc_zero :: b' ->
-      integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
-  | Bitc_one :: b' ->
-      let b'_val = integerFromBoolList (false,(List.reverse (List.map bit_to_bool b'))) in
-      (* integerFromBoolList takes a list with LSB first, so we reverse it *)
-      let msb_val = integerPow 2 ((List.length b) - 1) in
-      b'_val - msb_val
-  end
-
-
-(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *)
-val integer_address_of_int_list : list int -> integer
-let rec integerFromIntListAux (acc: integer) (is: list int) = 
-  match is with 
-  | [] -> acc
-  | (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is'
-  end
-let integer_address_of_int_list (is: list int) =
-  integerFromIntListAux 0 is
-
-val address_of_byte_list : list byte -> address 
-let address_of_byte_list bs = 
-  if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else 
-  Address bs (integer_of_byte_list bs)
-
-(* operations on addresses *)
-
-val add_address_nat : address -> nat -> address 
-let add_address_nat (a:address) (i:nat) : address = 
-  address_of_integer ((integer_of_address a) + (integerFromNat i))
-
-val clear_low_order_bits_of_address : address -> address 
-let clear_low_order_bits_of_address a = 
-  match a with 
-  | Address [b0;b1;b2;b3;b4;b5;b6;b7] i -> 
-      match b7 with
-      | Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] -> 
-          let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in
-	  let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in
-          Address bytes (integer_of_byte_list bytes)
-      | _ -> failwith "Byte does not contain 8 bits"
-      end
-  | _ -> failwith "Address does not contain 8 bytes"
-  end
-
 val translate_address :
   context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address
   -> maybe address * maybe (list event)
 
-val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
-let byte_list_of_memory_value endian mv = 
-  let mv = if endian = E_big_endian then mv else List.reverse mv in
-  maybe_all (List.map byte_of_memory_byte mv)
-    
-
-val integer_of_memory_value : end_flag -> memory_value -> maybe integer 
-let integer_of_memory_value endian (mv:memory_value):maybe integer = 
-  match byte_list_of_memory_value endian mv with
-  | Just bs -> Just (integer_of_byte_list bs)
-  | Nothing -> Nothing 
-  end
-
-val memory_value_of_integer : end_flag  -> nat -> integer -> memory_value 
-let memory_value_of_integer endian (len:nat) (i:integer):memory_value =
-  let mv = List.map (byte_lifted_of_byte) (byte_list_of_integer len i) in
-  if endian = E_big_endian then mv else List.reverse mv
-
-
-val integer_of_register_value : register_value -> maybe integer 
-let integer_of_register_value (rv:register_value):maybe integer = 
-  match maybe_all (List.map bit_of_bit_lifted rv.rv_bits) with
-  | Nothing -> Nothing
-  | Just bs -> Just (integer_of_bit_list bs)
-  end 
-  
-val register_value_of_integer : nat -> nat -> direction -> integer -> register_value 
-let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value =
-  let bs = bit_list_of_integer len i in
-  build_register_value (List.map bit_lifted_of_bit bs) dir len start
-
-(* *)
-
-val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
-let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3]
-
-val register_value_of_address : address -> direction -> register_value   
-let register_value_of_address (Address bytes _) dir : register_value = 
-  let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in
-   <| rv_bits = bits;
-      rv_dir = dir;
-      rv_start = 0; 
-      rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1
-   |>
-
-val register_value_of_memory_value : memory_value -> direction -> register_value
-let register_value_of_memory_value bytes dir : register_value =
-  let bitls = List.concatMap (fun (Byte_lifted bs) -> bs) bytes in
-  <| rv_bits = bitls;
-     rv_dir = dir;
-     rv_start = 0;
-     rv_start_internal = if dir = D_increasing then 0 else (List.length bitls) - 1
-   |>                                                     
-
-val memory_value_of_register_value: register_value -> memory_value
-let memory_value_of_register_value r =
-  (byte_lifteds_of_bit_lifteds r.rv_bits)
-   
-val address_lifted_of_register_value : register_value -> maybe address_lifted
-(* returning Nothing iff the register value is not 64 bits wide, but
-allowing Bitl_undef and Bitl_unknown *)
-let address_lifted_of_register_value (rv:register_value) : maybe address_lifted = 
-  if List.length rv.rv_bits <> 64 then Nothing
-  else 
-    Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits)
-                         (if List.all concretizable_bitl rv.rv_bits 
-			  then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with
-                              | (Just(bits)) -> Just (integer_of_bit_list bits)
-                              | Nothing -> Nothing end
-			  else Nothing))
-
-val address_of_address_lifted : address_lifted -> maybe address
-(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *)
-let address_of_address_lifted (al:address_lifted): maybe address =
-  match al with
-  | Address_lifted bls (Just i)-> 
-      match maybe_all ((List.map byte_of_byte_lifted) bls) with
-      | Nothing -> Nothing
-      | Just bs -> Just (Address bs i)
-      end
-  | _ -> Nothing
-end
-
-val address_of_register_value : register_value -> maybe address
-(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *)
-let address_of_register_value (rv:register_value) : maybe address = 
-  match address_lifted_of_register_value rv with
-  | Nothing -> Nothing
-  | Just al -> 
-      match address_of_address_lifted al with
-      | Nothing -> Nothing
-      | Just a -> Just a
-      end
-  end
-
-let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address = 
-  match byte_list_of_memory_value endian mv with
-  | Nothing -> Nothing
-  | Just bs -> 
-      if List.length bs <> 8 then Nothing else
-      Just (address_of_byte_list bs)
-  end 
-
-val byte_of_int : int -> byte
-let byte_of_int (i:int) : byte = 
-  Byte (bit_list_of_integer 8 (integerFromInt i))
-
-val memory_byte_of_int : int -> memory_byte
-let memory_byte_of_int (i:int) : memory_byte = 
-  memory_byte_of_byte (byte_of_int i)
-
-(*
-val int_of_memory_byte : int -> maybe memory_byte
-let int_of_memory_byte (mb:memory_byte) : int = 
-  failwith "TODO"
-*)
-
-
-
-
-val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value
-let memory_value_of_address_lifted endian (al:address_lifted) =
-  match al with
-  | Address_lifted bs _ -> if endian = E_big_endian then bs else List.reverse bs
-  end
-
-val byte_list_of_address : address -> list byte
-let byte_list_of_address (a:address) : list byte = 
-  match a with
-  | Address bs _ -> bs
-  end
-
-val memory_value_of_address : end_flag -> address -> memory_value
-let memory_value_of_address endian addr =
-  match addr with
-  | Address bs _ -> List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs)
-  end
-
-val byte_list_of_opcode : opcode -> list byte
-let byte_list_of_opcode (opc:opcode) : list byte = 
-  match opc with
-  | Opcode bs -> bs
- end
-
-(** ****************************************** *)
-(** show type class instantiations             *)
-(** ****************************************** *)
-
-(* matching printing_functions.ml *)
-val stringFromReg_name : reg_name -> string
-let stringFromReg_name r = match r with
-| Reg s start size dir -> s
-| Reg_slice s start dir (first,second) ->
-    let (first,second) = 
-      match dir with
-      | D_increasing -> (first,second) 
-      | D_decreasing -> (start - first, start - second)
-      end in
-    s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-| Reg_field s size dir f (first, second) ->
-    s ^ "." ^ f
-| Reg_f_slice s start dir f (first1,second1) (first,second) ->
-    let (first,second) = 
-      match dir with
-      | D_increasing -> (first,second) 
-      | D_decreasing -> (start - first, start - second)
-      end in
-    s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-end
-
-instance (Show reg_name)
-  let show = stringFromReg_name
-end
-
-
-(* hex pp of integers, adapting the Lem string_extra.lem code *)
-val stringFromNaturalHexHelper : natural -> list char -> list char
-let rec stringFromNaturalHexHelper n acc =
-  if n = 0 then
-    acc
-  else
-    stringFromNaturalHexHelper (n / 16) (String_extra.chr (natFromNatural (let nd = n mod 16 in if nd <=9 then nd + 48 else nd - 10 + 97)) :: acc)
-
-val stringFromNaturalHex : natural -> string
-let (*~{ocaml;hol}*) stringFromNaturalHex n = 
-  if n = 0 then "0" else toString (stringFromNaturalHexHelper n [])
-
-val stringFromIntegerHex : integer -> string
-let (*~{ocaml}*) stringFromIntegerHex i = 
-  if i < 0 then 
-    "-" ^ stringFromNaturalHex (naturalFromInteger i)
-  else
-    stringFromNaturalHex (naturalFromInteger i)
-
-
-let stringFromAddress (Address bs i) = 
-  let i' = integer_of_byte_list bs in
-  if i=i' then
-(*TODO: ideally this should be made to match the src/pp.ml pp_address; the following very roughly matches what's used in the ppcmem UI, enough to make exceptions readable *)
-    if i < 65535 then 
-      show i 
-    else
-      stringFromIntegerHex i
-  else
-    "stringFromAddress bytes and integer mismatch"
-
-instance (Show address)
-  let show = stringFromAddress
-end
-
-let stringFromByte_lifted bl =
-  match byte_of_byte_lifted bl with
-  | Nothing -> "u?"  
-  | Just (Byte bits) -> 
-      let i = integer_of_bit_list bits in
-      show i
-  end
-
-instance (Show byte_lifted)
-  let show = stringFromByte_lifted
-end
-
-(* possible next instruction address options *)
-type nia = 
-  | NIA_successor
-  | NIA_concrete_address of address
-  | NIA_LR   (* "LR0:61 || 0b00" in Power pseudocode *)
-  | NIA_CTR  (* "CTR0:61 || 0b00" in Power pseudocode *)
-  | NIA_register of reg_name (* the address will be in a register,
-                                corresponds to AArch64 BLR, BR, RET
-                                instructions *)
-
-let niaCompare n1 n2 = match (n1,n2) with
-  | (NIA_successor,NIA_successor) -> EQ
-  | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
-  | (NIA_LR,NIA_LR) -> EQ
-  | (NIA_CTR,NIA_CTR) -> EQ
-  | (NIA_register r1,NIA_register r2) -> compare r1 r2
-
-  | (NIA_successor,_) -> LT
-  | (NIA_concrete_address _,_) -> LT
-  | (NIA_LR,_) -> LT
-  | (NIA_CTR,_) -> LT
-  | (_,_) -> GT
-  end
-
-instance (Ord nia)
-  let compare = niaCompare
-  let (<)  n1 n2 = (niaCompare n1 n2) = LT
-  let (<=) n1 n2 = (niaCompare n1 n2) <> GT
-  let (>)  n1 n2 = (niaCompare n1 n2) = GT
-  let (>=) n1 n2 = (niaCompare n1 n2) <> LT
-end
-
-let stringFromNia = function
-  | NIA_successor -> "NIA_successor"
-  | NIA_concrete_address a -> "NIA_concrete_address " ^ show a
-  | NIA_LR -> "NIA_LR"
-  | NIA_CTR -> "NIA_CTR"
-  | NIA_register r -> "NIA_register " ^ show r
-end
-
-instance (Show nia)
-  let show = stringFromNia
-end
-
-type dia =
-  | DIA_none
-  | DIA_concrete_address of address
-  | DIA_register of reg_name
-
-let diaCompare d1 d2 = match (d1, d2) with
-  | (DIA_none, DIA_none) -> EQ
-  | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2
-  | (DIA_register r1, DIA_register r2) -> compare r1 r2
-  | (DIA_none, _) -> LT
-  | (DIA_concrete_address _, _) -> LT
-  | (DIA_register _, _) -> LT
-end
-
-instance (Ord dia)
-  let compare = diaCompare
-  let (<)  n1 n2 = (diaCompare n1 n2) = LT
-  let (<=) n1 n2 = (diaCompare n1 n2) <> GT
-  let (>)  n1 n2 = (diaCompare n1 n2) = GT
-  let (>=) n1 n2 = (diaCompare n1 n2) <> LT
-end
-
-let stringFromDia = function
-  | DIA_none               ->  "DIA_none"
-  | DIA_concrete_address a ->  "DIA_concrete_address " ^ show a
-  | DIA_register r ->  "DIA_delayed_register " ^ show r
-end
-
-instance (Show dia)
-  let show = stringFromDia
-end
-
                       
 val instruction_analysis :
   context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
   -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)
+
+
+val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state string unit
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index a1c49796..d54b7155 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -1,5 +1,6 @@
 open Printf ;;
 open Interp_ast ;;
+open Sail_impl_base ;;
 open Interp_utilities ;;
 open Interp_interface ;;
 open Interp_inter_imp ;;
@@ -86,10 +87,10 @@ let bits_lifted_homogenous_of_bit_lifteds (bls:bit_lifted list) : bits_lifted_ho
   bits_lifted_homogenous_of_bit_lifteds' bls' acc0 
 
 (*let byte_it_lifted_to_string = function
-  | Bitl_zero -> "0"
-  | Bitl_one ->  "1"
-  | Bitl_undef -> "u"
-  | Bitl_unknown -> "?"
+  | BL0 -> "0"
+  | BL1 ->  "1"
+  | BLUndef -> "u"
+  | BLUnknown -> "?"
 *)
 
 let bit_lifted_to_string = function
@@ -103,7 +104,7 @@ let hex_int_to_string i =
 
 let bytes_lifted_homogenous_to_string = function
   | Bitslh_concrete bs -> 
-      let i = to_int (Interp_interface.integer_of_bit_list bs) in
+      let i = to_int (Sail_impl_base.integer_of_bit_list bs) in
       hex_int_to_string i
   | Bitslh_undef -> "uu"
   | Bitslh_unknown -> "??"
@@ -126,7 +127,7 @@ print as lifted hex, otherwise print as lifted bits *)
 let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (starto: int option) (abbreviate_zero_to_nine: bool) =  
   let l = List.length bls in
   if l mod 8 = 0 then  (*  if List.mem l [8;16;32;64;128] then *)
-    let bytesl = List.map (fun (Byte_lifted bs) -> bs) (Interp_interface.byte_lifteds_of_bit_lifteds bls) in
+    let bytesl = List.map (fun (Byte_lifted bs) -> bs) (Sail_impl_base.byte_lifteds_of_bit_lifteds bls) in
     let byteslhos = List.map bits_lifted_homogenous_of_bit_lifteds bytesl in
     match maybe_all byteslhos with 
     | None -> (* print as bitvector after all *)
@@ -134,7 +135,7 @@ let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (s
     | Some (byteslhs: bits_lifted_homogenous list) -> 
         (* if abbreviate_zero_to_nine, all bytes are concrete, and the number is <=9, just print that *)  
         (*   (note that that doesn't print the length or start - it's appropriate only for memory values, where we typically have an explicit footprint also printed *)
-        let nos = List.rev_map (function blh -> match blh with | Bitslh_concrete bs -> Some (Interp_interface.nat_of_bit_list bs) | Bitslh_undef -> None | Bitslh_unknown -> None) byteslhs in 
+        let nos = List.rev_map (function blh -> match blh with | Bitslh_concrete bs -> Some (Sail_impl_base.nat_of_bit_list bs) | Bitslh_undef -> None | Bitslh_unknown -> None) byteslhs in 
         let (lsb,msbs) = ((List.hd nos), List.tl nos) in
         match (abbreviate_zero_to_nine, List.for_all (fun no -> no=Some 0) msbs, lsb) with 
         | (true, true, Some n) when n <= 9 -> 
@@ -256,7 +257,7 @@ let dir_to_string = function
   | D_decreasing -> "dec"
 
 let reg_name_to_string = function
-  | Reg0(s,start,size,d) -> s (*^ "(" ^ (string_of_int start) ^ ", " ^ (string_of_int size) ^ ", " ^ (dir_to_string d) ^ ")"*)
+  | Reg(s,start,size,d) -> s (*^ "(" ^ (string_of_int start) ^ ", " ^ (string_of_int size) ^ ", " ^ (dir_to_string d) ^ ")"*)
   | Reg_slice(s,start,dir,(first,second)) -> 
     let first,second = 
       match dir with
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index c7747b50..2ce2c016 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -1,5 +1,6 @@
 open Interp_utilities;;
 open Interp_ast ;;
+open Sail_impl_base ;;
 open Interp_interface ;;
 
 (*Functions to translate values, registers, or locations strings *)
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index eec87f4f..b536a77d 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -1,5 +1,6 @@
 open Printf
 open Interp_ast
+open Sail_impl_base
 open Interp_interface
 open Interp_inter_imp
 
@@ -107,22 +108,22 @@ let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
 
 let rec perform_action ((reg, mem, tagmem) as env) = function
  (* registers *)
- | Read_reg0(Reg0(id,_,_,_), _) -> (Some(Reg.find id reg), env)
- | Read_reg0(Reg_slice(id, _, _, range), _)
- | Read_reg0(Reg_field(id, _, _, _, range), _) -> (Some(slice (Reg.find id reg) range), env)
- | Read_reg0(Reg_f_slice(id, _,_,_, range, mini_range), _) ->
+ | Read_reg1(Reg(id,_,_,_), _) -> (Some(Reg.find id reg), env)
+ | Read_reg1(Reg_slice(id, _, _, range), _)
+ | Read_reg1(Reg_field(id, _, _, _, range), _) -> (Some(slice (Reg.find id reg) range), env)
+ | Read_reg1(Reg_f_slice(id, _,_,_, range, mini_range), _) ->
    (Some(slice (slice (Reg.find id reg) range) mini_range),env)
- | Write_reg0(Reg0(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem,tagmem))
- | Write_reg0((Reg_slice(id,_,_,range) as reg_n),value, _) 
- | Write_reg0((Reg_field(id,_,_,_,range) as reg_n),value,_)->
+ | Write_reg1(Reg(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem,tagmem))
+ | Write_reg1((Reg_slice(id,_,_,range) as reg_n),value, _) 
+ | Write_reg1((Reg_field(id,_,_,_,range) as reg_n),value,_)->
      let old_val = Reg.find id reg in
      let new_val = fupdate_slice reg_n old_val value range in
      (None, (Reg.add id new_val reg, mem,tagmem))
- | Write_reg0((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) ->
+ | Write_reg1((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) ->
    let old_val = Reg.find id reg in
    let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in
    (None,(Reg.add id new_val reg,mem,tagmem))
- | Read_mem0(kind,location, length, _,_) ->
+ | Read_mem1(kind,location, length, _,_) ->
    let address = match address_of_address_lifted location with
      | Some a -> a
      | None -> assert false (*TODO remember how to report an error *)in
@@ -160,7 +161,7 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
          | b::bytes -> 
            writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in
      (None,(reg,writing naddress length bytes mem,tagmem)))
- | Write_memv0(Some location, bytes, _, _) ->
+ | Write_memv1(Some location, bytes, _, _) ->
    let address = match address_of_address_lifted location with
      | Some a -> a
      | _ -> failwith "Write address not known" in
@@ -261,20 +262,20 @@ let run
       (green act) lhs (blue arrow) rhs in
   let left = "<-" and right = "->" in
   let rec loop mode env = function
-    | Done ->
+    | Done0 ->
       interactf "%s: %s\n" (grey name) (blue "done");
       (true, mode, !track_dependencies, env)
-    | Error0 s -> 
+    | Error1 s -> 
       errorf "%s: %s: %s\n" (grey name) (red "error") s;
       (false, mode, !track_dependencies, env)
-    | Escape (None, _) ->
+    | Escape0 (None, _) ->
       show "exiting current instruction" "" "" "";
       interactf "%s: %s\n" (grey name) (blue "done");
       (true, mode, !track_dependencies, env)
-    | Fail0 (Some s) ->
+    | Fail1 (Some s) ->
       errorf "%s: %s: %s\n" (grey name) (red "assertion failed") s;
       (false, mode, !track_dependencies, env)
-    | Fail0 None ->
+    | Fail1 None ->
       errorf "%s: %s: %s\n" (grey name) (red "assertion failed") "No message provided";
       (false, mode, !track_dependencies, env)
     | action ->
@@ -290,17 +291,17 @@ let run
           mode in
       let (mode', env', next) =
         (match action with    
-        | Read_reg0(reg,next_thunk) ->
+        | Read_reg1(reg,next_thunk) ->
           (match return with
            | Some(value) -> 
              show "read_reg" (reg_name_to_string reg) right (register_value_to_string value);
              let next = next_thunk value in
              (step next, env', next)
            | None -> assert false)
-        | Write_reg0(reg,value,next) ->
+        | Write_reg1(reg,value,next) ->
           show "write_reg" (reg_name_to_string reg) left (register_value_to_string value);
           (step next, env', next)
-        | Read_mem0(kind, (Address_lifted(location,_)), length, tracking, next_thunk) ->
+        | Read_mem1(kind, (Address_lifted(location,_)), length, tracking, next_thunk) ->
           (match return with
            | Some(value) -> 
              show "read_mem"
@@ -327,26 +328,26 @@ let run
              show "write_mem value depended on" (dependencies_to_string vdeps) "" "";);
           let next = next_thunk true in
           (step next,env',next)
-        | Write_memv0(Some(Address_lifted(location,_)),value,_,next_thunk) ->
+        | Write_memv1(Some(Address_lifted(location,_)),value,_,next_thunk) ->
           show "write_mem value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value);
           let next = next_thunk true in
           (step next,env',next)
-        | Write_ea0(_,(Address_lifted(location,_)), size,_,next) ->
+        | Write_ea1(_,(Address_lifted(location,_)), size,_,next) ->
           show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes");
           (step next, env, next)
-        | Barrier0(bkind,next) ->
+        | Barrier1(bkind,next) ->
           show "mem_barrier" "" "" "";
           (step next, env, next)
-        | Internal(None,None, next) ->
+        | Internal0(None,None, next) ->
           show "stepped" "" "" "";
           (step ~force:true next,env',next)
-        | Internal((Some fn),None,next) ->
+        | Internal0((Some fn),None,next) ->
           show "evaluated" fn "" "";
           (step ~force:true next, env',next)
-        | Internal(None,Some vdisp,next) ->
+        | Internal0(None,Some vdisp,next) ->
           show "evaluated" (vdisp ()) "" "";
           (step ~force:true next,env', next)
-        | Internal((Some fn),(Some vdisp),next) ->
+        | Internal0((Some fn),(Some vdisp),next) ->
           show "evaluated" (fn ^ " " ^ (vdisp ())) "" "";
           (step ~force:true next, env', next)
         | Nondet_choice(nondets, next) ->
@@ -369,18 +370,18 @@ let run
               loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies !default_endian) next))
               choose_order (false,mode,!track_dependencies,env'); in
             (step i_state,env',i_state) end
-        | Escape(Some e,_) ->
+        | Escape0(Some e,_) ->
           show "exiting current evaluation" "" "" "";
           step e,env', e
-        | Escape _ -> assert false
-        | Error0 _ -> failwith "Internal error"
-        | Fail0 _ -> failwith "Assertion in program failed"
-        | Done ->
+        | Escape0 _ -> assert false
+        | Error1 _ -> failwith "Internal error"
+        | Fail1 _ -> failwith "Assertion in program failed"
+        | Done0 ->
           show "done evalution" "" "" "";
           assert false
-        | Footprint0 _ -> assert false
-        | Write_ea0 _ -> assert false
-        | Write_memv0 _ -> assert false)
+        | Footprint1 _ -> assert false
+        | Write_ea1 _ -> assert false
+        | Write_memv1 _ -> assert false)
         (*| _ -> assert false*)
       in
       loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies !default_endian) next) in
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
new file mode 100644
index 00000000..60c7bf0b
--- /dev/null
+++ b/src/lem_interp/sail_impl_base.lem
@@ -0,0 +1,1309 @@
+open import Pervasives_extra
+open import Interp_ast (* only because the instruction type refers to base effect *)
+            
+(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
+instance forall 'a. Ord 'a => (Ord (maybe 'a))
+  let compare = maybeCompare compare
+  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
+  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
+  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
+  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
+end
+
+type word8 = nat (* bounded at a byte, for when lem supports it*)
+
+type end_flag =
+  | E_big_endian
+  | E_little_endian
+
+type bit =
+  | Bitc_zero
+  | Bitc_one
+
+type bit_lifted = 
+  | Bitl_zero
+  | Bitl_one
+  | Bitl_undef
+  | Bitl_unknown
+
+type direction = 
+  | D_increasing
+  | D_decreasing
+
+(* at some point this should probably not mention bit_lifted anymore *)
+type register_value = <| 
+    rv_bits: list bit_lifted (* MSB first, smallest index number *); 
+    rv_dir: direction; 
+    rv_start: nat ;
+    rv_start_internal: nat; 
+    (*when dir is increasing, rv_start = rv_start_internal. 
+      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
+    |>
+
+type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*)
+
+type instruction_field_value = list bit
+
+type byte = Byte of list bit (* of length 8 *)  (*MSB first everywhere*) 
+
+type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer
+(* for both values of end_flag, MSBy first *)
+
+type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*)
+
+type memory_value = list memory_byte
+(* the list is of length >=1 *)
+(* for both big-endian (Power) and little-endian (ARM), the head of the
+     list is the byte stored at the lowest address *)
+(* for big-endian Power the head of the list is the most-significant
+   byte, in both the interpreter and machineDef* code. *)
+(* For little-endian ARM, the head of the list is the
+   least-significant byte in machineDef* code and the
+   most-significant byte in interpreter code, with the switch over
+   (a list-reverse) being done just inside the interpreter interface*)
+(* In other words, in the machineDef* code the lowest-address byte is first,
+   and in the interpreter code the most-significant byte is first *)
+
+
+
+(* not sure which of these is more handy yet *)
+type address = Address of list byte (* of length 8 *) * integer
+(* type address = Address of integer *)
+
+type opcode = Opcode of list byte (* of length 4 *)
+
+(** typeclass instantiations *)
+
+let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
+  match (b1,b2) with
+  | (Bitc_zero, Bitc_zero) -> EQ
+  | (Bitc_one, Bitc_one) -> EQ
+  | (Bitc_zero, _) -> LT
+  | (_,_) -> GT
+  end
+let inline {ocaml} bitCompare = defaultCompare
+
+let ~{ocaml} bitLess b1 b2      = bitCompare b1 b2 =  LT
+let ~{ocaml} bitLessEq b1 b2    = bitCompare b1 b2 <> GT
+let ~{ocaml} bitGreater b1 b2   = bitCompare b1 b2 =  GT
+let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
+
+let inline {ocaml} bitLess      = defaultLess
+let inline {ocaml} bitLessEq    = defaultLessEq
+let inline {ocaml} bitGreater   = defaultGreater
+let inline {ocaml} bitGreaterEq = defaultGreaterEq
+
+instance (Ord bit)
+  let compare = bitCompare
+  let (<)  = bitLess
+  let (<=) = bitLessEq
+  let (>)  = bitGreater
+  let (>=) = bitGreaterEq
+end
+
+let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
+  match (bl1,bl2) with
+  | (Bitl_zero, Bitl_zero) -> EQ
+  | (Bitl_one, Bitl_one) -> EQ
+  | (Bitl_undef,Bitl_undef) -> EQ
+  | (Bitl_unknown,Bitl_unknown) -> EQ
+  | (Bitl_zero,_) -> LT
+  | (Bitl_one, _) -> LT
+  | (Bitl_undef, _) -> LT
+  | (_,_) -> GT
+  end
+let inline {ocaml} bit_liftedCompare = defaultCompare
+
+let ~{ocaml} bit_liftedLess b1 b2      = bit_liftedCompare b1 b2 =  LT
+let ~{ocaml} bit_liftedLessEq b1 b2    = bit_liftedCompare b1 b2 <> GT
+let ~{ocaml} bit_liftedGreater b1 b2   = bit_liftedCompare b1 b2 =  GT
+let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} bit_liftedLess      = defaultLess
+let inline {ocaml} bit_liftedLessEq    = defaultLessEq
+let inline {ocaml} bit_liftedGreater   = defaultGreater
+let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
+
+instance (Ord bit_lifted)
+  let compare = bit_liftedCompare
+  let (<)  = bit_liftedLess
+  let (<=) = bit_liftedLessEq
+  let (>)  = bit_liftedGreater
+  let (>=) = bit_liftedGreaterEq
+end
+
+let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
+let inline {ocaml} byte_liftedCompare = defaultCompare
+
+let ~{ocaml} byte_liftedLess b1 b2      = byte_liftedCompare b1 b2 =  LT
+let ~{ocaml} byte_liftedLessEq b1 b2    = byte_liftedCompare b1 b2 <> GT
+let ~{ocaml} byte_liftedGreater b1 b2   = byte_liftedCompare b1 b2 =  GT
+let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} byte_liftedLess      = defaultLess
+let inline {ocaml} byte_liftedLessEq    = defaultLessEq
+let inline {ocaml} byte_liftedGreater   = defaultGreater
+let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq
+
+instance (Ord byte_lifted)
+  let compare = byte_liftedCompare
+  let (<)  = byte_liftedLess
+  let (<=) = byte_liftedLessEq
+  let (>)  = byte_liftedGreater
+  let (>=) = byte_liftedGreaterEq
+end
+
+let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2
+let inline {ocaml} byteCompare = defaultCompare
+
+let ~{ocaml} byteLess b1 b2      = byteCompare b1 b2 =  LT
+let ~{ocaml} byteLessEq b1 b2    = byteCompare b1 b2 <> GT
+let ~{ocaml} byteGreater b1 b2   = byteCompare b1 b2 =  GT
+let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT
+
+let inline {ocaml} byteLess      = defaultLess
+let inline {ocaml} byteLessEq    = defaultLessEq
+let inline {ocaml} byteGreater   = defaultGreater
+let inline {ocaml} byteGreaterEq = defaultGreaterEq
+
+instance (Ord byte)
+  let compare = byteCompare
+  let (<)  = byteLess
+  let (<=) = byteLessEq
+  let (>)  = byteGreater
+  let (>=) = byteGreaterEq
+end
+
+let (*~{ocaml}*) addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
+(*let inline {ocaml} addressCompare = defaultCompare*)
+
+let ~{ocaml} addressLess b1 b2      = addressCompare b1 b2 =  LT
+let ~{ocaml} addressLessEq b1 b2    = addressCompare b1 b2 <> GT
+let ~{ocaml} addressGreater b1 b2   = addressCompare b1 b2 =  GT
+let ~{ocaml} addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT
+
+let inline {ocaml} addressLess      = defaultLess
+let inline {ocaml} addressLessEq    = defaultLessEq
+let inline {ocaml} addressGreater   = defaultGreater
+let inline {ocaml} addressGreaterEq = defaultGreaterEq
+
+instance (Ord address)
+  let compare = addressCompare
+  let (<)  = addressLess
+  let (<=) = addressLessEq
+  let (>)  = addressGreater
+  let (>=) = addressGreaterEq
+end
+
+let {coq} addressEqual a1 a2 = (addressCompare a1 a2) = EQ
+let inline ~{coq} addressEqual = unsafe_structural_equality
+
+let {coq} addressInequal a1 a2 = not (addressEqual a1 a2)
+let inline ~{coq} addressInequal = unsafe_structural_inequality
+
+instance  (Eq address)
+  let (=)  = addressEqual
+  let (<>) = addressInequal
+end
+
+let ~{ocaml} directionCompare d1 d2 =
+  match (d1, d2) with
+  | (D_decreasing, D_increasing) -> GT
+  | (D_increasing, D_decreasing) -> LT
+  | _ -> EQ
+  end
+let inline {ocaml} directionCompare = defaultCompare
+
+let ~{ocaml} directionLess b1 b2      = directionCompare b1 b2 =  LT
+let ~{ocaml} directionLessEq b1 b2    = directionCompare b1 b2 <> GT
+let ~{ocaml} directionGreater b1 b2   = directionCompare b1 b2 =  GT
+let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT
+
+let inline {ocaml} directionLess      = defaultLess
+let inline {ocaml} directionLessEq    = defaultLessEq
+let inline {ocaml} directionGreater   = defaultGreater
+let inline {ocaml} directionGreaterEq = defaultGreaterEq
+
+instance (Ord direction)
+  let compare = directionCompare
+  let (<)  = directionLess
+  let (<=) = directionLessEq
+  let (>)  = directionGreater
+  let (>=) = directionGreaterEq
+end
+
+let ~{ocaml} register_valueCompare rv1 rv2 =
+  compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal)
+          (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal)
+let inline {ocaml} register_valueCompare = defaultCompare
+
+let ~{ocaml} register_valueLess b1 b2      = register_valueCompare b1 b2 =  LT
+let ~{ocaml} register_valueLessEq b1 b2    = register_valueCompare b1 b2 <> GT
+let ~{ocaml} register_valueGreater b1 b2   = register_valueCompare b1 b2 =  GT
+let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT
+
+let inline {ocaml} register_valueLess      = defaultLess
+let inline {ocaml} register_valueLessEq    = defaultLessEq
+let inline {ocaml} register_valueGreater   = defaultGreater
+let inline {ocaml} register_valueGreaterEq = defaultGreaterEq
+
+instance (Ord register_value)
+  let compare = register_valueCompare
+  let (<)  = register_valueLess
+  let (<=) = register_valueLessEq
+  let (>)  = register_valueGreater
+  let (>=) = register_valueGreaterEq
+end
+
+let ~{ocaml} address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) =
+  compare (b1,i1) (b2,i2)
+let inline {ocaml} address_liftedCompare = defaultCompare
+
+let ~{ocaml} address_liftedLess b1 b2      = address_liftedCompare b1 b2 =  LT
+let ~{ocaml} address_liftedLessEq b1 b2    = address_liftedCompare b1 b2 <> GT
+let ~{ocaml} address_liftedGreater b1 b2   = address_liftedCompare b1 b2 =  GT
+let ~{ocaml} address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} address_liftedLess      = defaultLess
+let inline {ocaml} address_liftedLessEq    = defaultLessEq
+let inline {ocaml} address_liftedGreater   = defaultGreater
+let inline {ocaml} address_liftedGreaterEq = defaultGreaterEq
+
+instance (Ord address_lifted)
+  let compare = address_liftedCompare
+  let (<)  = address_liftedLess
+  let (<=) = address_liftedLessEq
+  let (>)  = address_liftedGreater
+  let (>=) = address_liftedGreaterEq
+end
+
+(* Registers *)
+type slice = (nat * nat)
+
+type reg_name = 
+  (* do we really need this here if ppcmem already has this information by itself? *)
+| Reg of string * nat * nat * direction
+(*Name of the register, accessing the entire register, the start and size of this register, and its direction *)
+
+| Reg_slice of string * nat * direction * slice 
+(* Name of the register, accessing from the bit indexed by the first
+to the bit indexed by the second integer of the slice, inclusive. For
+machineDef* the first is a smaller number or equal to the second, adjusted
+to reflect the correct span direction in the interpreter side.  *)
+
+| Reg_field of string * nat * direction * string * slice 
+(*Name of the register, start and direction, and name of the field of the register
+accessed. The slice specifies where this field is in the register*)
+
+| Reg_f_slice of string * nat * direction * string * slice * slice 
+(* The first four components are as in Reg_field; the final slice
+specifies a part of the field, indexed w.r.t. the register as a whole *)
+
+let register_base_name : reg_name -> string = function
+  | Reg s _ _ _             -> s
+  | Reg_slice s _ _ _       -> s
+  | Reg_field s _ _ _ _     -> s
+  | Reg_f_slice s _ _ _ _ _ -> s
+  end
+
+let slice_of_reg_name : reg_name -> slice = function
+  | Reg _ start width D_increasing -> (start, start + width -1)
+  | Reg _ start width D_decreasing -> (start - width - 1, start)
+  | Reg_slice _ _ _ sl             -> sl
+  | Reg_field _ _ _ _ sl           -> sl
+  | Reg_f_slice _ _ _ _ _ sl       -> sl
+  end
+
+let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = 
+  register_base_name r = register_base_name r' &&
+  let (i1,  i2)  = slice_of_reg_name r in
+  let (i1', i2') = slice_of_reg_name r' in
+  i1' <= i2 && i2' >= i1
+
+let reg_nameCompare r1 r2 = 
+  compare (register_base_name r1,slice_of_reg_name r1)
+          (register_base_name r2,slice_of_reg_name r2)
+
+let reg_nameLess b1 b2      = reg_nameCompare b1 b2 =  LT
+let reg_nameLessEq b1 b2    = reg_nameCompare b1 b2 <> GT
+let reg_nameGreater b1 b2   = reg_nameCompare b1 b2 =  GT
+let reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT
+
+instance (Ord reg_name)
+  let compare = reg_nameCompare
+  let (<)  = reg_nameLess
+  let (<=) = reg_nameLessEq
+  let (>)  = reg_nameGreater
+  let (>=) = reg_nameGreaterEq
+end
+
+let reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ
+let reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2)
+
+instance  (Eq reg_name)
+  let (=)  = reg_nameEqual
+  let (<>) = reg_nameInequal
+end
+
+instance (SetType reg_name)
+  let setElemCompare = reg_nameCompare
+end
+
+let direction_of_reg_name r = match r with
+  | Reg _ _ _ d -> d
+  | Reg_slice _ _ d _ -> d
+  | Reg_field _ _ d _ _ -> d
+  | Reg_f_slice _ _ d _ _ _ -> d
+ end
+
+let start_of_reg_name r = match r with
+  | Reg _ start _ _ -> start
+  | Reg_slice _ start _ _ -> start
+  | Reg_field _ start _ _ _ -> start
+  | Reg_f_slice _ start _ _ _ _ -> start
+end
+
+(* Data structures for building up instructions *)
+
+type read_kind =
+  (* common reads *)
+  Read_plain
+  | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
+  (* Power reads *)
+  | Read_reserve
+  (* AArch64 reads *)
+  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+
+instance (Show read_kind)
+  let show = function
+    | Read_plain -> "Read_plain"
+    | Read_tag -> "Read_tag"
+    | Read_reserve -> "Read_reserve"
+    | Read_acquire -> "Read_acquire"
+    | Read_exclusive -> "Read_exclusive"
+    | Read_exclusive_acquire -> "Read_exclusive_acquire"
+    | Read_stream -> "Read_stream"
+  end
+end
+
+type write_kind =
+  (* common writes *)
+    Write_plain
+  | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
+  (* Power writes *)
+  | Write_conditional
+  (* AArch64 writes *)
+  | Write_release | Write_exclusive | Write_exclusive_release
+
+type barrier_kind =
+  (* Power barriers *)
+  Sync | LwSync | Eieio | Isync
+  (* AArch64 barriers *)
+  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
+
+type instruction_kind = 
+  | IK_barrier of barrier_kind 
+  | IK_mem_read of read_kind 
+  | IK_mem_write of write_kind
+(* SS reinstating cond_branches
+at present branches are not distinguished in the instruction_kind;
+they just have particular nias (and will be IK_simple *)
+  | IK_cond_branch 
+(*  | IK_uncond_branch *)
+  | IK_simple
+
+(* the address_lifted types should go away here and be replaced by address *)
+type outcome 's 'e 'a =
+  (* Request to read memory, value is location to read, integer is size to read,
+     followed by registers that were used in computing that size *)
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'e 'a)
+  (* Tell the system a write is imminent, at address lifted, of size nat *)
+  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'e 'a
+  (* Request to write memory at last signalled address. Memory value should be 8
+     times the size given in ea signal *)
+  | Write_memv of memory_value * (bool -> outcome_s 's 'e 'a)
+  (* Request a memory barrier *)
+  | Barrier of barrier_kind * outcome_s 's 'e 'a
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of outcome_s 's 'e 'a
+  (* Request to read register, will track dependency when mode.track_values *)
+  | Read_reg of reg_name * (register_value -> outcome_s 's 'e 'a) 
+  (* Request to write register *)
+  | Write_reg of (reg_name * register_value) * (outcome_s 's 'e 'a)
+  | Escape of maybe (outcome_s 's 'e 'e)
+  (*Result of a failed assert with possible error message to report*)
+  | Fail of maybe string
+  | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'e 'a
+  | Done of 'a
+  | Error of string
+   and outcome_s 's 'e 'a = outcome 's 'e 'a * maybe 's
+
+let ~{ocaml} read_kindCompare rk1 rk2 =
+  match (rk1, rk2) with
+  | (Read_plain, Read_plain)             -> EQ
+  | (Read_plain, Read_reserve)           -> LT
+  | (Read_plain, Read_acquire)           -> LT
+  | (Read_plain, Read_exclusive)         -> LT
+  | (Read_plain, Read_exclusive_acquire) -> LT
+  | (Read_plain, Read_stream)            -> LT
+
+  | (Read_reserve, Read_plain)             -> GT
+  | (Read_reserve, Read_reserve)           -> EQ
+  | (Read_reserve, Read_acquire)           -> LT
+  | (Read_reserve, Read_exclusive)         -> LT
+  | (Read_reserve, Read_exclusive_acquire) -> LT
+  | (Read_reserve, Read_stream)            -> LT
+
+  | (Read_acquire, Read_plain)             -> GT
+  | (Read_acquire, Read_reserve)           -> GT
+  | (Read_acquire, Read_acquire)           -> EQ
+  | (Read_acquire, Read_exclusive)         -> LT
+  | (Read_acquire, Read_exclusive_acquire) -> LT
+  | (Read_acquire, Read_stream)            -> LT
+
+  | (Read_exclusive, Read_plain)             -> GT
+  | (Read_exclusive, Read_reserve)           -> GT
+  | (Read_exclusive, Read_acquire)           -> GT
+  | (Read_exclusive, Read_exclusive)         -> EQ
+  | (Read_exclusive, Read_exclusive_acquire) -> LT
+  | (Read_exclusive, Read_stream)            -> LT
+
+  | (Read_exclusive_acquire, Read_plain)             -> GT
+  | (Read_exclusive_acquire, Read_reserve)           -> GT
+  | (Read_exclusive_acquire, Read_acquire)           -> GT
+  | (Read_exclusive_acquire, Read_exclusive)         -> GT
+  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
+  | (Read_exclusive_acquire, Read_stream)            -> GT
+
+  | (Read_stream, Read_plain)             -> GT
+  | (Read_stream, Read_reserve)           -> GT
+  | (Read_stream, Read_acquire)           -> GT
+  | (Read_stream, Read_exclusive)         -> GT
+  | (Read_stream, Read_exclusive_acquire) -> GT
+  | (Read_stream, Read_stream)            -> EQ
+  end
+let inline {ocaml} read_kindCompare = defaultCompare
+
+let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
+let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
+let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
+let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
+
+let inline {ocaml} read_kindLess      = defaultLess
+let inline {ocaml} read_kindLessEq    = defaultLessEq
+let inline {ocaml} read_kindGreater   = defaultGreater
+let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
+
+instance (Ord read_kind)
+  let compare = read_kindCompare
+  let (<)  = read_kindLess
+  let (<=) = read_kindLessEq
+  let (>)  = read_kindGreater
+  let (>=) = read_kindGreaterEq
+end
+
+let ~{ocaml} write_kindCompare wk1 wk2 =
+  match (wk1, wk2) with
+  | (Write_plain, Write_plain)             -> EQ
+  | (Write_plain, Write_conditional)       -> LT
+  | (Write_plain, Write_release)           -> LT
+  | (Write_plain, Write_exclusive)         -> LT
+  | (Write_plain, Write_exclusive_release) -> LT
+
+  | (Write_conditional, Write_plain)             -> GT
+  | (Write_conditional, Write_conditional)       -> EQ
+  | (Write_conditional, Write_release)           -> LT
+  | (Write_conditional, Write_exclusive)         -> LT
+  | (Write_conditional, Write_exclusive_release) -> LT
+
+  | (Write_release, Write_plain)             -> GT
+  | (Write_release, Write_conditional)       -> GT
+  | (Write_release, Write_release)           -> EQ
+  | (Write_release, Write_exclusive)         -> LT
+  | (Write_release, Write_exclusive_release) -> LT
+
+  | (Write_exclusive, Write_plain)             -> GT
+  | (Write_exclusive, Write_conditional)       -> GT
+  | (Write_exclusive, Write_release)           -> GT
+  | (Write_exclusive, Write_exclusive)         -> EQ
+  | (Write_exclusive, Write_exclusive_release) -> LT
+
+  | (Write_exclusive_release, Write_plain)             -> GT
+  | (Write_exclusive_release, Write_conditional)       -> GT
+  | (Write_exclusive_release, Write_release)           -> GT
+  | (Write_exclusive_release, Write_exclusive)         -> GT
+  | (Write_exclusive_release, Write_exclusive_release) -> EQ
+  end
+let inline {ocaml} write_kindCompare = defaultCompare
+
+let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
+let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
+let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
+let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
+
+let inline {ocaml} write_kindLess      = defaultLess
+let inline {ocaml} write_kindLessEq    = defaultLessEq
+let inline {ocaml} write_kindGreater   = defaultGreater
+let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
+
+instance (Ord write_kind)
+  let compare = write_kindCompare
+  let (<)  = write_kindLess
+  let (<=) = write_kindLessEq
+  let (>)  = write_kindGreater
+  let (>=) = write_kindGreaterEq
+end
+
+let ~{ocaml} barrier_kindCompare bk1 bk2 =
+  match (bk1, bk2) with
+  | (Sync, Sync)   -> EQ
+  | (Sync, LwSync) -> LT
+  | (Sync, Eieio)  -> LT
+  | (Sync, Isync)  -> LT
+  | (Sync, DMB)    -> LT
+  | (Sync, DMB_ST) -> LT
+  | (Sync, DMB_LD) -> LT
+  | (Sync, DSB)    -> LT
+  | (Sync, DSB_ST) -> LT
+  | (Sync, DSB_LD) -> LT
+  | (Sync, ISB)    -> LT
+
+  | (LwSync, Sync)   -> GT
+  | (LwSync, LwSync) -> EQ
+  | (LwSync, Eieio)  -> LT
+  | (LwSync, Isync)  -> LT
+  | (LwSync, DMB)    -> LT
+  | (LwSync, DMB_ST) -> LT
+  | (LwSync, DMB_LD) -> LT
+  | (LwSync, DSB)    -> LT
+  | (LwSync, DSB_ST) -> LT
+  | (LwSync, DSB_LD) -> LT
+  | (LwSync, ISB)    -> LT
+
+  | (Eieio, Sync)   -> GT
+  | (Eieio, LwSync) -> GT
+  | (Eieio, Eieio)  -> EQ
+  | (Eieio, Isync)  -> LT
+  | (Eieio, DMB)    -> LT
+  | (Eieio, DMB_ST) -> LT
+  | (Eieio, DMB_LD) -> LT
+  | (Eieio, DSB)    -> LT
+  | (Eieio, DSB_ST) -> LT
+  | (Eieio, DSB_LD) -> LT
+  | (Eieio, ISB)    -> LT
+
+  | (Isync, Sync)   -> GT
+  | (Isync, LwSync) -> GT
+  | (Isync, Eieio)  -> GT
+  | (Isync, Isync)  -> EQ
+  | (Isync, DMB)    -> LT
+  | (Isync, DMB_ST) -> LT
+  | (Isync, DMB_LD) -> LT
+  | (Isync, DSB)    -> LT
+  | (Isync, DSB_ST) -> LT
+  | (Isync, DSB_LD) -> LT
+  | (Isync, ISB)    -> LT
+
+  | (DMB, Sync)   -> GT
+  | (DMB, LwSync) -> GT
+  | (DMB, Eieio)  -> GT
+  | (DMB, ISync)  -> GT
+  | (DMB, DMB)    -> EQ
+  | (DMB, DMB_ST) -> LT
+  | (DMB, DMB_LD) -> LT
+  | (DMB, DSB)    -> LT
+  | (DMB, DSB_ST) -> LT
+  | (DMB, DSB_LD) -> LT
+  | (DMB, ISB)    -> LT
+
+  | (DMB_ST, Sync)   -> GT
+  | (DMB_ST, LwSync) -> GT
+  | (DMB_ST, Eieio)  -> GT
+  | (DMB_ST, ISync)  -> GT
+  | (DMB_ST, DMB)    -> GT
+  | (DMB_ST, DMB_ST) -> EQ
+  | (DMB_ST, DMB_LD) -> LT
+  | (DMB_ST, DSB)    -> LT
+  | (DMB_ST, DSB_ST) -> LT
+  | (DMB_ST, DSB_LD) -> LT
+  | (DMB_ST, ISB)    -> LT
+
+  | (DMB_LD, Sync)   -> GT
+  | (DMB_LD, LwSync) -> GT
+  | (DMB_LD, Eieio)  -> GT
+  | (DMB_LD, ISync)  -> GT
+  | (DMB_LD, DMB)    -> GT
+  | (DMB_LD, DMB_ST) -> GT
+  | (DMB_LD, DMB_LD) -> EQ
+  | (DMB_LD, DSB)    -> LT
+  | (DMB_LD, DSB_ST) -> LT
+  | (DMB_LD, DSB_LD) -> LT
+  | (DMB_LD, ISB)    -> LT
+
+  | (DSB, Sync)   -> GT
+  | (DSB, LwSync) -> GT
+  | (DSB, Eieio)  -> GT
+  | (DSB, ISync)  -> GT
+  | (DSB, DMB)    -> GT
+  | (DSB, DMB_ST) -> GT
+  | (DSB, DMB_LD) -> GT
+  | (DSB, DSB)    -> EQ
+  | (DSB, DSB_ST) -> LT
+  | (DSB, DSB_LD) -> LT
+  | (DSB, ISB)    -> LT
+
+  | (DSB_ST, Sync)   -> GT
+  | (DSB_ST, LwSync) -> GT
+  | (DSB_ST, Eieio)  -> GT
+  | (DSB_ST, ISync)  -> GT
+  | (DSB_ST, DMB)    -> GT
+  | (DSB_ST, DMB_ST) -> GT
+  | (DSB_ST, DMB_LD) -> GT
+  | (DSB_ST, DSB)    -> GT
+  | (DSB_ST, DSB_ST) -> EQ
+  | (DSB_ST, DSB_LD) -> LT
+  | (DSB_ST, ISB)    -> LT
+
+  | (DSB_LD, Sync)   -> GT
+  | (DSB_LD, LwSync) -> GT
+  | (DSB_LD, Eieio)  -> GT
+  | (DSB_LD, ISync)  -> GT
+  | (DSB_LD, DMB)    -> GT
+  | (DSB_LD, DMB_ST) -> GT
+  | (DSB_LD, DMB_LD) -> GT
+  | (DSB_LD, DSB)    -> GT
+  | (DSB_LD, DSB_ST) -> GT
+  | (DSB_LD, DSB_LD) -> EQ
+  | (DSB_LD, ISB)    -> LT
+                          
+  | (ISB, Sync)   -> GT
+  | (ISB, LwSync) -> GT
+  | (ISB, Eieio)  -> GT
+  | (ISB, ISync)  -> GT
+  | (ISB, DMB)    -> GT
+  | (ISB, DMB_ST) -> GT
+  | (ISB, DMB_LD) -> GT
+  | (ISB, DSB)    -> GT
+  | (ISB, DSB_ST) -> GT
+  | (ISB, DSB_LD) -> GT
+  | (ISB, ISB)    -> EQ
+  end
+let inline {ocaml} barrier_kindCompare = defaultCompare
+
+let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
+let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
+let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
+let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
+
+let inline {ocaml} barrier_kindLess      = defaultLess
+let inline {ocaml} barrier_kindLessEq    = defaultLessEq
+let inline {ocaml} barrier_kindGreater   = defaultGreater
+let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
+
+instance (Ord barrier_kind)
+  let compare = barrier_kindCompare
+  let (<)  = barrier_kindLess
+  let (<=) = barrier_kindLessEq
+  let (>)  = barrier_kindGreater
+  let (>=) = barrier_kindGreaterEq
+end
+
+
+
+
+(*Type representint the constructor parameters in instruction, other is a type not representable externally*)
+type instr_parm_typ = 
+  | Bit (*A single bit, represented as a one element Bitvector as a value*)
+  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
+  | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *)
+  | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
+  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
+
+let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
+  | (Bit,Bit) -> true
+  | (Bvector i1,Bvector i2) -> i1 = i2
+  | (Range i1,Range i2) -> i1 = i2
+  | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
+  | (Other,Other) -> true
+  | _ -> false
+end
+let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality
+
+let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
+let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality
+
+instance (Eq instr_parm_typ) 
+  let (=) = instr_parm_typEqual
+  let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
+end 
+
+let instr_parm_typShow ip = match ip with
+  | Bit -> "Bit"
+  | Bvector i -> "Bvector " ^ show i
+  | Range i -> "Range " ^ show i
+  | Enum s i -> "Enum " ^ s ^ " " ^ show i
+  | Other -> "Other"
+ end
+
+instance (Show instr_parm_typ)
+let show = instr_parm_typShow
+end
+
+(*A representation of the AST node for each instruction in the spec, with concrete values from this call,
+  and the potential static effects from the funcl clause for this instruction 
+  Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
+*)
+type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
+
+let {coq} instructionEqual i1 i2 = match (i1,i2) with
+  | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
+end
+let inline ~{coq} instructionEqual = unsafe_structural_equality
+
+let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2)
+let inline ~{coq} instructionInequal = unsafe_structural_inequality
+
+type decode_error = 
+  | Unsupported_instruction_error of instruction
+  | Not_an_instruction_error of opcode
+  | Internal_error of string
+
+type instruction_or_decode_error =
+  | IDE_instr of instruction
+  | IDE_decode_error of decode_error
+
+
+(** operations and coercions on basic values *)
+
+val word8_to_bitls : word8 -> list bit_lifted
+val bitls_to_word8 : list bit_lifted -> word8
+
+val integer_of_word8_list : list word8 -> integer
+val word8_list_of_integer : integer -> integer -> list word8 
+
+val concretizable_bitl : bit_lifted -> bool
+val concretizable_bytl : byte_lifted -> bool
+val concretizable_bytls : list byte_lifted -> bool
+
+let concretizable_bitl = function
+  | Bitl_zero -> true
+  | Bitl_one -> true
+  | Bitl_undef -> false
+  | Bitl_unknown -> false
+end 
+
+let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs
+let concretizable_bytls = List.all concretizable_bytl
+
+(* constructing values *)
+
+val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value
+let build_register_value bs dir width start_index =
+  <| rv_bits = bs;
+     rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
+     rv_start_internal = start_index; 
+     rv_start = if dir = D_increasing 
+       then start_index 
+       else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *)
+  |>
+
+val register_value : bit_lifted -> direction -> nat -> nat -> register_value
+let register_value b dir width start_index = 
+  build_register_value (List.replicate width b) dir width start_index
+
+val register_value_zeros : direction -> nat -> nat -> register_value
+let register_value_zeros dir width start_index = 
+  register_value Bitl_zero dir width start_index
+
+val register_value_ones : direction -> nat -> nat -> register_value
+let register_value_ones dir width start_index = 
+  register_value Bitl_one dir width start_index
+
+val byte_lifted_undef : byte_lifted
+let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef)
+
+val byte_lifted_unknown : byte_lifted
+let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown)
+  
+val memory_value_unknown : nat (*the number of bytes*) -> memory_value
+let memory_value_unknown (width:nat) : memory_value = 
+  List.replicate width byte_lifted_unknown 
+
+val memory_value_undef : nat (*the number of bytes*) -> memory_value
+let memory_value_undef (width:nat) : memory_value = 
+  List.replicate width byte_lifted_undef 
+
+(* lengths *)  
+
+val memory_value_length : memory_value -> nat
+let memory_value_length (mv:memory_value) = List.length mv
+
+
+(* aux fns *)
+
+val maybe_all : forall 'a.  list (maybe 'a) -> maybe (list 'a)
+let rec maybe_all' xs acc = 
+  match xs with
+  | [] -> Just (List.reverse acc)
+  | Nothing :: _ -> Nothing
+  | (Just y)::xs' -> maybe_all' xs' (y::acc)
+  end
+let maybe_all xs = maybe_all' xs [] 
+
+(** coercions *)
+
+(* bits and bytes *)
+
+let bit_to_bool = function (* TODO: rename bool_of_bit *)
+  | Bitc_zero -> false
+  | Bitc_one -> true
+end
+
+
+val bit_lifted_of_bit : bit -> bit_lifted
+let bit_lifted_of_bit b = 
+  match b with
+  | Bitc_zero -> Bitl_zero
+  | Bitc_one -> Bitl_one
+  end
+
+val bit_of_bit_lifted : bit_lifted -> maybe bit
+let bit_of_bit_lifted bl =
+  match bl with
+  | Bitl_zero -> Just Bitc_zero
+  | Bitl_one -> Just Bitc_one
+  | Bitl_undef -> Nothing
+  | Bitl_unknown -> Nothing
+  end
+
+
+val byte_lifted_of_byte : byte -> byte_lifted
+let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs)
+
+val byte_of_byte_lifted : byte_lifted -> maybe byte
+let byte_of_byte_lifted bl = 
+  match bl with
+  | Byte_lifted bls -> 
+      match maybe_all (List.map bit_of_bit_lifted bls) with
+      | Nothing -> Nothing
+      | Just bs -> Just (Byte bs)
+      end
+  end
+
+
+val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*)
+let rec bytes_of_bits bits = match bits with
+  | [] -> []
+  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
+    (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits)
+  | _ -> failwith "bytes_of_bits not given bits divisible by 8"
+end
+
+val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*)
+let rec byte_lifteds_of_bit_lifteds bits = match bits with
+  | [] -> []
+  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
+    (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits)
+  | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8"
+end
+
+
+val byte_of_memory_byte : memory_byte -> maybe byte
+let byte_of_memory_byte = byte_of_byte_lifted
+
+val memory_byte_of_byte : byte -> memory_byte
+let memory_byte_of_byte = byte_lifted_of_byte
+
+
+(* to and from nat *)
+
+(* this natFromBoolList could move to the Lem word.lem library *)
+val natFromBoolList : list bool -> nat
+let rec natFromBoolListAux (acc : nat) (bl : list bool) = 
+  match bl with 
+    | [] -> acc
+    | (true :: bl') -> natFromBoolListAux ((acc * 2) + 1) bl'
+    | (false :: bl') -> natFromBoolListAux (acc * 2) bl'
+  end
+let natFromBoolList bl = 
+  natFromBoolListAux 0 (List.reverse bl)
+
+
+val nat_of_bit_list : list bit -> nat 
+let nat_of_bit_list b =
+  natFromBoolList (List.reverse (List.map bit_to_bool b))
+  (* natFromBoolList takes a list with LSB first, for consistency with rest of Lem word library, so we reverse it. twice. *)
+
+
+(* to and from integer *)
+
+val integer_of_bit_list : list bit -> integer 
+let integer_of_bit_list b =
+  integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
+  (* integerFromBoolList takes a list with LSB first, so we reverse it *)
+
+val bit_list_of_integer : nat -> integer -> list bit 
+let bit_list_of_integer len b = 
+  List.map (fun b -> if b then Bitc_one else Bitc_zero) 
+    (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b)))
+
+val integer_of_byte_list : list byte -> integer 
+let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
+
+val byte_list_of_integer : nat -> integer -> list byte 
+let byte_list_of_integer (len:nat) (a:integer):list byte = 
+  let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
+
+
+val integer_of_address : address -> integer 
+let integer_of_address (a:address):integer = 
+  match a with
+  | Address bs i -> i 
+  end
+
+val address_of_integer : integer -> address 
+let address_of_integer (i:integer):address =
+  Address (byte_list_of_integer 8 i) i
+
+(* to and from signed-integer *)
+
+val signed_integer_of_bit_list : list bit -> integer
+let signed_integer_of_bit_list b =
+  match b with
+  | [] -> failwith "empty bit list"
+  | Bitc_zero :: b' ->
+      integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
+  | Bitc_one :: b' ->
+      let b'_val = integerFromBoolList (false,(List.reverse (List.map bit_to_bool b'))) in
+      (* integerFromBoolList takes a list with LSB first, so we reverse it *)
+      let msb_val = integerPow 2 ((List.length b) - 1) in
+      b'_val - msb_val
+  end
+
+
+(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *)
+val integer_address_of_int_list : list int -> integer
+let rec integerFromIntListAux (acc: integer) (is: list int) = 
+  match is with 
+  | [] -> acc
+  | (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is'
+  end
+let integer_address_of_int_list (is: list int) =
+  integerFromIntListAux 0 is
+
+val address_of_byte_list : list byte -> address 
+let address_of_byte_list bs = 
+  if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else 
+  Address bs (integer_of_byte_list bs)
+
+(* operations on addresses *)
+
+val add_address_nat : address -> nat -> address 
+let add_address_nat (a:address) (i:nat) : address = 
+  address_of_integer ((integer_of_address a) + (integerFromNat i))
+
+val clear_low_order_bits_of_address : address -> address 
+let clear_low_order_bits_of_address a = 
+  match a with 
+  | Address [b0;b1;b2;b3;b4;b5;b6;b7] i -> 
+      match b7 with
+      | Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] -> 
+          let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in
+	  let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in
+          Address bytes (integer_of_byte_list bytes)
+      | _ -> failwith "Byte does not contain 8 bits"
+      end
+  | _ -> failwith "Address does not contain 8 bytes"
+  end
+
+
+
+val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
+let byte_list_of_memory_value endian mv = 
+  let mv = if endian = E_big_endian then mv else List.reverse mv in
+  maybe_all (List.map byte_of_memory_byte mv)
+    
+
+val integer_of_memory_value : end_flag -> memory_value -> maybe integer 
+let integer_of_memory_value endian (mv:memory_value):maybe integer = 
+  match byte_list_of_memory_value endian mv with
+  | Just bs -> Just (integer_of_byte_list bs)
+  | Nothing -> Nothing 
+  end
+
+val memory_value_of_integer : end_flag  -> nat -> integer -> memory_value 
+let memory_value_of_integer endian (len:nat) (i:integer):memory_value =
+  let mv = List.map (byte_lifted_of_byte) (byte_list_of_integer len i) in
+  if endian = E_big_endian then mv else List.reverse mv
+
+
+val integer_of_register_value : register_value -> maybe integer 
+let integer_of_register_value (rv:register_value):maybe integer = 
+  match maybe_all (List.map bit_of_bit_lifted rv.rv_bits) with
+  | Nothing -> Nothing
+  | Just bs -> Just (integer_of_bit_list bs)
+  end 
+  
+val register_value_of_integer : nat -> nat -> direction -> integer -> register_value 
+let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value =
+  let bs = bit_list_of_integer len i in
+  build_register_value (List.map bit_lifted_of_bit bs) dir len start
+
+(* *)
+
+val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
+let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3]
+
+val register_value_of_address : address -> direction -> register_value   
+let register_value_of_address (Address bytes _) dir : register_value = 
+  let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in
+   <| rv_bits = bits;
+      rv_dir = dir;
+      rv_start = 0; 
+      rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1
+   |>
+
+val register_value_of_memory_value : memory_value -> direction -> register_value
+let register_value_of_memory_value bytes dir : register_value =
+  let bitls = List.concatMap (fun (Byte_lifted bs) -> bs) bytes in
+  <| rv_bits = bitls;
+     rv_dir = dir;
+     rv_start = 0;
+     rv_start_internal = if dir = D_increasing then 0 else (List.length bitls) - 1
+   |>                                                     
+
+val memory_value_of_register_value: register_value -> memory_value
+let memory_value_of_register_value r =
+  (byte_lifteds_of_bit_lifteds r.rv_bits)
+   
+val address_lifted_of_register_value : register_value -> maybe address_lifted
+(* returning Nothing iff the register value is not 64 bits wide, but
+allowing Bitl_undef and Bitl_unknown *)
+let address_lifted_of_register_value (rv:register_value) : maybe address_lifted = 
+  if List.length rv.rv_bits <> 64 then Nothing
+  else 
+    Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits)
+                         (if List.all concretizable_bitl rv.rv_bits 
+			  then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with
+                              | (Just(bits)) -> Just (integer_of_bit_list bits)
+                              | Nothing -> Nothing end
+			  else Nothing))
+
+val address_of_address_lifted : address_lifted -> maybe address
+(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *)
+let address_of_address_lifted (al:address_lifted): maybe address =
+  match al with
+  | Address_lifted bls (Just i)-> 
+      match maybe_all ((List.map byte_of_byte_lifted) bls) with
+      | Nothing -> Nothing
+      | Just bs -> Just (Address bs i)
+      end
+  | _ -> Nothing
+end
+
+val address_of_register_value : register_value -> maybe address
+(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *)
+let address_of_register_value (rv:register_value) : maybe address = 
+  match address_lifted_of_register_value rv with
+  | Nothing -> Nothing
+  | Just al -> 
+      match address_of_address_lifted al with
+      | Nothing -> Nothing
+      | Just a -> Just a
+      end
+  end
+
+let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address = 
+  match byte_list_of_memory_value endian mv with
+  | Nothing -> Nothing
+  | Just bs -> 
+      if List.length bs <> 8 then Nothing else
+      Just (address_of_byte_list bs)
+  end 
+
+val byte_of_int : int -> byte
+let byte_of_int (i:int) : byte = 
+  Byte (bit_list_of_integer 8 (integerFromInt i))
+
+val memory_byte_of_int : int -> memory_byte
+let memory_byte_of_int (i:int) : memory_byte = 
+  memory_byte_of_byte (byte_of_int i)
+
+(*
+val int_of_memory_byte : int -> maybe memory_byte
+let int_of_memory_byte (mb:memory_byte) : int = 
+  failwith "TODO"
+*)
+
+
+
+val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value
+let memory_value_of_address_lifted endian (Address_lifted bs _ :address_lifted) =
+  if endian = E_big_endian then bs else List.reverse bs
+
+val byte_list_of_address : address -> list byte
+let byte_list_of_address (Address bs _) : list byte = bs
+
+val memory_value_of_address : end_flag -> address -> memory_value
+let memory_value_of_address endian (Address bs _) =
+  List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs)
+
+val byte_list_of_opcode : opcode -> list byte
+let byte_list_of_opcode (Opcode bs) : list byte = bs
+
+(** ****************************************** *)
+(** show type class instantiations             *)
+(** ****************************************** *)
+
+(* matching printing_functions.ml *)
+val stringFromReg_name : reg_name -> string
+let stringFromReg_name r = match r with
+| Reg s start size dir -> s
+| Reg_slice s start dir (first,second) ->
+    let (first,second) = 
+      match dir with
+      | D_increasing -> (first,second) 
+      | D_decreasing -> (start - first, start - second)
+      end in
+    s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
+| Reg_field s size dir f (first, second) ->
+    s ^ "." ^ f
+| Reg_f_slice s start dir f (first1,second1) (first,second) ->
+    let (first,second) = 
+      match dir with
+      | D_increasing -> (first,second) 
+      | D_decreasing -> (start - first, start - second)
+      end in
+    s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
+end
+
+instance (Show reg_name)
+  let show = stringFromReg_name
+end
+
+
+(* hex pp of integers, adapting the Lem string_extra.lem code *)
+val stringFromNaturalHexHelper : natural -> list char -> list char
+let rec stringFromNaturalHexHelper n acc =
+  if n = 0 then
+    acc
+  else
+    stringFromNaturalHexHelper (n / 16) (String_extra.chr (natFromNatural (let nd = n mod 16 in if nd <=9 then nd + 48 else nd - 10 + 97)) :: acc)
+
+val stringFromNaturalHex : natural -> string
+let (*~{ocaml;hol}*) stringFromNaturalHex n = 
+  if n = 0 then "0" else toString (stringFromNaturalHexHelper n [])
+
+val stringFromIntegerHex : integer -> string
+let (*~{ocaml}*) stringFromIntegerHex i = 
+  if i < 0 then 
+    "-" ^ stringFromNaturalHex (naturalFromInteger i)
+  else
+    stringFromNaturalHex (naturalFromInteger i)
+
+
+let stringFromAddress (Address bs i) = 
+  let i' = integer_of_byte_list bs in
+  if i=i' then
+(*TODO: ideally this should be made to match the src/pp.ml pp_address; the following very roughly matches what's used in the ppcmem UI, enough to make exceptions readable *)
+    if i < 65535 then 
+      show i 
+    else
+      stringFromIntegerHex i
+  else
+    "stringFromAddress bytes and integer mismatch"
+
+instance (Show address)
+  let show = stringFromAddress
+end
+
+let stringFromByte_lifted bl =
+  match byte_of_byte_lifted bl with
+  | Nothing -> "u?"  
+  | Just (Byte bits) -> 
+      let i = integer_of_bit_list bits in
+      show i
+  end
+
+instance (Show byte_lifted)
+  let show = stringFromByte_lifted
+end
+
+(* possible next instruction address options *)
+type nia = 
+  | NIA_successor
+  | NIA_concrete_address of address
+  | NIA_LR   (* "LR0:61 || 0b00" in Power pseudocode *)
+  | NIA_CTR  (* "CTR0:61 || 0b00" in Power pseudocode *)
+  | NIA_register of reg_name (* the address will be in a register,
+                                corresponds to AArch64 BLR, BR, RET
+                                instructions *)
+
+let niaCompare n1 n2 = match (n1,n2) with
+  | (NIA_successor,NIA_successor) -> EQ
+  | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
+  | (NIA_LR,NIA_LR) -> EQ
+  | (NIA_CTR,NIA_CTR) -> EQ
+  | (NIA_register r1,NIA_register r2) -> compare r1 r2
+
+  | (NIA_successor,_) -> LT
+  | (NIA_concrete_address _,_) -> LT
+  | (NIA_LR,_) -> LT
+  | (NIA_CTR,_) -> LT
+  | (_,_) -> GT
+  end
+
+instance (Ord nia)
+  let compare = niaCompare
+  let (<)  n1 n2 = (niaCompare n1 n2) = LT
+  let (<=) n1 n2 = (niaCompare n1 n2) <> GT
+  let (>)  n1 n2 = (niaCompare n1 n2) = GT
+  let (>=) n1 n2 = (niaCompare n1 n2) <> LT
+end
+
+let stringFromNia = function
+  | NIA_successor -> "NIA_successor"
+  | NIA_concrete_address a -> "NIA_concrete_address " ^ show a
+  | NIA_LR -> "NIA_LR"
+  | NIA_CTR -> "NIA_CTR"
+  | NIA_register r -> "NIA_register " ^ show r
+end
+
+instance (Show nia)
+  let show = stringFromNia
+end
+
+type dia =
+  | DIA_none
+  | DIA_concrete_address of address
+  | DIA_register of reg_name
+
+let diaCompare d1 d2 = match (d1, d2) with
+  | (DIA_none, DIA_none) -> EQ
+  | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2
+  | (DIA_register r1, DIA_register r2) -> compare r1 r2
+  | (DIA_none, _) -> LT
+  | (DIA_concrete_address _, _) -> LT
+  | (DIA_register _, _) -> LT
+end
+
+instance (Ord dia)
+  let compare = diaCompare
+  let (<)  n1 n2 = (diaCompare n1 n2) = LT
+  let (<=) n1 n2 = (diaCompare n1 n2) <> GT
+  let (>)  n1 n2 = (diaCompare n1 n2) = GT
+  let (>=) n1 n2 = (diaCompare n1 n2) <> LT
+end
+
+let stringFromDia = function
+  | DIA_none               ->  "DIA_none"
+  | DIA_concrete_address a ->  "DIA_concrete_address " ^ show a
+  | DIA_register r ->  "DIA_delayed_register " ^ show r
+end
+
+instance (Show dia)
+  let show = stringFromDia
+end
+
+
+type v_kind = Bitv | Bytev
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 7f9866f4..b73cb6e1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2079,7 +2079,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
 
 let doc_id_lem_ctor (Id_aux(i,_)) =
   match i with
-  | Id("bit") -> string "bit" 
+  | Id("bit") -> string "bitU" 
   | Id("int") -> string "integer"
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
@@ -2145,7 +2145,9 @@ let doc_typ_lem, doc_atomic_typ_lem =
          if atyp_needed then parens tpp else tpp
       | _ -> atomic_typ atyp_needed regtypes ty 
     and atomic_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_id (Id_aux (Id "bool",_)) -> string "bit"
+      | Typ_id (Id_aux (Id "bool",_)) -> string "bitU"
+      | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU"
+      | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
       | Typ_id ((Id_aux (Id name,_)) as id) ->
          if List.exists ((=) name) regtypes
          then string "register"
@@ -3037,7 +3039,7 @@ let reg_decls (Defs defs) =
       (separate space [string "type";string "regstate";equals])
       (anglebars
          ((separate_map (semi ^^ break 1))
-            (fun (reg,_) -> separate space [string (String.lowercase reg);colon;string "vector bit"])
+            (fun (reg,_) -> separate space [string (String.lowercase reg);colon;string "vector bitU"])
             regs
          )) in
 
diff --git a/src/process_file.ml b/src/process_file.ml
index d12c1415..f1878609 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -179,7 +179,7 @@ let output1 libpath out_arg filename defs  =
          let ((o2,_, _) as ext_o2) =
            open_output_with_check_unformatted (f' ^ "embed.lem") in
          (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
-           ["Pervasives_extra";"Vector";"State";"Arch";"Sail_values"];
+           ["Pervasives_extra";"Vector";"Prompt";"Arch";"Sail_values"];
          close_output_with_check ext_o1;
          close_output_with_check ext_o2
       | Lem_out (Some lib) ->
@@ -188,7 +188,7 @@ let output1 libpath out_arg filename defs  =
          let ((o2,_, _) as ext_o2) =
            open_output_with_check_unformatted (f' ^ "embed.lem") in
 	 (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
-           ["Pervasives_extra";"Vector";"State";"Arch";"Sail_values"; lib];
+           ["Pervasives_extra";"Vector";"Prompt";"Arch";"Sail_values"; lib];
          close_output_with_check ext_o1;
          close_output_with_check ext_o2
       | Ocaml_out None ->