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

1 files changed, 1309 insertions, 0 deletions

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