Coq MIPS snapshot

12 files changed, 4481 insertions, 0 deletions

diff --git a/snapshots/coq/lib/coq/Makefile b/snapshots/coq/lib/coq/Makefile
new file mode 100644
index 00000000..97869e3c
--- /dev/null
+++ b/snapshots/coq/lib/coq/Makefile
@@ -0,0 +1,24 @@
+BBV_DIR=../../../bbv/theories
+
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v
+
+COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
+
+TARGETS=$(SRC:.v=.vo)
+
+.PHONY: all clean *.ide
+
+all: $(TARGETS)
+clean:
+	rm -f -- $(TARGETS) $(TARGETS:.vo=.glob) $(TARGETS:%.vo=.%.aux) deps
+
+%.vo: %.v
+	coqc $(COQ_LIBS) $<
+
+%.ide: %.v
+	coqide $(COQ_LIBS) $<
+
+deps: $(SRC)
+	coqdep $(COQ_LIBS) $(SRC) > deps
+
+-include deps
diff --git a/snapshots/coq/lib/coq/Sail2_impl_base.v b/snapshots/coq/lib/coq/Sail2_impl_base.v
new file mode 100644
index 00000000..639083f6
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_impl_base.v
@@ -0,0 +1,1058 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import Sail2_instr_kinds.
+
+(*
+class ( EnumerationType 'a ) 
+  val toNat : 'a -> nat
+end
+
+
+val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
+let ~{ocaml} enumeration_typeCompare e1 e2 =
+  compare (toNat e1) (toNat e2)
+let inline {ocaml} enumeration_typeCompare = defaultCompare
+
+ 
+default_instance forall 'a. EnumerationType 'a => (Ord 'a)
+  let compare = enumeration_typeCompare
+  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
+  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
+  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
+  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
+end
+
+
+
+(* 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    (* used for modelling h/w arch unspecified bits *)
+  | Bitl_unknown  (* used for interpreter analysis exhaustive execution *)
+
+type direction = 
+  | D_increasing
+  | D_decreasing
+
+let dir_of_bool is_inc = if is_inc then D_increasing else D_decreasing
+let bool_of_dir = function
+  | D_increasing -> true
+  | D_decreasing -> false
+  end
+
+(* 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 *)
+(* the head of the list is the byte stored at the lowest address;
+when calling a Sail function with a wmv effect, the least significant 8
+bits of the bit vector passed to the function will be interpreted as
+the lowest address byte; similarly, when calling a Sail function with
+rmem effect, the lowest address byte will be placed in the least
+significant 8 bits of the bit vector returned by the function; this
+behaviour is consistent with little-endian. *)
+
+
+(* 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 *)
+
+instance (EnumerationType bit)
+  let toNat = function
+    | Bitc_zero -> 0
+    | Bitc_one -> 1
+  end
+end
+
+instance (EnumerationType bit_lifted)
+  let toNat = function
+    | Bitl_zero -> 0
+    | Bitl_one -> 1
+    | Bitl_undef -> 2
+    | Bitl_unknown -> 3
+  end
+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} opcodeCompare (Opcode o1) (Opcode o2) =
+  compare o1 o2
+let {ocaml} opcodeCompare = defaultCompare
+
+let ~{ocaml} opcodeLess b1 b2      = opcodeCompare b1 b2 =  LT
+let ~{ocaml} opcodeLessEq b1 b2    = opcodeCompare b1 b2 <> GT
+let ~{ocaml} opcodeGreater b1 b2   = opcodeCompare b1 b2 =  GT
+let ~{ocaml} opcodeGreaterEq b1 b2 = opcodeCompare b1 b2 <> LT
+
+let inline {ocaml} opcodeLess      = defaultLess
+let inline {ocaml} opcodeLessEq    = defaultLessEq
+let inline {ocaml} opcodeGreater   = defaultGreater
+let inline {ocaml} opcodeGreaterEq = defaultGreaterEq
+
+instance (Ord opcode)
+  let compare = opcodeCompare
+  let (<)  = opcodeLess
+  let (<=) = opcodeLessEq
+  let (>)  = opcodeGreater
+  let (>=) = opcodeGreaterEq
+end
+
+let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
+(* this cannot be defaultCompare for OCaml because addresses contain big ints *)
+
+let addressLess b1 b2      = addressCompare b1 b2 =  LT
+let addressLessEq b1 b2    = addressCompare b1 b2 <> GT
+let addressGreater b1 b2   = addressCompare b1 b2 =  GT
+let addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT
+
+instance (SetType address)
+  let setElemCompare = addressCompare
+end
+
+instance (Ord address)
+  let compare = addressCompare
+  let (<)  = addressLess
+  let (<=) = addressLessEq
+  let (>)  = addressGreater
+  let (>=) = addressGreaterEq
+end
+
+let {coq; ocaml} addressEqual a1 a2 = (addressCompare a1 a2) = EQ
+let inline {hol; isabelle} addressEqual = unsafe_structural_equality
+
+let {coq; ocaml} addressInequal a1 a2 = not (addressEqual a1 a2)
+let inline {hol; isabelle} 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
+
+instance (Show direction)
+  let show = function D_increasing -> "D_increasing" | D_decreasing  -> "D_decreasing" end
+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 address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) =
+  compare (i1,b1) (i2,b2)
+(* this cannot be defaultCompare for OCaml because address_lifteds contain big
+   ints *)
+
+let address_liftedLess b1 b2      = address_liftedCompare b1 b2 =  LT
+let address_liftedLessEq b1 b2    = address_liftedCompare b1 b2 <> GT
+let address_liftedGreater b1 b2   = address_liftedCompare b1 b2 =  GT
+let address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT
+
+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 width_of_reg_name (r: reg_name) : nat =
+  let width_of_slice (i, j) = (* j - i + 1 in *)
+
+    (integerFromNat j) - (integerFromNat i) + 1
+    $> abs $> natFromInteger
+  in
+  match r with
+  | Reg _ _ width _          -> width
+  | Reg_slice _ _ _ sl       -> width_of_slice sl
+  | Reg_field _ _ _ _ sl     -> width_of_slice sl
+  | Reg_f_slice _ _ _ _ _ sl -> width_of_slice 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 {coq;ocaml} reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ
+let {hol;isabelle} reg_nameEqual = unsafe_structural_equality
+let {coq;ocaml} reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2)
+let {hol;isabelle} reg_nameInequal = unsafe_structural_inequality
+
+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 *)
+
+(* read_kind, write_kind, barrier_kind, trans_kind and instruction_kind have
+   been moved to sail_instr_kinds.lem.  This removes the dependency of the
+   shallow embedding on the rest of sail_impl_base.lem, and helps avoid name
+   clashes between the different monad types. *)
+
+type event = 
+  | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+  | E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
+  | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
+  | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
+  | E_excl_res
+  | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
+  | E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
+  | E_barrier of barrier_kind
+  | E_footprint 
+  | E_read_reg of reg_name
+  | E_write_reg of reg_name * register_value
+  | E_escape
+  | E_error of string 
+
+
+let eventCompare e1 e2 = 
+  match (e1,e2) with
+  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
+     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_read_memt rk1 v1 i1 tr1, E_read_memt rk2 v2 i2 tr2) ->
+     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
+    compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
+  | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
+    compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
+  | (E_excl_res, E_excl_res) -> EQ
+  | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
+  | (E_write_memvt _ mv1 tr1, E_write_memvt _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
+  | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
+  | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
+  | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
+  | (E_error s1, E_error s2) -> compare s1 s2
+  | (E_escape,E_escape) -> EQ
+  | (E_read_mem _ _ _ _, _) -> LT
+  | (E_write_mem _ _ _ _ _ _, _) -> LT
+  | (E_write_ea _ _ _ _, _) -> LT
+  | (E_excl_res, _) -> LT
+  | (E_write_memv _ _ _, _) -> LT
+  | (E_barrier _, _) -> LT
+  | (E_read_reg _, _) -> LT
+  | (E_write_reg _ _, _) -> LT
+  | _ -> GT
+  end
+
+let eventLess b1 b2      = eventCompare b1 b2 =  LT
+let eventLessEq b1 b2    = eventCompare b1 b2 <> GT
+let eventGreater b1 b2   = eventCompare b1 b2 =  GT
+let eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT
+
+instance (Ord event)
+  let compare = eventCompare
+  let (<)  = eventLess
+  let (<=) = eventLessEq
+  let (>)  = eventGreater
+  let (>=) = eventGreaterEq
+end
+
+instance (SetType event)
+  let setElemCompare = compare
+end
+
+
+(* the address_lifted types should go away here and be replaced by address *)
+type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
+type outcome 'a 'e =
+  (* 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 -> with_aux (outcome 'a 'e))
+  (* Tell the system a write is imminent, at address lifted, of size nat *)
+  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a 'e))
+  (* Request the result of store-exclusive *)
+  | Excl_res of (bool -> with_aux (outcome 'a 'e))
+  (* 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 -> with_aux (outcome 'a 'e))
+  (* Request a memory barrier *)
+  | Barrier of barrier_kind * with_aux (outcome 'a 'e)
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of with_aux (outcome 'a 'e)
+  (* Request to read register, will track dependency when mode.track_values *)
+  | Read_reg of reg_name * (register_value -> with_aux (outcome 'a 'e))
+  (* Request to write register *)
+  | Write_reg of (reg_name * register_value) * with_aux (outcome 'a 'e)
+  | Escape of maybe string
+  (*Result of a failed assert with possible error message to report*)
+  | Fail of maybe string
+  (* Exception of type 'e *)
+  | Exception of 'e
+  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a 'e)
+  | Done of 'a
+  | Error of string
+
+type outcome_s 'a 'e = with_aux (outcome 'a 'e)
+(* first string : output of instruction_stack_to_string
+   second string: output of local_variables_to_string *)
+
+(** 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 register_value_for_reg : reg_name -> list bit_lifted -> register_value
+let register_value_for_reg r bs : register_value =
+  let () = ensure (width_of_reg_name r = List.length bs)
+      ("register_value_for_reg (\"" ^ show (register_base_name r) ^ "\") length mismatch: "
+          ^ show (width_of_reg_name r) ^ " vs " ^ show (List.length bs))
+  in
+  let (j1, j2) = slice_of_reg_name r in
+  let d = direction_of_reg_name r in
+  <|  rv_bits = bs;
+      rv_dir = d;
+      rv_start_internal = if d = D_increasing then j1 else (start_of_reg_name r) - j1;
+      rv_start = j1;
+  |>
+
+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 
+
+val match_endianness : forall 'a. end_flag -> list 'a -> list 'a
+let match_endianness endian l =
+  match endian with
+  | E_little_endian -> List.reverse l
+  | E_big_endian    -> l
+  end
+
+(* 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)
+
+let address_of_byte_lifted_list bls =
+  match maybe_all (List.map byte_of_byte_lifted bls) with
+  | Nothing -> Nothing
+  | Just bs -> Just (address_of_byte_list bs)
+  end
+
+(* 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 =
+  match_endianness endian mv
+  $> List.map byte_of_memory_byte
+  $> maybe_all
+
+
+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 =
+  List.map byte_lifted_of_byte (byte_list_of_integer len i)
+  $> match_endianness endian
+
+
+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
+
+(* NOTE: register_value_for_reg_of_integer might be easier to use *)
+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 register_value_for_reg_of_integer : reg_name -> integer -> register_value
+let register_value_for_reg_of_integer (r: reg_name) (i:integer) : register_value =
+  register_value_of_integer (width_of_reg_name r) (start_of_reg_name r) (direction_of_reg_name r) i
+
+(* *)
+
+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) =
+  match_endianness endian 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 _) =
+  match_endianness endian bs
+  $> List.map byte_lifted_of_byte
+
+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 =
+  let norm_sl start dir (first,second) = (first,second)
+    (* match dir with
+      | D_increasing -> (first,second)
+      | D_decreasing -> (start - first, start - second)
+    end *)
+  in
+  match r with
+  | Reg s start size dir -> s
+  | Reg_slice s start dir sl ->
+      let (first,second) = norm_sl start dir sl in
+      s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
+  | Reg_field s start dir f sl ->
+      let (first,second) = norm_sl start dir sl in
+      s ^ "." ^ f ^ " (" ^ (show start) ^ ", " ^ (show dir) ^ ", " ^ (show first) ^ ", " ^ (show second) ^ ")"
+  | 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_indirect_address
+
+let niaCompare n1 n2 = match (n1,n2) with
+  | (NIA_successor, NIA_successor) -> EQ
+  | (NIA_successor, _) -> LT
+  | (_, NIA_successor) -> GT
+  | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
+  | (NIA_concrete_address _, _) -> LT
+  | (_, NIA_concrete_address _) -> GT
+  | (NIA_indirect_address, NIA_indirect_address) -> EQ
+  (* | (NIA_indirect_address, _) -> LT
+  | (_, NIA_indirect_address) -> 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_indirect_address   -> "NIA_indirect_address"
+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_none, _) -> LT
+  | (DIA_concrete_address a1, DIA_none) -> GT
+  | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2
+  | (DIA_concrete_address a1, _) -> LT
+  | (DIA_register r1, DIA_register r2) -> compare r1 r2
+  | (DIA_register _, _) -> GT
+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
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_instr_kinds.v b/snapshots/coq/lib/coq/Sail2_instr_kinds.v
new file mode 100644
index 00000000..0145d8b3
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_instr_kinds.v
@@ -0,0 +1,253 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+
+(*
+
+class ( EnumerationType 'a )
+  val toNat : 'a -> nat
+end
+
+
+val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
+let ~{ocaml} enumeration_typeCompare e1 e2 :=
+  compare (toNat e1) (toNat e2)
+let inline {ocaml} enumeration_typeCompare := defaultCompare
+
+
+default_instance forall 'a. EnumerationType 'a => (Ord 'a)
+  let compare := enumeration_typeCompare
+  let (<)  r1 r2 := (enumeration_typeCompare r1 r2) = LT
+  let (<=) r1 r2 := (enumeration_typeCompare r1 r2) <> GT
+  let (>)  r1 r2 := (enumeration_typeCompare r1 r2) = GT
+  let (>=) r1 r2 := (enumeration_typeCompare r1 r2) <> LT
+end
+*)
+
+(* Data structures for building up instructions *)
+
+(* careful: changes in the read/write/barrier kinds have to be
+   reflected in deep_shallow_convert *)
+Inductive read_kind :=
+  (* common reads *)
+  | Read_plain
+  (* Power reads *)
+  | Read_reserve
+  (* AArch64 reads *)
+  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+  (* RISC-V reads *)
+  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
+  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
+  | Read_RISCV_reserved_strong_acquire
+  (* x86 reads *)
+  | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
+.
+(*
+instance (Show read_kind)
+  let show := function
+    | Read_plain -> "Read_plain"
+    | Read_reserve -> "Read_reserve"
+    | Read_acquire -> "Read_acquire"
+    | Read_exclusive -> "Read_exclusive"
+    | Read_exclusive_acquire -> "Read_exclusive_acquire"
+    | Read_stream -> "Read_stream"
+    | Read_RISCV_acquire -> "Read_RISCV_acquire"
+    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
+    | Read_RISCV_reserved -> "Read_RISCV_reserved"
+    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
+    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
+    | Read_X86_locked -> "Read_X86_locked"
+  end
+end
+*)
+Inductive write_kind :=
+  (* common writes *)
+  | Write_plain
+  (* Power writes *)
+  | Write_conditional
+  (* AArch64 writes *)
+  | Write_release | Write_exclusive | Write_exclusive_release
+  (* RISC-V *)
+  | Write_RISCV_release     | Write_RISCV_strong_release
+  | Write_RISCV_conditional | Write_RISCV_conditional_release
+  | Write_RISCV_conditional_strong_release
+  (* x86 writes *)
+  | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
+.
+(*
+instance (Show write_kind)
+  let show := function
+    | Write_plain -> "Write_plain"
+    | Write_conditional -> "Write_conditional"
+    | Write_release -> "Write_release"
+    | Write_exclusive -> "Write_exclusive"
+    | Write_exclusive_release -> "Write_exclusive_release"
+    | Write_RISCV_release -> "Write_RISCV_release"
+    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
+    | Write_RISCV_conditional -> "Write_RISCV_conditional"
+    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
+    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
+    | Write_X86_locked -> "Write_X86_locked"
+  end
+end
+*)
+Inductive barrier_kind :=
+  (* Power barriers *)
+  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
+  (* AArch64 barriers *)
+  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
+  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
+  | Barrier_TM_COMMIT
+  (* MIPS barriers *)
+  | Barrier_MIPS_SYNC
+  (* RISC-V barriers *)
+  | Barrier_RISCV_rw_rw
+  | Barrier_RISCV_r_rw
+  | Barrier_RISCV_r_r
+  | Barrier_RISCV_rw_w
+  | Barrier_RISCV_w_w
+  | Barrier_RISCV_i
+  (* X86 *)
+  | Barrier_x86_MFENCE.
+
+(*
+instance (Show barrier_kind)
+  let show := function
+    | Barrier_Sync -> "Barrier_Sync"
+    | Barrier_LwSync -> "Barrier_LwSync"
+    | Barrier_Eieio -> "Barrier_Eieio"
+    | Barrier_Isync -> "Barrier_Isync"
+    | Barrier_DMB -> "Barrier_DMB"
+    | Barrier_DMB_ST -> "Barrier_DMB_ST"
+    | Barrier_DMB_LD -> "Barrier_DMB_LD"
+    | Barrier_DSB -> "Barrier_DSB"
+    | Barrier_DSB_ST -> "Barrier_DSB_ST"
+    | Barrier_DSB_LD -> "Barrier_DSB_LD"
+    | Barrier_ISB -> "Barrier_ISB"
+    | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
+    | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
+    | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
+    | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
+    | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
+    | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
+    | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_i     -> "Barrier_RISCV_i"
+    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
+  end
+end*)
+
+Inductive trans_kind :=
+  (* AArch64 *)
+  | Transaction_start | Transaction_commit | Transaction_abort.
+(*
+instance (Show trans_kind)
+  let show := function
+  | Transaction_start  -> "Transaction_start"
+  | Transaction_commit -> "Transaction_commit"
+  | Transaction_abort  -> "Transaction_abort"
+  end
+end*)
+
+Inductive instruction_kind :=
+  | IK_barrier   : barrier_kind -> instruction_kind
+  | IK_mem_read  : read_kind -> instruction_kind
+  | IK_mem_write : write_kind -> instruction_kind
+  | IK_mem_rmw   : (read_kind * write_kind) -> instruction_kind
+  | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+  indirect/computed-branch (single nia of kind NIA_indirect_address)
+  and branch/jump (single nia of kind NIA_concrete_address) *)
+  | IK_trans     : trans_kind -> instruction_kind
+  | IK_simple    : instruction_kind.
+
+(*
+instance (Show instruction_kind)
+  let show := function
+    | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
+    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
+    | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
+    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
+    | IK_branch               -> "IK_branch"
+    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
+    | IK_simple               -> "IK_simple"
+  end
+end
+*)
+
+Definition read_is_exclusive r :=
+match r with
+  | Read_plain => false
+  | Read_reserve => true
+  | Read_acquire => false
+  | Read_exclusive => true
+  | Read_exclusive_acquire => true
+  | Read_stream => false
+  | Read_RISCV_acquire => false
+  | Read_RISCV_strong_acquire => false
+  | Read_RISCV_reserved => true
+  | Read_RISCV_reserved_acquire => true
+  | Read_RISCV_reserved_strong_acquire => true
+  | Read_X86_locked => true
+end.
+
+
+(*
+instance (EnumerationType read_kind)
+  let toNat := function
+    | Read_plain -> 0
+    | Read_reserve -> 1
+    | Read_acquire -> 2
+    | Read_exclusive -> 3
+    | Read_exclusive_acquire -> 4
+    | Read_stream -> 5
+    | Read_RISCV_acquire -> 6
+    | Read_RISCV_strong_acquire -> 7
+    | Read_RISCV_reserved -> 8
+    | Read_RISCV_reserved_acquire -> 9
+    | Read_RISCV_reserved_strong_acquire -> 10
+    | Read_X86_locked -> 11
+  end
+end
+
+instance (EnumerationType write_kind)
+  let toNat := function
+    | Write_plain -> 0
+    | Write_conditional -> 1
+    | Write_release -> 2
+    | Write_exclusive -> 3
+    | Write_exclusive_release -> 4
+    | Write_RISCV_release -> 5
+    | Write_RISCV_strong_release -> 6
+    | Write_RISCV_conditional -> 7
+    | Write_RISCV_conditional_release -> 8
+    | Write_RISCV_conditional_strong_release -> 9
+    | Write_X86_locked -> 10
+  end
+end
+
+instance (EnumerationType barrier_kind)
+  let toNat := function
+    | Barrier_Sync -> 0
+    | Barrier_LwSync -> 1
+    | Barrier_Eieio ->2
+    | Barrier_Isync -> 3
+    | Barrier_DMB -> 4
+    | Barrier_DMB_ST -> 5
+    | Barrier_DMB_LD -> 6
+    | Barrier_DSB -> 7
+    | Barrier_DSB_ST -> 8
+    | Barrier_DSB_LD -> 9
+    | Barrier_ISB -> 10
+    | Barrier_TM_COMMIT -> 11
+    | Barrier_MIPS_SYNC -> 12
+    | Barrier_RISCV_rw_rw -> 13
+    | Barrier_RISCV_r_rw -> 14
+    | Barrier_RISCV_r_r -> 15
+    | Barrier_RISCV_rw_w -> 16
+    | Barrier_RISCV_w_w -> 17
+    | Barrier_RISCV_i -> 18
+    | Barrier_x86_MFENCE -> 19
+  end
+end
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_operators.v b/snapshots/coq/lib/coq/Sail2_operators.v
new file mode 100644
index 00000000..5a8b1119
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_operators.v
@@ -0,0 +1,237 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import Sail2_values.
+Require List.
+Import List.ListNotations.
+
+(*** Bit vector operations *)
+
+Section Bitvectors.
+Context {a b c} `{Bitvector a} `{Bitvector b} `{Bitvector c}.
+
+(*val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c*)
+Definition concat_bv (l : a) (r : b) : list bitU := bits_of l ++ bits_of r.
+
+(*val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b*)
+Definition cons_bv b' (v : a) : list bitU := b' :: bits_of v.
+
+Definition cast_unit_bv b : list bitU := [b].
+Definition bv_of_bit len b : list bitU := extz_bits len [b].
+
+(*Definition most_significant v := match bits_of v with
+  | cons b _ => b
+  | _ => failwith "most_significant applied to empty vector"
+  end.
+
+Definition get_max_representable_in sign (n : integer) : integer :=
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+Definition get_min_representable_in _ (n : integer) : integer :=
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a*)
+Definition arith_op_bv_int {a} `{Bitvector a} (op : Z -> Z -> Z) (sign : bool) (l : a) (r : Z) : a :=
+  let r' := of_int (length l) r in
+  arith_op_bv op sign l r'.
+
+(*val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a*)
+Definition arith_op_int_bv {a} `{Bitvector a} (op : Z -> Z -> Z) (sign : bool) (l : Z) (r : a) : a :=
+  let l' := of_int (length r) l in
+  arith_op_bv op sign l' r.
+(*
+Definition add_bv_int := arith_op_bv_int Zplus false 1.
+Definition sadd_bv_int := arith_op_bv_int Zplus true 1.
+Definition sub_bv_int := arith_op_bv_int Zminus false 1.
+Definition mult_bv_int := arith_op_bv_int Zmult false 2.
+Definition smult_bv_int := arith_op_bv_int Zmult true 2.
+
+(*val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b
+Definition arith_op_int_bv op sign size l r :=
+  let r' = int_of_bv sign r in
+  let n = op l r' in
+  of_int (size * length r) n
+
+Definition add_int_bv = arith_op_int_bv integerAdd false 1
+Definition sadd_int_bv = arith_op_int_bv integerAdd true 1
+Definition sub_int_bv = arith_op_int_bv integerMinus false 1
+Definition mult_int_bv = arith_op_int_bv integerMult false 2
+Definition smult_int_bv = arith_op_int_bv integerMult true 2
+
+Definition arith_op_bv_bit op sign (size : integer) l r :=
+  let l' = int_of_bv sign l in
+  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
+  of_int (size * length l) n
+
+Definition add_bv_bit := arith_op_bv_bit integerAdd false 1
+Definition sadd_bv_bit := arith_op_bv_bit integerAdd true 1
+Definition sub_bv_bit := arith_op_bv_bit integerMinus true 1
+
+val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU)
+Definition arith_op_overflow_bv op sign size l r :=
+  let len := length l in
+  let act_size := len * size in
+  let (l_sign,r_sign) := (int_of_bv sign l,int_of_bv sign r) in
+  let (l_unsign,r_unsign) := (int_of_bv false l,int_of_bv false r) in
+  let n := op l_sign r_sign in
+  let n_unsign := op l_unsign r_unsign in
+  let correct_size := of_int act_size n in
+  let one_more_size_u := bits_of_int (act_size + 1) n_unsign in
+  let overflow :=
+    if n <= get_max_representable_in sign len &&
+         n >= get_min_representable_in sign len
+    then B0 else B1 in
+  let c_out := most_significant one_more_size_u in
+  (correct_size,overflow,c_out)
+
+Definition add_overflow_bv := arith_op_overflow_bv integerAdd false 1
+Definition add_overflow_bv_signed := arith_op_overflow_bv integerAdd true 1
+Definition sub_overflow_bv := arith_op_overflow_bv integerMinus false 1
+Definition sub_overflow_bv_signed := arith_op_overflow_bv integerMinus true 1
+Definition mult_overflow_bv := arith_op_overflow_bv integerMult false 2
+Definition mult_overflow_bv_signed := arith_op_overflow_bv integerMult true 2
+
+val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU)
+Definition arith_op_overflow_bv_bit op sign size l r_bit :=
+  let act_size := length l * size in
+  let l' := int_of_bv sign l in
+  let l_u := int_of_bv false l in
+  let (n,nu,changed) := match r_bit with
+    | B1 -> (op l' 1, op l_u 1, true)
+    | B0 -> (l',l_u,false)
+    | BU -> failwith "arith_op_overflow_bv_bit applied to undefined bit"
+    end in
+  let correct_size := of_int act_size n in
+  let one_larger := bits_of_int (act_size + 1) nu in
+  let overflow :=
+    if changed
+    then
+      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+      then B0 else B1
+    else B0 in
+  (correct_size,overflow,most_significant one_larger)
+
+Definition add_overflow_bv_bit := arith_op_overflow_bv_bit integerAdd false 1
+Definition add_overflow_bv_bit_signed := arith_op_overflow_bv_bit integerAdd true 1
+Definition sub_overflow_bv_bit := arith_op_overflow_bv_bit integerMinus false 1
+Definition sub_overflow_bv_bit_signed := arith_op_overflow_bv_bit integerMinus true 1
+
+type shift := LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
+
+val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a
+Definition shift_op_bv op v n :=
+  match op with
+  | LL_shift ->
+     of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n)
+  | RR_shift ->
+     of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1))
+  | RR_shift_arith ->
+     of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1))
+  | LL_rot ->
+     of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1))
+  | RR_rot ->
+     of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1))
+  end
+
+Definition shiftl_bv := shift_op_bv LL_shift (*"<<"*)
+Definition shiftr_bv := shift_op_bv RR_shift (*">>"*)
+Definition arith_shiftr_bv := shift_op_bv RR_shift_arith
+Definition rotl_bv := shift_op_bv LL_rot (*"<<<"*)
+Definition rotr_bv := shift_op_bv LL_rot (*">>>"*)
+
+Definition shiftl_mword w n := Machine_word.shiftLeft w (natFromInteger n)
+Definition shiftr_mword w n := Machine_word.shiftRight w (natFromInteger n)
+Definition rotl_mword w n := Machine_word.rotateLeft (natFromInteger n) w
+Definition rotr_mword w n := Machine_word.rotateRight (natFromInteger n) w
+
+Definition rec arith_op_no0 (op : integer -> integer -> integer) l r :=
+  if r = 0
+  then Nothing
+  else Just (op l r)
+
+val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b
+Definition arith_op_bv_no0 op sign size l r :=
+  let act_size := length l * size in
+  let (l',r') := (int_of_bv sign l,int_of_bv sign r) in
+  let n := arith_op_no0 op l' r' in
+  let (representable,n') :=
+    match n with
+    | Just n' ->
+      (n' <= get_max_representable_in sign act_size &&
+         n' >= get_min_representable_in sign act_size, n')
+    | _ -> (false,0)
+    end in
+  if representable then (of_int act_size n') else (of_bits (repeat [BU] act_size))
+
+Definition mod_bv := arith_op_bv_no0 hardware_mod false 1
+Definition quot_bv := arith_op_bv_no0 hardware_quot false 1
+Definition quot_bv_signed := arith_op_bv_no0 hardware_quot true 1
+
+Definition mod_mword := Machine_word.modulo
+Definition quot_mword := Machine_word.unsignedDivide
+Definition quot_mword_signed := Machine_word.signedDivide
+
+Definition arith_op_bv_int_no0 op sign size l r :=
+  arith_op_bv_no0 op sign size l (of_int (length l) r)
+
+Definition quot_bv_int := arith_op_bv_int_no0 hardware_quot false 1
+Definition mod_bv_int := arith_op_bv_int_no0 hardware_mod false 1
+*)
+Definition replicate_bits_bv {a b} `{Bitvector a} `{Bitvector b} (v : a) count : b := of_bits (repeat (bits_of v) count).
+Import List.
+Import ListNotations.
+Definition duplicate_bit_bv {a} `{Bitvector a} bit len : a := replicate_bits_bv [bit] len.
+
+(*val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+Definition eq_bv {A} `{Bitvector A} (l : A) r := (unsigned l =? unsigned r).
+
+(*val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+Definition neq_bv (l : a) (r :a) : bool := (negb (unsigned l =? unsigned r)).
+(*
+val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+Definition ucmp_bv cmp l r := cmp (unsigned l) (unsigned r)
+
+val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+Definition scmp_bv cmp l r := cmp (signed l) (signed r)
+
+Definition ult_bv := ucmp_bv (<)
+Definition slt_bv := scmp_bv (<)
+Definition ugt_bv := ucmp_bv (>)
+Definition sgt_bv := scmp_bv (>)
+Definition ulteq_bv := ucmp_bv (<=)
+Definition slteq_bv := scmp_bv (<=)
+Definition ugteq_bv := ucmp_bv (>=)
+Definition sgteq_bv := scmp_bv (>=)
+*)
+
+(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)*)
+Definition get_slice_int_bv {a} `{Bitvector a} len n lo : a :=
+  let hi := lo + len - 1 in
+  let bs := bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo).
+
+(*val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+Definition set_slice_int_bv {a} `{Bitvector a} len n lo (v : a) :=
+  let hi := lo + len - 1 in
+  let bs := bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v))).*)
+
+End Bitvectors.
diff --git a/snapshots/coq/lib/coq/Sail2_operators_bitlists.v b/snapshots/coq/lib/coq/Sail2_operators_bitlists.v
new file mode 100644
index 00000000..b0240c4e
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_operators_bitlists.v
@@ -0,0 +1,187 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import Sail2_values.
+Require Import Sail2_operators.
+
+(*
+
+(* Specialisation of operators to bit lists *)
+
+val access_vec_inc : list bitU -> integer -> bitU
+let access_vec_inc = access_bv_inc
+
+val access_vec_dec : list bitU -> integer -> bitU
+let access_vec_dec = access_bv_dec
+
+val update_vec_inc : list bitU -> integer -> bitU -> list bitU
+let update_vec_inc = update_bv_inc
+
+val update_vec_dec : list bitU -> integer -> bitU -> list bitU
+let update_vec_dec = update_bv_dec
+
+val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
+let subrange_vec_inc = subrange_bv_inc
+
+val subrange_vec_dec : list bitU -> integer -> integer -> list bitU
+let subrange_vec_dec = subrange_bv_dec
+
+val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU
+let update_subrange_vec_inc = update_subrange_bv_inc
+
+val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU
+let update_subrange_vec_dec = update_subrange_bv_dec
+
+val extz_vec : integer -> list bitU -> list bitU
+let extz_vec = extz_bv
+
+val exts_vec : integer -> list bitU -> list bitU
+let exts_vec = exts_bv
+
+val concat_vec : list bitU -> list bitU -> list bitU
+let concat_vec = concat_bv
+
+val cons_vec : bitU -> list bitU -> list bitU
+let cons_vec = cons_bv
+
+val bool_of_vec : mword ty1 -> bitU
+let bool_of_vec = bool_of_bv
+
+val cast_unit_vec : bitU -> mword ty1
+let cast_unit_vec = cast_unit_bv
+
+val vec_of_bit : integer -> bitU -> list bitU
+let vec_of_bit = bv_of_bit
+
+val msb : list bitU -> bitU
+let msb = most_significant
+
+val int_of_vec : bool -> list bitU -> integer
+let int_of_vec = int_of_bv
+
+val string_of_vec : list bitU -> string
+let string_of_vec = string_of_bv
+
+val and_vec : list bitU -> list bitU -> list bitU
+val or_vec  : list bitU -> list bitU -> list bitU
+val xor_vec : list bitU -> list bitU -> list bitU
+val not_vec : list bitU -> list bitU
+let and_vec = and_bv
+let or_vec  = or_bv
+let xor_vec = xor_bv
+let not_vec = not_bv
+
+val add_vec   : list bitU -> list bitU -> list bitU
+val sadd_vec  : list bitU -> list bitU -> list bitU
+val sub_vec   : list bitU -> list bitU -> list bitU
+val mult_vec  : list bitU -> list bitU -> list bitU
+val smult_vec : list bitU -> list bitU -> list bitU
+let add_vec   = add_bv
+let sadd_vec  = sadd_bv
+let sub_vec   = sub_bv
+let mult_vec  = mult_bv
+let smult_vec = smult_bv
+
+val add_vec_int   : list bitU -> integer -> list bitU
+val sadd_vec_int  : list bitU -> integer -> list bitU
+val sub_vec_int   : list bitU -> integer -> list bitU
+val mult_vec_int  : list bitU -> integer -> list bitU
+val smult_vec_int : list bitU -> integer -> list bitU
+let add_vec_int   = add_bv_int
+let sadd_vec_int  = sadd_bv_int
+let sub_vec_int   = sub_bv_int
+let mult_vec_int  = mult_bv_int
+let smult_vec_int = smult_bv_int
+
+val add_int_vec   : integer -> list bitU -> list bitU
+val sadd_int_vec  : integer -> list bitU -> list bitU
+val sub_int_vec   : integer -> list bitU -> list bitU
+val mult_int_vec  : integer -> list bitU -> list bitU
+val smult_int_vec : integer -> list bitU -> list bitU
+let add_int_vec   = add_int_bv
+let sadd_int_vec  = sadd_int_bv
+let sub_int_vec   = sub_int_bv
+let mult_int_vec  = mult_int_bv
+let smult_int_vec = smult_int_bv
+
+val add_vec_bit  : list bitU -> bitU -> list bitU
+val sadd_vec_bit : list bitU -> bitU -> list bitU
+val sub_vec_bit  : list bitU -> bitU -> list bitU
+let add_vec_bit  = add_bv_bit
+let sadd_vec_bit = sadd_bv_bit
+let sub_vec_bit  = sub_bv_bit
+
+val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec        : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec         = add_overflow_bv
+let add_overflow_vec_signed  = add_overflow_bv_signed
+let sub_overflow_vec         = sub_overflow_bv
+let sub_overflow_vec_signed  = sub_overflow_bv_signed
+let mult_overflow_vec        = mult_overflow_bv
+let mult_overflow_vec_signed = mult_overflow_bv_signed
+
+val add_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec_bit         = add_overflow_bv_bit
+let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit         = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed
+
+val shiftl       : list bitU -> integer -> list bitU
+val shiftr       : list bitU -> integer -> list bitU
+val arith_shiftr : list bitU -> integer -> list bitU
+val rotl         : list bitU -> integer -> list bitU
+val rotr         : list bitU -> integer -> list bitU
+let shiftl       = shiftl_bv
+let shiftr       = shiftr_bv
+let arith_shiftr = arith_shiftr_bv
+let rotl         = rotl_bv
+let rotr         = rotr_bv
+
+val mod_vec         : list bitU -> list bitU -> list bitU
+val quot_vec        : list bitU -> list bitU -> list bitU
+val quot_vec_signed : list bitU -> list bitU -> list bitU
+let mod_vec         = mod_bv
+let quot_vec        = quot_bv
+let quot_vec_signed = quot_bv_signed
+
+val mod_vec_int  : list bitU -> integer -> list bitU
+val quot_vec_int : list bitU -> integer -> list bitU
+let mod_vec_int  = mod_bv_int
+let quot_vec_int = quot_bv_int
+
+val replicate_bits : list bitU -> integer -> list bitU
+let replicate_bits = replicate_bits_bv
+
+val duplicate : bitU -> integer -> list bitU
+let duplicate = duplicate_bit_bv
+
+val eq_vec    : list bitU -> list bitU -> bool
+val neq_vec   : list bitU -> list bitU -> bool
+val ult_vec   : list bitU -> list bitU -> bool
+val slt_vec   : list bitU -> list bitU -> bool
+val ugt_vec   : list bitU -> list bitU -> bool
+val sgt_vec   : list bitU -> list bitU -> bool
+val ulteq_vec : list bitU -> list bitU -> bool
+val slteq_vec : list bitU -> list bitU -> bool
+val ugteq_vec : list bitU -> list bitU -> bool
+val sgteq_vec : list bitU -> list bitU -> bool
+let eq_vec    = eq_bv
+let neq_vec   = neq_bv
+let ult_vec   = ult_bv
+let slt_vec   = slt_bv
+let ugt_vec   = ugt_bv
+let sgt_vec   = sgt_bv
+let ulteq_vec = ulteq_bv
+let slteq_vec = slteq_bv
+let ugteq_vec = ugteq_bv
+let sgteq_vec = sgteq_bv
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_operators_mwords.v b/snapshots/coq/lib/coq/Sail2_operators_mwords.v
new file mode 100644
index 00000000..fba23071
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_operators_mwords.v
@@ -0,0 +1,438 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import Sail2_values.
+Require Import Sail2_operators.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+Require Import bbv.Word.
+Require bbv.BinNotation.
+Require Import Arith.
+Require Import ZArith.
+Require Import Omega.
+Require Import Eqdep_dec.
+
+Module Z_eq_dec.
+Definition U := Z.
+Definition eq_dec := Z.eq_dec.
+End Z_eq_dec.
+Module ZEqdep := DecidableEqDep (Z_eq_dec).
+
+Definition cast_mword {m n} (x : mword m) (eq : m = n) : mword n.
+rewrite <- eq.
+exact x.
+Defined.
+
+Lemma cast_mword_refl {m} {H:m = m} (x : mword m) : cast_mword x H = x.
+rewrite (ZEqdep.UIP _ _ H eq_refl).
+reflexivity.
+Qed.
+
+Definition autocast {m n} (x : mword m) `{H:ArithFact (m = n)} : mword n :=
+  cast_mword x (use_ArithFact H).
+
+Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m = n)} : monad rv (mword n) e :=
+  x >>= fun x => returnm (cast_mword x (use_ArithFact H)).
+
+Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n.
+rewrite <- eq.
+exact x.
+Defined.
+
+Lemma cast_word_refl {m} {H:m = m} (x : word m) : cast_word x H = x.
+rewrite (UIP_refl_nat _ H).
+reflexivity.
+Qed.
+
+Definition mword_of_nat {m} (x : Word.word m) : mword (Z.of_nat m).
+destruct m.
+- exact x.
+- simpl. rewrite SuccNat2Pos.id_succ. exact x.
+Defined.
+
+Definition cast_to_mword {m n} (x : Word.word m) (eq : Z.of_nat m = n) : mword n.
+destruct n.
+- constructor.
+- rewrite <- eq. exact (mword_of_nat x).
+- exfalso. destruct m; simpl in *; congruence.
+Defined.
+
+(*
+(* Specialisation of operators to machine words *)
+
+val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU*)
+Definition access_vec_inc {a} : mword a -> Z -> bitU := access_mword_inc.
+
+(*val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU*)
+Definition access_vec_dec {a} : mword a -> Z -> bitU := access_mword_dec.
+
+(*val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*)
+(* TODO: probably ought to use a monadic version instead, but using bad default for
+   type compatibility just now *)
+Definition update_vec_inc {a} (w : mword a) i b : mword a :=
+ opt_def w (update_mword_inc w i b).
+
+(*val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*)
+Definition update_vec_dec {a} (w : mword a) i b : mword a := opt_def w (update_mword_dec w i b).
+
+Lemma subrange_lemma0 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : (Z.to_nat o <= Z.to_nat m < Z.to_nat n)%nat.
+intros.
+unwrap_ArithFacts.
+split.
++ apply Z2Nat.inj_le; omega.
++ apply Z2Nat.inj_lt; omega.
+Qed.
+Lemma subrange_lemma1 {n m o} : (o <= m < n -> n = m + 1 + (n - (m + 1)))%nat.
+intros. omega.
+Qed.
+Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat.
+omega.
+Qed.
+Lemma subrange_lemma3 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} :
+  Z.of_nat (Z.to_nat m - Z.to_nat o + 1)%nat = m - o + 1.
+unwrap_ArithFacts.
+rewrite Nat2Z.inj_add.
+rewrite Nat2Z.inj_sub.
+repeat rewrite Z2Nat.id; try omega.
+reflexivity.
+apply Z2Nat.inj_le; omega.
+Qed.
+
+Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : mword (m - o + 1) :=
+  let n := Z.to_nat n in
+  let m := Z.to_nat m in
+  let o := Z.to_nat o in
+  let prf : (o <= m < n)%nat := subrange_lemma0 in
+  let w := get_word v in
+  cast_to_mword (split2 o (m-o+1)
+                        (cast_word (split1 (m+1) (n-(m+1)) (cast_word w (subrange_lemma1 prf)))
+                                   (subrange_lemma2 prf))) subrange_lemma3.
+
+Definition subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <= m)} `{ArithFact (m <= o < n)} : mword (o - m + 1) := autocast (subrange_vec_dec v (n-1-m) (n-1-o)).
+
+(* TODO: get rid of bogus default *)
+Parameter dummy_vector : forall {n} `{ArithFact (n >= 0)}, mword n.
+
+(*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
+Definition update_subrange_vec_inc {a b} (v : mword a) i j (w : mword b) : mword a :=
+  opt_def dummy_vector (of_bits (update_subrange_bv_inc v i j w)).
+
+(*val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
+Definition update_subrange_vec_dec {a b} (v : mword a) i j (w : mword b) : mword a :=
+  opt_def dummy_vector (of_bits (update_subrange_bv_dec v i j w)).
+
+Lemma mword_nonneg {a} : mword a -> a >= 0.
+destruct a;
+auto using Z.le_ge, Zle_0_pos with zarith.
+destruct 1.
+Qed.
+
+(*val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
+Definition extz_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+refine (cast_to_mword (Word.zext (get_word v) (Z.to_nat (b - a))) _).
+unwrap_ArithFacts.
+assert (a >= 0). { apply mword_nonneg. assumption. }
+rewrite <- Z2Nat.inj_add; try omega.
+rewrite Zplus_minus.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
+
+(*val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
+Definition exts_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+refine (cast_to_mword (Word.sext (get_word v) (Z.to_nat (b - a))) _).
+unwrap_ArithFacts.
+assert (a >= 0). { apply mword_nonneg. assumption. }
+rewrite <- Z2Nat.inj_add; try omega.
+rewrite Zplus_minus.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
+
+Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := extz_vec n v.
+
+Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v.
+
+Lemma truncate_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat.
+intros.
+assert ((Z.to_nat m <= Z.to_nat n)%nat).
+{ apply Z2Nat.inj_le; omega. }
+omega.
+Qed.
+
+Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
+  cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+
+Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
+intros.
+rewrite Nat2Z.inj_add.
+rewrite Z2Nat.id; auto with zarith.
+rewrite Z2Nat.id; auto with zarith.
+Qed.
+
+
+(*val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c*)
+Definition concat_vec {a b} (v : mword a) (w : mword b) : mword (a + b) :=
+ cast_to_mword (Word.combine (get_word w) (get_word v)) (ltac:(solve [auto using concat_eq, mword_nonneg with zarith]) : Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b).
+
+(*val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b*)
+(*Definition cons_vec {a b} : bitU -> mword a -> mword b := cons_bv.*)
+
+(*val bool_of_vec : mword ty1 -> bitU
+Definition bool_of_vec := bool_of_bv
+
+val cast_unit_vec : bitU -> mword ty1
+Definition cast_unit_vec := cast_unit_bv
+
+val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
+Definition vec_of_bit := bv_of_bit*)
+
+Require Import bbv.NatLib.
+
+Lemma Npow2_pow {n} : (2 ^ (N.of_nat n) = Npow2 n)%N.
+induction n.
+* reflexivity.
+* rewrite Nnat.Nat2N.inj_succ.
+  rewrite N.pow_succ_r'.
+  rewrite IHn.
+  rewrite Npow2_S.
+  rewrite Word.Nmul_two.
+  reflexivity.
+Qed.
+
+Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <= z /\ z <= 2 ^ a - 1)} :=
+ existT _ (Z.of_N (Word.wordToN (get_word x))) _.
+Next Obligation.
+constructor.
+constructor.
+* apply N2Z.is_nonneg.
+* assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). {
+    rewrite N2Z.inj_sub.
+    * rewrite N2Z.inj_pow.
+      rewrite Z2N.id; auto.
+      destruct a; auto with zarith. destruct x.
+    * apply N.le_trans with (m := (2^0)%N); auto using N.le_refl.
+      apply N.pow_le_mono_r.
+      inversion 1.
+      apply N.le_0_l.
+  }
+  rewrite H.
+  apply N2Z.inj_le.
+  rewrite N.sub_1_r.
+  apply N.lt_le_pred.
+  rewrite <- Z_nat_N.
+  rewrite Npow2_pow.
+  apply Word.wordToN_bound.
+Defined.
+
+Lemma Zpow_pow2 {n} : 2 ^ Z.of_nat n = Z.of_nat (pow2 n).
+induction n.
+* reflexivity.
+* rewrite pow2_S_z.
+  rewrite Nat2Z.inj_succ.
+  rewrite Z.pow_succ_r; auto with zarith.
+Qed.
+
+Program Definition sint {a} `{ArithFact (a > 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <= z /\ z <= 2 ^ (a-1) - 1)} :=
+  existT _ (Word.wordToZ (get_word x)) _.
+Next Obligation.
+destruct H.
+destruct a; try inversion fact.
+constructor.
+generalize (get_word x).
+rewrite <- positive_nat_Z.
+destruct (Pos2Nat.is_succ p) as [n eq].
+rewrite eq.
+rewrite Nat2Z.id.
+intro w.
+destruct (Word.wordToZ_size' w) as [LO HI].
+replace 1 with (Z.of_nat 1); auto.
+rewrite <- Nat2Z.inj_sub; auto with arith.
+simpl.
+rewrite <- minus_n_O.
+rewrite Zpow_pow2.
+rewrite Z.sub_1_r.
+rewrite <- Z.lt_le_pred.
+auto.
+Defined.
+
+Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0.
+unfold length_list.
+auto with zarith.
+Qed.
+Hint Resolve length_list_pos : sail.
+
+Definition vec_of_bits (l:list bitU) : mword (length_list l) := opt_def dummy_vector (of_bits l).
+(*
+
+val msb : forall 'a. Size 'a => mword 'a -> bitU
+Definition msb := most_significant
+
+val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
+Definition int_of_vec := int_of_bv
+
+val string_of_vec : forall 'a. Size 'a => mword 'a -> string*)
+Definition string_of_bits {n} (w : mword n) : string := string_of_bv w.
+Definition with_word' {n} (P : Type -> Type) : (forall n, Word.word n -> P (Word.word n)) -> mword n -> P (mword n) := fun f w => @with_word n _ (f (Z.to_nat n)) w.
+Definition word_binop {n} (f : forall n, Word.word n -> Word.word n -> Word.word n) : mword n -> mword n -> mword n := with_word' (fun x => x -> x) f.
+Definition word_unop {n} (f : forall n, Word.word n -> Word.word n) : mword n -> mword n := with_word' (fun x => x) f.
+
+
+(*
+val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a*)
+Definition and_vec {n} : mword n -> mword n -> mword n := word_binop Word.wand.
+Definition or_vec  {n} : mword n -> mword n -> mword n := word_binop Word.wor.
+Definition xor_vec {n} : mword n -> mword n -> mword n := word_binop Word.wxor.
+Definition not_vec {n} : mword n -> mword n := word_unop Word.wnot.
+
+(*val add_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val sadd_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val sub_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val mult_vec  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b*)
+Definition add_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wplus.
+(*Definition sadd_vec  {n} : mword n -> mword n -> mword n := sadd_bv w.*)
+Definition sub_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wminus.
+Definition mult_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+  word_binop Word.wmult (zero_extend l _) (zero_extend r _).
+Definition mults_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+  word_binop Word.wmult (sign_extend l _) (sign_extend r _).
+
+(*val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sadd_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+val smult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
+Definition add_vec_int   {a} (l : mword a) (r : Z) : mword a := arith_op_bv_int Z.add   false l r.
+Definition sadd_vec_int  {a} (l : mword a) (r : Z) : mword a := arith_op_bv_int Z.add   true  l r.
+Definition sub_vec_int   {a} (l : mword a) (r : Z) : mword a := arith_op_bv_int Z.sub   false l r.
+(*Definition mult_vec_int  {a b} : mword a -> Z -> mword b := mult_bv_int.
+Definition smult_vec_int {a b} : mword a -> Z -> mword b := smult_bv_int.*)
+
+(*val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sadd_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+val smult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+Definition add_int_vec   := add_int_bv
+Definition sadd_int_vec  := sadd_int_bv
+Definition sub_int_vec   := sub_int_bv
+Definition mult_int_vec  := mult_int_bv
+Definition smult_int_vec := smult_int_bv
+
+val add_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val sadd_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val sub_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+Definition add_vec_bit  := add_bv_bit
+Definition sadd_vec_bit := sadd_bv_bit
+Definition sub_vec_bit  := sub_bv_bit
+
+val add_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val add_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+Definition add_overflow_vec         := add_overflow_bv
+Definition add_overflow_vec_signed  := add_overflow_bv_signed
+Definition sub_overflow_vec         := sub_overflow_bv
+Definition sub_overflow_vec_signed  := sub_overflow_bv_signed
+Definition mult_overflow_vec        := mult_overflow_bv
+Definition mult_overflow_vec_signed := mult_overflow_bv_signed
+
+val add_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val add_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+Definition add_overflow_vec_bit         := add_overflow_bv_bit
+Definition add_overflow_vec_bit_signed  := add_overflow_bv_bit_signed
+Definition sub_overflow_vec_bit         := sub_overflow_bv_bit
+Definition sub_overflow_vec_bit_signed  := sub_overflow_bv_bit_signed
+
+val shiftl       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val shiftr       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(* TODO: check/redefine behaviour on out-of-range n *)
+Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v.
+Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v.
+Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v.
+(*
+Definition rotl         := rotl_bv
+Definition rotr         := rotr_bv
+
+val mod_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+Definition mod_vec         := mod_bv
+Definition quot_vec        := quot_bv
+Definition quot_vec_signed := quot_bv_signed
+
+val mod_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+Definition mod_vec_int  := mod_bv_int
+Definition quot_vec_int := quot_bv_int
+
+val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
+Fixpoint replicate_bits_aux {a} (w : Word.word a) (n : nat) : Word.word (n * a) :=
+match n with
+| O => Word.WO
+| S m => Word.combine w (replicate_bits_aux w m)
+end.
+Lemma replicate_ok {n a} `{ArithFact (n >= 0)} `{ArithFact (a >= 0)} :
+   Z.of_nat (Z.to_nat n * Z.to_nat a) = a * n.
+destruct H. destruct H0.
+rewrite <- Z2Nat.id; auto with zarith.
+rewrite Z2Nat.inj_mul; auto with zarith.
+rewrite Nat.mul_comm. reflexivity.
+Qed.
+Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (a * n) :=
+ cast_to_mword (replicate_bits_aux (get_word w) (Z.to_nat n)) replicate_ok.
+
+(*val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
+Definition duplicate := duplicate_bit_bv
+
+val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool*)
+Definition eq_vec  {n} (x : mword n) (y : mword n) : bool := Word.weqb (get_word x) (get_word y).
+Definition neq_vec {n} (x : mword n) (y : mword n) : bool := negb (eq_vec x y).
+(*Definition ult_vec   := ult_bv.
+Definition slt_vec   := slt_bv.
+Definition ugt_vec   := ugt_bv.
+Definition sgt_vec   := sgt_bv.
+Definition ulteq_vec := ulteq_bv.
+Definition slteq_vec := slteq_bv.
+Definition ugteq_vec := ugteq_bv.
+Definition sgteq_vec := sgteq_bv.
+
+*)
+
+Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
+  match n with
+  | S (S (S (S (S (S (S (S m))))))) =>
+    combine
+      (reverse_endianness_word (split2 8 m bits))
+      (split1 8 m bits)
+  | _ => bits
+  end.
+Next Obligation.
+omega.
+Qed.
+
+Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits.
+
+Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
diff --git a/snapshots/coq/lib/coq/Sail2_prompt.v b/snapshots/coq/lib/coq/Sail2_prompt.v
new file mode 100644
index 00000000..ab7d5bac
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_prompt.v
@@ -0,0 +1,122 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+(*Require Import Sail_impl_base*)
+Require Import Sail2_values.
+Require Import Sail2_prompt_monad.
+
+Require Import List.
+Import ListNotations.
+(*
+
+val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
+let rec iter_aux i f xs = match xs with
+  | x :: xs -> f i x >> iter_aux (i + 1) f xs
+  | [] -> return ()
+  end
+
+declare {isabelle} termination_argument iter_aux = automatic
+
+val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
+let iteri f xs = iter_aux 0 f xs
+
+val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
+let iter f xs = iteri (fun _ x -> f x) xs
+
+val foreachM : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
+Fixpoint foreachM {a rv Vars e} (l : list a) (vars : Vars) (body : a -> Vars -> monad rv Vars e) : monad rv Vars e :=
+match l with
+| [] => returnm vars
+| (x :: xs) =>
+  body x vars >>= fun vars =>
+  foreachM xs vars body
+end.
+
+Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+  if sumbool_of_bool (from + off <=? to) then
+    match n with
+    | O => returnm vars
+    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' from to step (off + step) n vars body
+    end
+  else returnm vars.
+
+Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+  if sumbool_of_bool (to <=? from + off) then
+    match n with
+    | O => returnm vars
+    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' from to step (off - step) n vars body
+    end
+  else returnm vars.
+
+Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} :=
+    foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} :=
+    foreach_ZM_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+
+(*declare {isabelle} termination_argument foreachM = automatic*)
+
+(*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
+Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
+ l >>= (fun l => if l then r else returnm false).
+
+(*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
+Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
+ l >>= (fun l => if l then returnm true else r).
+
+(*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
+Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
+match b with
+  | B0 => returnm false
+  | B1 => returnm true
+  | BU => Fail "bool_of_bitU"
+end.
+
+(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
+Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E :=
+match b with
+  | B0 => returnm false
+  | B1 => returnm true
+  | BU => undefined_bool tt
+end.
+
+
+(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
+let rec whileM vars cond body =
+  cond vars >>= fun cond_val ->
+  if cond_val then
+    body vars >>= fun vars -> whileM vars cond body
+  else return vars
+
+val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
+let rec untilM vars cond body =
+  body vars >>= fun vars ->
+  cond vars >>= fun cond_val ->
+  if cond_val then return vars else untilM vars cond body
+
+(*let write_two_regs r1 r2 vec =
+  let is_inc =
+    let is_inc_r1 = is_inc_of_reg r1 in
+    let is_inc_r2 = is_inc_of_reg r2 in
+    let () = ensure (is_inc_r1 = is_inc_r2)
+                    "write_two_regs called with vectors of different direction" in
+    is_inc_r1 in
+
+  let (size_r1 : integer) = size_of_reg r1 in
+  let (start_vec : integer) = get_start vec in
+  let size_vec = length vec in
+  let r1_v =
+    if is_inc
+    then slice vec start_vec (size_r1 - start_vec - 1)
+    else slice vec start_vec (start_vec - size_r1 - 1) in
+  let r2_v =
+    if is_inc
+    then slice vec (size_r1 - start_vec) (size_vec - start_vec)
+    else slice vec (start_vec - size_r1) (start_vec - size_vec) in
+  write_reg r1 r1_v >> write_reg r2 r2_v*)
+
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_prompt_monad.v b/snapshots/coq/lib/coq/Sail2_prompt_monad.v
new file mode 100644
index 00000000..43e873f7
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_prompt_monad.v
@@ -0,0 +1,252 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import String.
+(*Require Import Sail_impl_base*)
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
+
+
+
+Definition register_name := string.
+Definition address := list bitU.
+
+Inductive monad regval a e :=
+  | Done : a -> monad regval a e
+  (* Read a number : bytes from memory, returned in little endian order *)
+  | Read_mem : read_kind -> address -> nat -> (list memory_byte -> monad regval a e) -> monad regval a e
+  (* Read the tag : a memory address *)
+  | Read_tag : address -> (bitU -> monad regval a e) -> monad regval a e
+  (* Tell the system a write is imminent, at address lifted, : size nat *)
+  | Write_ea : write_kind -> address -> nat -> monad regval a e -> monad regval a e
+  (* Request the result : store-exclusive *)
+  | Excl_res : (bool -> monad regval a e) -> monad regval a e
+  (* Request to write memory at last signalled address. Memory value should be 8
+     times the size given in ea signal, given in little endian order *)
+  | Write_memv : list memory_byte -> (bool -> monad regval a e) -> monad regval a e
+  (* Request to write the tag at last signalled address. *)
+  | Write_tag : address -> bitU -> (bool -> monad regval a e) -> monad regval a e
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint : monad regval a e -> monad regval a e
+  (* Request a memory barrier *)
+  | Barrier : barrier_kind -> monad regval a e -> monad regval a e
+  (* Request to read register, will track dependency when mode.track_values *)
+  | Read_reg : register_name -> (regval -> monad regval a e) -> monad regval a e
+  (* Request to write register *)
+  | Write_reg : register_name -> regval -> monad regval a e -> monad regval a e
+  | Undefined : (bool -> monad regval a e) -> monad regval a e
+  (*Result : a failed assert with possible error message to report*)
+  | Fail : string -> monad regval a e
+  | Error : string -> monad regval a e
+  (* Exception : type e *)
+  | Exception : e -> monad regval a e.
+  (* TODO: Reading/writing tags *)
+
+Arguments Done [_ _ _].
+Arguments Read_mem [_ _ _].
+Arguments Read_tag [_ _ _].
+Arguments Write_ea [_ _ _].
+Arguments Excl_res [_ _ _].
+Arguments Write_memv [_ _ _].
+Arguments Write_tag [_ _ _].
+Arguments Footprint [_ _ _].
+Arguments Barrier [_ _ _].
+Arguments Read_reg [_ _ _].
+Arguments Write_reg [_ _ _].
+Arguments Undefined [_ _ _].
+Arguments Fail [_ _ _].
+Arguments Error [_ _ _].
+Arguments Exception [_ _ _].
+
+(*val return : forall rv a e. a -> monad rv a e*)
+Definition returnm {rv A E} (a : A) : monad rv A E := Done a.
+
+(*val bind : forall rv a b e. monad rv a e -> (a -> monad rv b e) -> monad rv b e*)
+Fixpoint bind {rv A B E} (m : monad rv A E) (f : A -> monad rv B E) := match m with
+  | Done a => f a
+  | Read_mem rk a sz k => Read_mem rk a sz (fun v => bind (k v) f)
+  | Read_tag a k =>       Read_tag a       (fun v => bind (k v) f)
+  | Write_memv descr k => Write_memv descr (fun v => bind (k v) f)
+  | Write_tag a t k =>    Write_tag a t    (fun v => bind (k v) f)
+  | Read_reg descr k =>   Read_reg descr   (fun v => bind (k v) f)
+  | Excl_res k =>         Excl_res         (fun v => bind (k v) f)
+  | Undefined k =>        Undefined        (fun v => bind (k v) f)
+  | Write_ea wk a sz k => Write_ea wk a sz (bind k f)
+  | Footprint k =>        Footprint        (bind k f)
+  | Barrier bk k =>       Barrier bk       (bind k f)
+  | Write_reg r v k =>    Write_reg r v    (bind k f)
+  | Fail descr =>         Fail descr
+  | Error descr =>        Error descr
+  | Exception e =>        Exception e
+end.
+
+Notation "m >>= f" := (bind m f) (at level 50, left associativity).
+(*val (>>) : forall rv b e. monad rv unit e -> monad rv b e -> monad rv b e*)
+Definition bind0 {rv A E} (m : monad rv unit E) (n : monad rv A E) :=
+  m >>= fun (_ : unit) => n.
+Notation "m >> n" := (bind0 m n) (at level 50, left associativity).
+
+(*val exit : forall rv a e. unit -> monad rv a e*)
+Definition exit {rv A E} (_ : unit) : monad rv A E := Fail "exit".
+
+(*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
+Definition undefined_bool {rv e} (_:unit) : monad rv bool e := Undefined returnm.
+
+(*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
+Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
+ if exp then Done tt else Fail msg.
+
+Definition assert_exp' {rv E} (exp :bool) msg : monad rv (exp = true) E :=
+ if exp return monad rv (exp = true) E then Done eq_refl else Fail msg.
+Definition bindH {rv A P E} (m : monad rv P E) (n : monad rv A E) :=
+  m >>= fun (H : P) => n.
+Notation "m >>> n" := (bindH m n) (at level 50, left associativity).
+
+(*val throw : forall rv a e. e -> monad rv a e*)
+Definition throw {rv A E} e : monad rv A E := Exception e.
+
+(*val try_catch : forall rv a e1 e2. monad rv a e1 -> (e1 -> monad rv a e2) -> monad rv a e2*)
+Fixpoint try_catch {rv A E1 E2} (m : monad rv A E1) (h : E1 -> monad rv A E2) := match m with
+  | Done a =>             Done a
+  | Read_mem rk a sz k => Read_mem rk a sz (fun v => try_catch (k v) h)
+  | Read_tag a k =>       Read_tag a       (fun v => try_catch (k v) h)
+  | Write_memv descr k => Write_memv descr (fun v => try_catch (k v) h)
+  | Write_tag a t k =>    Write_tag a t     (fun v => try_catch (k v) h)
+  | Read_reg descr k =>   Read_reg descr   (fun v => try_catch (k v) h)
+  | Excl_res k =>         Excl_res         (fun v => try_catch (k v) h)
+  | Undefined k =>        Undefined        (fun v => try_catch (k v) h)
+  | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h)
+  | Footprint k =>        Footprint        (try_catch k h)
+  | Barrier bk k =>       Barrier bk       (try_catch k h)
+  | Write_reg r v k =>    Write_reg r v    (try_catch k h)
+  | Fail descr =>         Fail descr
+  | Error descr =>        Error descr
+  | Exception e =>        h e
+end.
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "either r e", where "inr e"
+   represents a proper exception and "inl r" an early return : value "r". *)
+Definition monadR rv a r e := monad rv a (sum r e).
+
+(*val early_return : forall rv a r e. r -> monadR rv a r e*)
+Definition early_return {rv A R E} (r : R) : monadR rv A R E := throw (inl r).
+
+(*val catch_early_return : forall rv a e. monadR rv a a e -> monad rv a e*)
+Definition catch_early_return {rv A E} (m : monadR rv A A E) :=
+  try_catch m
+    (fun r => match r with
+      | inl a => returnm a
+      | inr e => throw e
+     end).
+
+(* Lift to monad with early return by wrapping exceptions *)
+(*val liftR : forall rv a r e. monad rv a e -> monadR rv a r e*)
+Definition liftR {rv A R E} (m : monad rv A E) : monadR rv A R E :=
+ try_catch m (fun e => throw (inr e)).
+
+(* Catch exceptions in the presence : early returns *)
+(*val try_catchR : forall rv a r e1 e2. monadR rv a r e1 -> (e1 -> monadR rv a r e2) ->  monadR rv a r e2*)
+Definition try_catchR {rv A R E1 E2} (m : monadR rv A R E1) (h : E1 -> monadR rv A R E2) :=
+  try_catch m
+    (fun r => match r with
+      | inl r => throw (inl r)
+      | inr e => h e
+     end).
+
+(*val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e*)
+Definition maybe_fail {rv A E} msg (x : option A) : monad rv A E :=
+match x with
+  | Some a => returnm a
+  | None => Fail msg
+end.
+
+(*val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e*)
+Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte) E :=
+  Read_mem rk (bits_of addr) (Z.to_nat sz) returnm.
+
+(*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*)
+Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B) E :=
+  bind
+    (read_mem_bytes rk addr sz)
+    (fun bytes =>
+       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))).
+
+(*val read_tag : forall rv a e. Bitvector a => a -> monad rv bitU e*)
+Definition read_tag {rv a e} `{Bitvector a} (addr : a) : monad rv bitU e :=
+ Read_tag (bits_of addr) returnm.
+
+(*val excl_result : forall rv e. unit -> monad rv bool e*)
+Definition excl_result {rv e} (_:unit) : monad rv bool e :=
+  let k successful := (returnm successful) in
+  Excl_res k.
+
+Definition write_mem_ea {rv a E} `{Bitvector a} wk (addr: a) sz : monad rv unit E :=
+ Write_ea wk (bits_of addr) (Z.to_nat sz) (Done tt).
+
+Definition write_mem_val {rv a e} `{Bitvector a} (v : a) : monad rv bool e := match mem_bytes_of_bits v with
+  | Some v => Write_memv v returnm
+  | None => Fail "write_mem_val"
+end.
+
+(*val write_tag : forall rv a e. Bitvector 'a => 'a -> bitU -> monad rv bool e*)
+Definition write_tag {rv a e} (addr : mword a) (b : bitU) : monad rv bool e := Write_tag (bits_of addr) b returnm.
+
+Definition read_reg {s rv a e} (reg : register_ref s rv a) : monad rv a e :=
+  let k v :=
+    match reg.(of_regval) v with
+      | Some v => Done v
+      | None => Error "read_reg: unrecognised value"
+    end
+  in
+  Read_reg reg.(name) k.
+
+(* TODO
+val read_reg_range : forall s r rv a e. Bitvector a => register_ref s rv r -> integer -> integer -> monad rv a e
+Definition read_reg_range reg i j :=
+  read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
+
+Definition read_reg_bit reg i :=
+  read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
+  returnm (extract_only_element v)
+
+Definition read_reg_field reg regfield :=
+  read_reg_aux (external_reg_field_whole reg regfield)
+
+Definition read_reg_bitfield reg regfield :=
+  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
+  returnm (extract_only_element v)*)
+
+Definition reg_deref {s rv a e} := @read_reg s rv a e.
+
+(*Parameter write_reg : forall {s rv a e}, register_ref s rv a -> a -> monad rv unit e.*)
+Definition write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e :=
+ Write_reg reg.(name) (reg.(regval_of) v) (Done tt).
+
+(* TODO
+Definition write_reg reg v :=
+  write_reg_aux (external_reg_whole reg) v
+Definition write_reg_range reg i j v :=
+  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
+Definition write_reg_pos reg i v :=
+  let iN := natFromInteger i in
+  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
+Definition write_reg_bit := write_reg_pos
+Definition write_reg_field reg regfield v :=
+  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
+Definition write_reg_field_bit reg regfield bit :=
+  write_reg_aux (external_reg_field_whole reg regfield.field_name)
+                (Vector [bit] 0 (is_inc_of_reg reg))
+Definition write_reg_field_range reg regfield i j v :=
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
+Definition write_reg_field_pos reg regfield i v :=
+  write_reg_field_range reg regfield i i [v]
+Definition write_reg_field_bit := write_reg_field_pos*)
+
+(*val barrier : forall rv e. barrier_kind -> monad rv unit e*)
+Definition barrier {rv e} bk : monad rv unit e := Barrier bk (Done tt).
+
+(*val footprint : forall rv e. unit -> monad rv unit e*)
+Definition footprint {rv e} (_ : unit) : monad rv unit e := Footprint (Done tt).
diff --git a/snapshots/coq/lib/coq/Sail2_state.v b/snapshots/coq/lib/coq/Sail2_state.v
new file mode 100644
index 00000000..404309e0
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_state.v
@@ -0,0 +1,74 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+(*Require Import Sail_impl_base*)
+Require Import Sail2_values.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+Require Import Sail2_state_monad.
+(*
+(* State monad wrapper around prompt monad *)
+
+val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
+let rec liftState ra s = match s with
+  | (Done a)             -> returnS a
+  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
+  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
+  | (Write_tagv t k)     -> bindS (write_tagS t)            (fun v -> liftState ra (k v))
+  | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
+  | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
+  | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
+  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
+  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
+  | (Footprint k)        -> liftState ra k
+  | (Barrier _ k)        -> liftState ra k
+  | (Fail descr)         -> failS descr
+  | (Error descr)        -> failS descr
+  | (Exception e)        -> throwS e
+end
+
+
+val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let rec iterS_aux i f xs = match xs with
+  | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
+  | [] -> returnS ()
+  end
+
+declare {isabelle} termination_argument iterS_aux = automatic
+
+val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let iteriS f xs = iterS_aux 0 f xs
+
+val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let iterS f xs = iteriS (fun _ x -> f x) xs
+
+val foreachS : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec foreachS xs vars body = match xs with
+  | [] -> returnS vars
+  | x :: xs ->
+     body x vars >>$= fun vars ->
+     foreachS xs vars body
+end
+
+declare {isabelle} termination_argument foreachS = automatic
+
+
+val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec whileS vars cond body s =
+  (cond vars >>$= (fun cond_val s' ->
+  if cond_val then
+    (body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s'
+  else returnS vars s')) s
+
+val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec untilS vars cond body s =
+  (body vars >>$= (fun vars s' ->
+  (cond vars >>$= (fun cond_val s'' ->
+  if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_state_monad.v b/snapshots/coq/lib/coq/Sail2_state_monad.v
new file mode 100644
index 00000000..5258c37a
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_state_monad.v
@@ -0,0 +1,258 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
+(*
+(* 'a is result type *)
+
+type memstate = map integer memory_byte
+type tagstate = map integer bitU
+(* type regstate = map string (vector bitU) *)
+
+type sequential_state 'regs =
+  <| regstate : 'regs;
+     memstate : memstate;
+     tagstate : tagstate;
+     write_ea : maybe (write_kind * integer * integer);
+     last_exclusive_operation_was_load : bool|>
+
+val init_state : forall 'regs. 'regs -> sequential_state 'regs
+let init_state regs =
+  <| regstate = regs;
+     memstate = Map.empty;
+     tagstate = Map.empty;
+     write_ea = Nothing;
+     last_exclusive_operation_was_load = false |>
+
+type ex 'e =
+  | Failure of string
+  | Throw of 'e
+
+type result 'a 'e =
+  | Value of 'a
+  | Ex of (ex 'e)
+
+(* State, nondeterminism and exception monad with result value type 'a
+   and exception type 'e. *)
+type monadS 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs)
+
+val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e
+let returnS a s = [(Value a,s)]
+
+val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e
+let bindS m f (s : sequential_state 'regs) =
+  List.concatMap (function
+                  | (Value a, s') -> f a s'
+                  | (Ex e, s') -> [(Ex e, s')]
+                  end) (m s)
+
+val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
+let seqS m n = bindS m (fun (_ : unit) -> n)
+
+let inline (>>$=) = bindS
+let inline (>>$) = seqS
+
+val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = List.map (fun x -> (Value x, s)) xs
+
+val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
+let readS f = (fun s -> returnS (f s) s)
+
+val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
+let updateS f = (fun s -> returnS () (f s))
+
+val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
+let failS msg s = [(Ex (Failure msg), s)]
+
+val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
+let exitS () = failS "exit"
+
+val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
+let throwS e s = [(Ex (Throw e), s)]
+
+val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2
+let try_catchS m h s =
+  List.concatMap (function
+                  | (Value a, s') -> returnS a s'
+                  | (Ex (Throw e), s') -> h e s'
+                  | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')]
+                  end) (m s)
+
+val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e
+let assert_expS exp msg = if exp then returnS () else failS msg
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "either 'r 'e", where "Right e"
+   represents a proper exception and "Left r" an early return of value "r". *)
+type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+let early_returnS r = throwS (Left r)
+
+val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+let catch_early_returnS m =
+  try_catchS m
+    (function
+      | Left a -> returnS a
+      | Right e -> throwS e
+     end)
+
+(* Lift to monad with early return by wrapping exceptions *)
+val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
+let liftSR m = try_catchS m (fun e -> throwS (Right e))
+
+(* Catch exceptions in the presence of early returns *)
+val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) ->  monadSR 'regs 'a 'r 'e2
+let try_catchSR m h =
+  try_catchS m
+    (function
+      | Left r -> throwS (Left r)
+      | Right e -> h e
+     end)
+
+val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
+let read_tagS addr =
+  readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate))
+
+(* Read bytes from memory and return in little endian order *)
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS read_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  let addrs = index_list addr (addr+sz-1) 1 in
+  let read_byte s addr = Map.lookup addr s.memstate in
+  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
+    | Just mem_val ->
+       updateS (fun s ->
+         if read_is_exclusive read_kind
+         then <| s with last_exclusive_operation_was_load = true |>
+         else s) >>$
+       returnS mem_val
+    | Nothing -> failS "read_memS"
+  end)
+
+val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+let read_memS rk a sz =
+  read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes ->
+  returnS (bits_of_mem_bytes bytes))
+
+val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
+let excl_resultS () =
+  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
+  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
+  chooseS (if excl_load then [false; true] else [false]))
+
+val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
+let write_mem_eaS write_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)
+
+(* Write little-endian list of bytes to previously announced address *)
+val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS v =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, sz) ->
+         let addrs = index_list addr (addr+sz-1) 1 in
+         (*let v = external_mem_value (bits_of v) in*)
+         let a_v = List.zip addrs v in
+         let write_byte mem (addr, v) = Map.insert addr v mem in
+         updateS (fun s ->
+           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
+         returnS true
+    end)
+
+val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
+let write_mem_valS v = match mem_bytes_of_bits v with
+  | Just v -> write_mem_bytesS v
+  | Nothing -> failS "write_mem_val"
+end
+
+val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e
+let write_tagS t =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, _) ->
+         (*let taddr = addr / cap_alignment in*)
+         updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
+         returnS true
+    end)
+
+val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
+let read_regS reg = readS (fun s -> reg.read_from s.regstate)
+
+(* TODO
+let read_reg_range reg i j state =
+  let v = slice (get_reg state (name_of_reg reg)) i j in
+  [(Value (vec_to_bvec v),state)]
+let read_reg_bit reg i state =
+  let v = access (get_reg state (name_of_reg reg)) i in
+  [(Value v,state)]
+let read_reg_field reg regfield =
+  let (i,j) = register_field_indices reg regfield in
+  read_reg_range reg i j
+let read_reg_bitfield reg regfield =
+  let (i,_) = register_field_indices reg regfield in
+  read_reg_bit reg i *)
+
+val read_regvalS : forall 'regs 'rv 'e.
+  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
+let read_regvalS (read, _) reg =
+  readS (fun s -> read reg s.regstate) >>$= (function
+      | Just v ->  returnS v
+      | Nothing -> failS ("read_regvalS " ^ reg)
+    end)
+
+val write_regvalS : forall 'regs 'rv 'e.
+  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
+let write_regvalS (_, write) reg v =
+  readS (fun s -> write reg v s.regstate) >>$= (function
+      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
+      | Nothing ->  failS ("write_regvalS " ^ reg)
+    end)
+
+val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
+let write_regS reg v =
+  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
+
+(* TODO
+val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
+let update_reg reg f v state =
+  let current_value = get_reg state reg in
+  let new_value = f current_value v in
+  [(Value (), set_reg state reg new_value)]
+
+let write_reg_field reg regfield = update_reg reg regfield.set_field
+
+val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
+let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val)
+let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
+
+let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x
+let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
+
+let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit)
+let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
+
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
+
+let update_reg_field_pos regfield i reg_val x =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update_list regfield.field_is_inc current_field_value i x in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
+
+let update_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
+*)
diff --git a/snapshots/coq/lib/coq/Sail2_values.v b/snapshots/coq/lib/coq/Sail2_values.v
new file mode 100644
index 00000000..f1f5f1de
--- /dev/null
+++ b/snapshots/coq/lib/coq/Sail2_values.v
@@ -0,0 +1,1576 @@
+(*========================================================================*)
+(*  Copyright (c) 2018 Sail contributors.                                 *)
+(*  This material is provided for anonymous review purposes only.         *)
+(*========================================================================*)
+
+(* Version of sail_values.lem that uses Lems machine words library *)
+
+(*Require Import Sail_impl_base*)
+Require Export ZArith.
+Require Import Ascii.
+Require Export String.
+Require Import bbv.Word.
+Require Export List.
+Require Export Sumbool.
+Require Export DecidableClass.
+Import ListNotations.
+
+Open Scope Z.
+
+(* Constraint solving basics.  A HintDb which unfolding hints and lemmata
+   can be added to, and a typeclass to wrap constraint arguments in to
+   trigger automatic solving. *)
+Create HintDb sail.
+Class ArithFact (P : Prop) := { fact : P }.
+Lemma use_ArithFact {P} `(ArithFact P) : P.
+apply fact.
+Defined.
+
+Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
+  existT _ n H.
+
+Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
+Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
+Lemma generic_eq_true {T} {x y:T} `{Decidable (x = y)} : generic_eq x y = true -> x = y.
+apply Decidable_spec.
+Qed.
+Lemma generic_eq_false {T} {x y:T} `{Decidable (x = y)} : generic_eq x y = false -> x <> y.
+unfold generic_eq.
+intros H1 H2.
+rewrite <- Decidable_spec in H2.
+congruence.
+Qed.
+Lemma generic_neq_true {T} {x y:T} `{Decidable (x = y)} : generic_neq x y = true -> x <> y.
+unfold generic_neq.
+intros H1 H2.
+rewrite <- Decidable_spec in H2.
+destruct Decidable_witness; simpl in *; 
+congruence.
+Qed.
+Lemma generic_neq_false {T} {x y:T} `{Decidable (x = y)} : generic_neq x y = false -> x = y.
+unfold generic_neq.
+intro H1.
+rewrite <- Decidable_spec.
+destruct Decidable_witness; simpl in *; 
+congruence.
+Qed.
+Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> y}) : 
+  forall (x y : T), Decidable (eq x y) := {
+  Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y))
+}.
+destruct (eqdec x y); simpl; split; congruence.
+Qed.
+
+
+(* Project away range constraints in comparisons *)
+Definition ltb_range_l {P} (l : sigT P) r := Z.ltb (projT1 l) r.
+Definition leb_range_l {P} (l : sigT P) r := Z.leb (projT1 l) r.
+Definition gtb_range_l {P} (l : sigT P) r := Z.gtb (projT1 l) r.
+Definition geb_range_l {P} (l : sigT P) r := Z.geb (projT1 l) r.
+Definition ltb_range_r {P} l (r : sigT P) := Z.ltb l (projT1 r).
+Definition leb_range_r {P} l (r : sigT P) := Z.leb l (projT1 r).
+Definition gtb_range_r {P} l (r : sigT P) := Z.gtb l (projT1 r).
+Definition geb_range_r {P} l (r : sigT P) := Z.geb l (projT1 r).
+
+Definition ii := Z.
+Definition nn := nat.
+
+(*val pow : Z -> Z -> Z*)
+Definition pow m n := m ^ n.
+
+Definition pow2 n := pow 2 n.
+(*
+Definition inline lt := (<)
+Definition inline gt := (>)
+Definition inline lteq := (<=)
+Definition inline gteq := (>=)
+
+val eq : forall a. Eq a => a -> a -> bool
+Definition inline eq l r := (l = r)
+
+val neq : forall a. Eq a => a -> a -> bool*)
+Definition neq l r := (negb (l =? r)). (* Z only *)
+
+(*let add_int l r := integerAdd l r
+Definition add_signed l r := integerAdd l r
+Definition sub_int l r := integerMinus l r
+Definition mult_int l r := integerMult l r
+Definition div_int l r := integerDiv l r
+Definition div_nat l r := natDiv l r
+Definition power_int_nat l r := integerPow l r
+Definition power_int_int l r := integerPow l (Z.to_nat r)
+Definition negate_int i := integerNegate i
+Definition min_int l r := integerMin l r
+Definition max_int l r := integerMax l r
+
+Definition add_real l r := realAdd l r
+Definition sub_real l r := realMinus l r
+Definition mult_real l r := realMult l r
+Definition div_real l r := realDiv l r
+Definition negate_real r := realNegate r
+Definition abs_real r := realAbs r
+Definition power_real b e := realPowInteger b e*)
+
+Definition print_int (_ : string) (_ : Z) : unit := tt.
+
+(*
+Definition or_bool l r := (l || r)
+Definition and_bool l r := (l && r)
+Definition xor_bool l r := xor l r
+*)
+Definition append_list {A:Type} (l : list A) r := l ++ r.
+Definition length_list {A:Type} (xs : list A) := Z.of_nat (List.length xs).
+Definition take_list {A:Type} n (xs : list A) := firstn (Z.to_nat n) xs.
+Definition drop_list {A:Type} n (xs : list A) := skipn (Z.to_nat n) xs.
+(*
+val repeat : forall a. list a -> Z -> list a*)
+Fixpoint repeat' {a} (xs : list a) n :=
+  match n with
+  | O => []
+  | S n => xs ++ repeat' xs n
+  end.
+Lemma repeat'_length {a} {xs : list a} {n : nat} : List.length (repeat' xs n) = (n * List.length xs)%nat.
+induction n.
+* reflexivity.
+* simpl.
+  rewrite app_length.
+  auto with arith.
+Qed.
+Definition repeat {a} (xs : list a) (n : Z) :=
+  if n <=? 0 then []
+  else repeat' xs (Z.to_nat n).
+Lemma repeat_length {a} {xs : list a} {n : Z} (H : n >= 0) : length_list (repeat xs n) = n * length_list xs.
+unfold length_list, repeat.
+destruct n.
++ reflexivity. 
++ simpl (List.length _).
+  rewrite repeat'_length.
+  rewrite Nat2Z.inj_mul.
+  rewrite positive_nat_Z.
+  reflexivity.  
++ exfalso.
+  auto with zarith.
+Qed.
+
+(*declare {isabelle} termination_argument repeat = automatic
+
+Definition duplicate_to_list bit length := repeat [bit] length
+
+Fixpoint replace bs (n : Z) b' := match bs with
+  | [] => []
+  | b :: bs =>
+     if n = 0 then b' :: bs
+              else b :: replace bs (n - 1) b'
+  end
+declare {isabelle} termination_argument replace = automatic
+
+Definition upper n := n
+
+(* Modulus operation corresponding to quot below -- result
+   has sign of dividend. *)
+Definition hardware_mod (a: Z) (b:Z) : Z :=
+  let m := (abs a) mod (abs b) in
+  if a < 0 then ~m else m
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+Definition hardware_quot (a:Z) (b:Z) : Z :=
+  let q := (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
+
+Definition max_64u := (integerPow 2 64) - 1
+Definition max_64  := (integerPow 2 63) - 1
+Definition min_64  := 0 - (integerPow 2 63)
+Definition max_32u := (4294967295 : Z)
+Definition max_32  := (2147483647 : Z)
+Definition min_32  := (0 - 2147483648 : Z)
+Definition max_8   := (127 : Z)
+Definition min_8   := (0 - 128 : Z)
+Definition max_5   := (31 : Z)
+Definition min_5   := (0 - 32 : Z)
+*)
+
+(* just_list takes a list of maybes and returns Some xs if all elements have
+   a value, and None if one of the elements is None. *)
+(*val just_list : forall a. list (option a) -> option (list a)*)
+Fixpoint just_list {A} (l : list (option A)) := match l with
+  | [] => Some []
+  | (x :: xs) =>
+    match (x, just_list xs) with
+      | (Some x, Some xs) => Some (x :: xs)
+      | (_, _) => None
+    end
+  end.
+(*declare {isabelle} termination_argument just_list = automatic
+
+lemma just_list_spec:
+  ((forall xs. (just_list xs = None) <-> List.elem None xs) &&
+   (forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))*)
+
+Lemma just_list_length {A} : forall (l : list (option A)) (l' : list A),
+  Some l' = just_list l -> List.length l = List.length l'.
+induction l.
+* intros.
+  simpl in H.
+  inversion H.
+  reflexivity.
+* intros.
+  destruct a; simplify_eq H.
+  simpl in *.
+  destruct (just_list l); simplify_eq H.
+  intros.
+  subst.
+  simpl.
+  f_equal.
+  apply IHl.
+  reflexivity.
+Qed.
+
+Lemma just_list_length_Z {A} : forall (l : list (option A)) l', Some l' = just_list l -> length_list l = length_list l'.
+unfold length_list.
+intros.
+f_equal.
+auto using just_list_length.
+Qed.
+
+(*** Bits *)
+Inductive bitU := B0 | B1 | BU.
+
+Definition showBitU b :=
+match b with
+  | B0 => "O"
+  | B1 => "I"
+  | BU => "U"
+end%string.
+
+Definition bitU_char b :=
+match b with
+| B0 => "0"
+| B1 => "1"
+| BU => "?"
+end%char.
+
+(*instance (Show bitU)
+  let show := showBitU
+end*)
+
+Class BitU (a : Type) : Type := {
+  to_bitU : a -> bitU;
+  of_bitU : bitU -> a
+}.
+
+Instance bitU_BitU : (BitU bitU) := {
+  to_bitU b := b;
+  of_bitU b := b
+}.
+
+Definition bool_of_bitU bu := match bu with
+  | B0 => Some false
+  | B1 => Some true
+  | BU => None
+  end.
+
+Definition bitU_of_bool (b : bool) := if b then B1 else B0.
+
+(*Instance bool_BitU : (BitU bool) := {
+  to_bitU := bitU_of_bool;
+  of_bitU := bool_of_bitU
+}.*)
+
+Definition cast_bit_bool := bool_of_bitU.
+(*
+Definition bit_lifted_of_bitU bu := match bu with
+  | B0 => Bitl_zero
+  | B1 => Bitl_one
+  | BU => Bitl_undef
+  end.
+
+Definition bitU_of_bit := function
+  | Bitc_zero => B0
+  | Bitc_one  => B1
+  end.
+
+Definition bit_of_bitU := function
+  | B0 => Bitc_zero
+  | B1 => Bitc_one
+  | BU => failwith "bit_of_bitU: BU"
+  end.
+
+Definition bitU_of_bit_lifted := function
+  | Bitl_zero => B0
+  | Bitl_one  => B1
+  | Bitl_undef => BU
+  | Bitl_unknown => failwith "bitU_of_bit_lifted Bitl_unknown"
+  end.
+*)
+Definition not_bit b :=
+match b with
+  | B1 => B0
+  | B0 => B1
+  | BU => BU
+  end.
+
+(*val is_one : Z -> bitU*)
+Definition is_one (i : Z) :=
+  if i =? 1 then B1 else B0.
+
+Definition binop_bit op x y :=
+  match (x, y) with
+  | (BU,_) => BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
+  | (_,BU) => BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
+  | (x,y) => bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y))
+  end.
+
+(*val and_bit : bitU -> bitU -> bitU
+Definition and_bit := binop_bit (&&)
+
+val or_bit : bitU -> bitU -> bitU
+Definition or_bit := binop_bit (||)
+
+val xor_bit : bitU -> bitU -> bitU
+Definition xor_bit := binop_bit xor
+
+val (&.) : bitU -> bitU -> bitU
+Definition inline (&.) x y := and_bit x y
+
+val (|.) : bitU -> bitU -> bitU
+Definition inline (|.) x y := or_bit x y
+
+val (+.) : bitU -> bitU -> bitU
+Definition inline (+.) x y := xor_bit x y
+*)
+
+(*** Bool lists ***)
+
+(*val bools_of_nat_aux : integer -> natural -> list bool -> list bool*)
+Fixpoint bools_of_nat_aux len (x : nat) (acc : list bool) : list bool :=
+  match len with
+  | O => acc
+  | S len' => bools_of_nat_aux len' (x / 2) ((if x mod 2 =? 1 then true else false) :: acc)
+  end %nat.
+  (*else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2)*)
+(*declare {isabelle} termination_argument bools_of_nat_aux = automatic*)
+Definition bools_of_nat len n := bools_of_nat_aux (Z.to_nat len) n [] (*List.reverse (bools_of_nat_aux n)*).
+
+(*val nat_of_bools_aux : natural -> list bool -> natural*)
+Fixpoint nat_of_bools_aux (acc : nat) (bs : list bool) : nat :=
+  match bs with
+  | [] => acc
+  | true :: bs => nat_of_bools_aux ((2 * acc) + 1) bs
+  | false :: bs => nat_of_bools_aux (2 * acc) bs
+end.
+(*declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic*)
+Definition nat_of_bools bs := nat_of_bools_aux 0 bs.
+
+(*val unsigned_of_bools : list bool -> integer*)
+Definition unsigned_of_bools bs := Z.of_nat (nat_of_bools bs).
+
+(*val signed_of_bools : list bool -> integer*)
+Definition signed_of_bools bs :=
+  match bs with
+    | true :: _  => 0 - (1 + (unsigned_of_bools (List.map negb bs)))
+    | false :: _ => unsigned_of_bools bs
+    | [] => 0 (* Treat empty list as all zeros *)
+  end.
+
+(*val int_of_bools : bool -> list bool -> integer*)
+Definition int_of_bools (sign : bool) bs := if sign then signed_of_bools bs else unsigned_of_bools bs.
+
+(*val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a*)
+Fixpoint pad_list_nat {a} (x : a) (xs : list a) n :=
+  match n with
+  | O => xs
+  | S n' => pad_list_nat x (x :: xs) n'
+  end.
+(*declare {isabelle} termination_argument pad_list = automatic*)
+Definition pad_list {a} x xs n := @pad_list_nat a x xs (Z.to_nat n).
+
+Definition ext_list {a} pad len (xs : list a) :=
+  let longer := len - (Z.of_nat (List.length xs)) in
+  if longer <? 0 then skipn (Z.abs_nat (longer)) xs
+  else pad_list pad xs longer.
+
+(*let extz_bools len bs = ext_list false len bs*)
+Definition exts_bools len bs :=
+  match bs with
+    | true :: _ => ext_list true len bs
+    | _ => ext_list false len bs
+  end.
+
+Fixpoint add_one_bool_ignore_overflow_aux bits := match bits with
+  | [] => []
+  | false :: bits => true :: bits
+  | true :: bits => false :: add_one_bool_ignore_overflow_aux bits
+end.
+(*declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic*)
+
+Definition add_one_bool_ignore_overflow bits :=
+  List.rev (add_one_bool_ignore_overflow_aux (List.rev bits)).
+
+(*let bool_list_of_int n =
+  let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in
+  if n >= (0 : integer) then bs_abs
+  else add_one_bool_ignore_overflow (List.map not bs_abs)
+let bools_of_int len n = exts_bools len (bool_list_of_int n)*)
+Definition bools_of_int len n :=
+  let bs_abs := bools_of_nat len (Z.abs_nat n) in
+  if n >=? 0 then bs_abs
+  else add_one_bool_ignore_overflow (List.map negb bs_abs).
+
+(*** Bit lists ***)
+
+(*val bits_of_nat_aux : natural -> list bitU*)
+Fixpoint bits_of_nat_aux n x :=
+  match n,x with
+  | O,_ => []
+  | _,O => []
+  | S n, S _ => (if x mod 2 =? 1 then B1 else B0) :: bits_of_nat_aux n (x / 2)
+  end%nat.
+(**declare {isabelle} termination_argument bits_of_nat_aux = automatic*)
+Definition bits_of_nat n := List.rev (bits_of_nat_aux n n).
+
+(*val nat_of_bits_aux : natural -> list bitU -> natural*)
+Fixpoint nat_of_bits_aux acc bs := match bs with
+  | [] => Some acc
+  | B1 :: bs => nat_of_bits_aux ((2 * acc) + 1) bs
+  | B0 :: bs => nat_of_bits_aux (2 * acc) bs
+  | BU :: bs => None
+end%nat.
+(*declare {isabelle} termination_argument nat_of_bits_aux = automatic*)
+Definition nat_of_bits bits := nat_of_bits_aux 0 bits.
+
+Definition not_bits := List.map not_bit.
+
+Definition binop_bits op bsl bsr :=
+  List.fold_right (fun '(bl, br) acc => binop_bit op bl br :: acc) [] (List.combine bsl bsr).
+(*
+Definition and_bits := binop_bits (&&)
+Definition or_bits := binop_bits (||)
+Definition xor_bits := binop_bits xor
+
+val unsigned_of_bits : list bitU -> Z*)
+Definition unsigned_of_bits bits :=
+match just_list (List.map bool_of_bitU bits) with
+| Some bs => Some (unsigned_of_bools bs)
+| None => None
+end.
+
+(*val signed_of_bits : list bitU -> Z*)
+Definition signed_of_bits bits :=
+  match just_list (List.map bool_of_bitU bits) with
+  | Some bs => Some (signed_of_bools bs)
+  | None => None
+  end.
+
+(*val int_of_bits : bool -> list bitU -> maybe integer*)
+Definition int_of_bits (sign : bool) bs :=
+ if sign then signed_of_bits bs else unsigned_of_bits bs.
+
+(*val pad_bitlist : bitU -> list bitU -> Z -> list bitU*)
+Fixpoint pad_bitlist_nat (b : bitU) bits n :=
+match n with
+| O => bits
+| S n' => pad_bitlist_nat b (b :: bits) n'
+end.
+Definition pad_bitlist b bits n := pad_bitlist_nat b bits (Z.to_nat n). (* Negative n will come out as 0 *)
+(*  if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1).
+declare {isabelle} termination_argument pad_bitlist = automatic*)
+
+Definition ext_bits pad len bits :=
+  let longer := len - (Z.of_nat (List.length bits)) in
+  if longer <? 0 then skipn (Z.abs_nat longer) bits
+  else pad_bitlist pad bits longer.
+
+Definition extz_bits len bits := ext_bits B0 len bits.
+Parameter undefined_list_bitU : list bitU.
+Definition exts_bits len bits :=
+  match bits with
+  | BU :: _ => undefined_list_bitU (*failwith "exts_bits: undefined bit"*)
+  | B1 :: _ => ext_bits B1 len bits
+  | _ => ext_bits B0 len bits
+  end.
+
+Fixpoint add_one_bit_ignore_overflow_aux bits := match bits with
+  | [] => []
+  | B0 :: bits => B1 :: bits
+  | B1 :: bits => B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ => undefined_list_bitU (*failwith "add_one_bit_ignore_overflow: undefined bit"*)
+end.
+(*declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic*)
+
+Definition add_one_bit_ignore_overflow bits :=
+  rev (add_one_bit_ignore_overflow_aux (rev bits)).
+
+Definition bitlist_of_int n :=
+  let bits_abs := B0 :: bits_of_nat (Z.abs_nat n) in
+  if n >=? 0 then bits_abs
+  else add_one_bit_ignore_overflow (not_bits bits_abs).
+
+Definition bits_of_int len n := exts_bits len (bitlist_of_int n).
+
+(*val arith_op_bits :
+  (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU*)
+Definition arith_op_bits (op : Z -> Z -> Z) (sign : bool) l r :=
+  match (int_of_bits sign l, int_of_bits sign r) with
+    | (Some li, Some ri) => bits_of_int (length_list l) (op li ri)
+    | (_, _) => repeat [BU] (length_list l)
+  end.
+
+
+Definition char_of_nibble x :=
+  match x with
+  | (B0, B0, B0, B0) => Some "0"%char
+  | (B0, B0, B0, B1) => Some "1"%char
+  | (B0, B0, B1, B0) => Some "2"%char
+  | (B0, B0, B1, B1) => Some "3"%char
+  | (B0, B1, B0, B0) => Some "4"%char
+  | (B0, B1, B0, B1) => Some "5"%char
+  | (B0, B1, B1, B0) => Some "6"%char
+  | (B0, B1, B1, B1) => Some "7"%char
+  | (B1, B0, B0, B0) => Some "8"%char
+  | (B1, B0, B0, B1) => Some "9"%char
+  | (B1, B0, B1, B0) => Some "A"%char
+  | (B1, B0, B1, B1) => Some "B"%char
+  | (B1, B1, B0, B0) => Some "C"%char
+  | (B1, B1, B0, B1) => Some "D"%char
+  | (B1, B1, B1, B0) => Some "E"%char
+  | (B1, B1, B1, B1) => Some "F"%char
+  | _ => None
+  end.
+
+Fixpoint hexstring_of_bits bs := match bs with
+  | b1 :: b2 :: b3 :: b4 :: bs =>
+     let n := char_of_nibble (b1, b2, b3, b4) in
+     let s := hexstring_of_bits bs in
+     match (n, s) with
+     | (Some n, Some s) => Some (String n s)
+     | _ => None
+     end
+  | [] => Some EmptyString
+  | _ => None
+  end%string.
+
+Fixpoint binstring_of_bits bs := match bs with
+  | b :: bs => String (bitU_char b) (binstring_of_bits bs)
+  | [] => EmptyString
+  end.
+
+Definition show_bitlist bs :=
+  match hexstring_of_bits bs with
+  | Some s => String "0" (String "x" s)
+  | None => String "0" (String "b" (binstring_of_bits bs))
+  end.
+
+(*** List operations *)
+(*
+Definition inline (^^) := append_list
+
+val subrange_list_inc : forall a. list a -> Z -> Z -> list a*)
+Definition subrange_list_inc {A} (xs : list A) i j :=
+  let toJ := firstn (Z.to_nat j + 1) xs in
+  let fromItoJ := skipn (Z.to_nat i) toJ in
+  fromItoJ.
+
+(*val subrange_list_dec : forall a. list a -> Z -> Z -> list a*)
+Definition subrange_list_dec {A} (xs : list A) i j :=
+  let top := (length_list xs) - 1 in
+  subrange_list_inc xs (top - i) (top - j).
+
+(*val subrange_list : forall a. bool -> list a -> Z -> Z -> list a*)
+Definition subrange_list {A} (is_inc : bool) (xs : list A) i j :=
+ if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j.
+
+Definition splitAt {A} n (l : list A) := (firstn n l, skipn n l).
+
+(*val update_subrange_list_inc : forall a. list a -> Z -> Z -> list a -> list a*)
+Definition update_subrange_list_inc {A} (xs : list A) i j xs' :=
+  let (toJ,suffix) := splitAt (Z.to_nat j + 1) xs in
+  let (prefix,_fromItoJ) := splitAt (Z.to_nat i) toJ in
+  prefix ++ xs' ++ suffix.
+
+(*val update_subrange_list_dec : forall a. list a -> Z -> Z -> list a -> list a*)
+Definition update_subrange_list_dec {A} (xs : list A) i j xs' :=
+  let top := (length_list xs) - 1 in
+  update_subrange_list_inc xs (top - i) (top - j) xs'.
+
+(*val update_subrange_list : forall a. bool -> list a -> Z -> Z -> list a -> list a*)
+Definition update_subrange_list {A} (is_inc : bool) (xs : list A) i j xs' :=
+  if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs'.
+
+Open Scope nat.
+Fixpoint nth_in_range {A} (n:nat) (l:list A) : n < length l -> A.
+refine 
+  (match n, l with
+  | O, h::_ => fun _ => h
+  | S m, _::t => fun H => nth_in_range A m t _
+  | _,_ => fun H => _
+  end).
+exfalso. inversion H.
+exfalso. inversion H.
+simpl in H. omega.
+Defined.
+
+Lemma nth_in_range_is_nth : forall A n (l : list A) d (H : n < length l),
+  nth_in_range n l H = nth n l d.
+intros until d. revert n.
+induction l; intros n H.
+* inversion H.
+* destruct n.
+  + reflexivity.
+  + apply IHl.
+Qed.
+
+Lemma nth_Z_nat {A} {n} {xs : list A} :
+  (0 <= n)%Z -> (n < length_list xs)%Z -> Z.to_nat n < length xs.
+unfold length_list.
+intros nonneg bounded.
+rewrite Z2Nat.inj_lt in bounded; auto using Zle_0_nat.
+rewrite Nat2Z.id in bounded.
+assumption.
+Qed.
+
+(*
+Lemma nth_top_aux {A} {n} {xs : list A} : Z.to_nat n < length xs -> let top := ((length_list xs) - 1)%Z in Z.to_nat (top - n)%Z < length xs.
+unfold length_list.
+generalize (length xs).
+intro n0.
+rewrite <- (Nat2Z.id n0).
+intro H.
+apply Z2Nat.inj_lt.
+* omega. 
+*)
+
+Close Scope nat.
+
+(*val access_list_inc : forall a. list a -> Z -> a*)
+Definition access_list_inc {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} := nth_in_range (Z.to_nat n) xs (nth_Z_nat (use_ArithFact _) (use_ArithFact _)).
+
+(*val access_list_dec : forall a. list a -> Z -> a*)
+Definition access_list_dec {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} : A.
+refine (
+  let top := (length_list xs) - 1 in
+  @access_list_inc A xs (top - n) _ _).
+constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega.
+constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega.
+Defined.
+
+(*val access_list : forall a. bool -> list a -> Z -> a*)
+Definition access_list {A} (is_inc : bool) (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} :=
+  if is_inc then access_list_inc xs n else access_list_dec xs n.
+
+Definition access_list_opt_inc {A} (xs : list A) n := nth_error xs (Z.to_nat n).
+
+(*val access_list_dec : forall a. list a -> Z -> a*)
+Definition access_list_opt_dec {A} (xs : list A) n :=
+  let top := (length_list xs) - 1 in
+  access_list_opt_inc xs (top - n).
+
+(*val access_list : forall a. bool -> list a -> Z -> a*)
+Definition access_list_opt {A} (is_inc : bool) (xs : list A) n :=
+  if is_inc then access_list_opt_inc xs n else access_list_opt_dec xs n.
+
+Definition list_update {A} (xs : list A) n x := firstn n xs ++ x :: skipn (S n) xs.
+
+(*val update_list_inc : forall a. list a -> Z -> a -> list a*)
+Definition update_list_inc {A} (xs : list A) n x := list_update xs (Z.to_nat n) x.
+
+(*val update_list_dec : forall a. list a -> Z -> a -> list a*)
+Definition update_list_dec {A} (xs : list A) n x :=
+  let top := (length_list xs) - 1 in
+  update_list_inc xs (top - n) x.
+
+(*val update_list : forall a. bool -> list a -> Z -> a -> list a*)
+Definition update_list {A} (is_inc : bool) (xs : list A) n x :=
+  if is_inc then update_list_inc xs n x else update_list_dec xs n x.
+
+(*Definition extract_only_element := function
+  | [] => failwith "extract_only_element called for empty list"
+  | [e] => e
+  | _ => failwith "extract_only_element called for list with more elements"
+end*)
+
+(*** Machine words *)
+
+Definition mword (n : Z) :=
+  match n with
+  | Zneg _ => False
+  | Z0 => word 0
+  | Zpos p => word (Pos.to_nat p)
+  end.
+
+Definition get_word {n} : mword n -> word (Z.to_nat n) :=
+  match n with
+  | Zneg _ => fun x => match x with end
+  | Z0 => fun x => x
+  | Zpos p => fun x => x
+  end.
+
+Definition with_word {n} {P : Type -> Type} : (word (Z.to_nat n) -> P (word (Z.to_nat n))) -> mword n -> P (mword n) :=
+match n with
+| Zneg _ => fun f w => match w with end
+| Z0 => fun f w => f w
+| Zpos _ => fun f w => f w
+end.
+
+Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n :=
+  match n with
+  | Zneg _ => fun H _ => _
+  | Z0 => fun _ w => w
+  | Zpos _ => fun _ w => w
+  end.
+
+(*val length_mword : forall a. mword a -> Z*)
+Definition length_mword {n} (w : mword n) := n.
+
+(*val slice_mword_dec : forall a b. mword a -> Z -> Z -> mword b*)
+(*Definition slice_mword_dec w i j := word_extract (Z.to_nat i) (Z.to_nat j) w.
+
+val slice_mword_inc : forall a b. mword a -> Z -> Z -> mword b
+Definition slice_mword_inc w i j :=
+  let top := (length_mword w) - 1 in
+  slice_mword_dec w (top - i) (top - j)
+
+val slice_mword : forall a b. bool -> mword a -> Z -> Z -> mword b
+Definition slice_mword is_inc w i j := if is_inc then slice_mword_inc w i j else slice_mword_dec w i j
+
+val update_slice_mword_dec : forall a b. mword a -> Z -> Z -> mword b -> mword a
+Definition update_slice_mword_dec w i j w' := word_update w (Z.to_nat i) (Z.to_nat j) w'
+
+val update_slice_mword_inc : forall a b. mword a -> Z -> Z -> mword b -> mword a
+Definition update_slice_mword_inc w i j w' :=
+  let top := (length_mword w) - 1 in
+  update_slice_mword_dec w (top - i) (top - j) w'
+
+val update_slice_mword : forall a b. bool -> mword a -> Z -> Z -> mword b -> mword a
+Definition update_slice_mword is_inc w i j w' :=
+  if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w'
+
+val access_mword_dec : forall a. mword a -> Z -> bitU*)
+Parameter undefined_bit : bool.
+Definition getBit {n} :=
+match n with
+| O => fun (w : word O) i => undefined_bit
+| S n => fun (w : word (S n)) i => wlsb (wrshift w i)
+end.
+
+Definition access_mword_dec {m} (w : mword m) n := bitU_of_bool (getBit (get_word w) (Z.to_nat n)).
+
+(*val access_mword_inc : forall a. mword a -> Z -> bitU*)
+Definition access_mword_inc {m} (w : mword m) n :=
+  let top := (length_mword w) - 1 in
+  access_mword_dec w (top - n).
+
+(*Parameter access_mword : forall {a}, bool -> mword a -> Z -> bitU.*)
+Definition access_mword {a} (is_inc : bool) (w : mword a) n :=
+  if is_inc then access_mword_inc w n else access_mword_dec w n.
+
+Definition setBit {n} :=
+match n with
+| O => fun (w : word O) i b => w
+| S n => fun (w : word (S n)) i (b : bool) =>
+  let bit : word (S n) := wlshift (natToWord _ 1) i in
+  let mask : word (S n) := wnot bit in
+  let masked := wand mask w in
+  if b then masked else wor masked bit
+end.
+
+(*val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a*)
+Definition update_mword_bool_dec {a} (w : mword a) n b : mword a :=
+  with_word (P := id) (fun w => setBit w (Z.to_nat n) b) w.
+Definition update_mword_dec {a} (w : mword a) n b :=
+ match bool_of_bitU b with
+ | Some bl => Some (update_mword_bool_dec w n bl)
+ | None => None
+ end.
+
+(*val update_mword_inc : forall a. mword a -> Z -> bitU -> mword a*)
+Definition update_mword_inc {a} (w : mword a) n b :=
+  let top := (length_mword w) - 1 in
+  update_mword_dec w (top - n) b.
+
+(*Parameter update_mword : forall {a}, bool -> mword a -> Z -> bitU -> mword a.*)
+Definition update_mword {a} (is_inc : bool) (w : mword a) n b :=
+  if is_inc then update_mword_inc w n b else update_mword_dec w n b.
+
+(*val int_of_mword : forall 'a. bool -> mword 'a -> integer*)
+Definition int_of_mword {a} `{ArithFact (a >= 0)} (sign : bool) (w : mword a) :=
+  if sign then wordToZ (get_word w) else Z.of_N (wordToN (get_word w)).
+
+
+(*val mword_of_int : forall a. Size a => Z -> Z -> mword a
+Definition mword_of_int len n :=
+  let w := wordFromInteger n in
+  if (length_mword w = len) then w else failwith "unexpected word length"
+*)
+Program Definition mword_of_int {len} `{H:ArithFact (len >= 0)} n : mword len :=
+match len with
+| Zneg _ => _
+| Z0 => ZToWord 0 n
+| Zpos p => ZToWord (Pos.to_nat p) n
+end.
+Next Obligation.
+destruct H.
+auto.
+Defined.
+(*
+(* Translating between a type level number (itself n) and an integer *)
+
+Definition size_itself_int x := Z.of_nat (size_itself x)
+
+(* NB: the corresponding sail type is forall n. atom(n) -> itself(n),
+   the actual integer is ignored. *)
+
+val make_the_value : forall n. Z -> itself n
+Definition inline make_the_value x := the_value
+*)
+
+Fixpoint bitlistFromWord {n} w :=
+match w with
+| WO => []
+| WS b w => b :: bitlistFromWord w
+end.
+
+Fixpoint wordFromBitlist l : word (length l) :=
+match l with
+| [] => WO
+| b::t => WS b (wordFromBitlist t)
+end.
+
+Local Open Scope nat.
+Program Definition fit_bbv_word {n m} (w : word n) : word m :=
+match Nat.compare m n with
+| Gt => extz w (m - n)
+| Eq => w
+| Lt => split2 (n - m) m w
+end.
+Next Obligation.
+symmetry in Heq_anonymous.
+apply nat_compare_gt in Heq_anonymous.
+omega.
+Defined.
+Next Obligation.
+
+symmetry in Heq_anonymous.
+apply nat_compare_eq in Heq_anonymous.
+omega.
+Defined.
+Next Obligation.
+
+symmetry in Heq_anonymous.
+apply nat_compare_lt in Heq_anonymous.
+omega.
+Defined.
+Local Close Scope nat.
+
+(*** Bitvectors *)
+
+Class Bitvector (a:Type) : Type := {
+  bits_of : a -> list bitU;
+  of_bits : list bitU -> option a;
+  of_bools : list bool -> a;
+  (* The first parameter specifies the desired length of the bitvector *)
+  of_int : Z -> Z -> a;
+  length : a -> Z;
+  unsigned : a -> option Z;
+  signed : a -> option Z;
+  arith_op_bv : (Z -> Z -> Z) -> bool -> a -> a -> a
+}.
+
+Instance bitlist_Bitvector {a : Type} `{BitU a} : (Bitvector (list a)) := {
+  bits_of v := List.map to_bitU v;
+  of_bits v := Some (List.map of_bitU v);
+  of_bools v := List.map of_bitU (List.map bitU_of_bool v);
+  of_int len n := List.map of_bitU (bits_of_int len n);
+  length := length_list;
+  unsigned v := unsigned_of_bits (List.map to_bitU v);
+  signed v := signed_of_bits (List.map to_bitU v);
+  arith_op_bv op sign l r := List.map of_bitU (arith_op_bits op sign (List.map to_bitU l) (List.map to_bitU r))
+}.
+
+Class ReasonableSize (a : Z) : Prop := {
+  isPositive : a >= 0
+}.
+
+Hint Resolve -> Z.gtb_lt Z.geb_le Z.ltb_lt Z.leb_le : zbool.
+Hint Resolve <- Z.ge_le_iff Z.gt_lt_iff : zbool.
+
+(* Omega doesn't know about In, but can handle disjunctions. *)
+Ltac unfold_In :=
+repeat match goal with
+| H:context [In ?x (?y :: ?t)] |- _ => change (In x (y :: t)) with (y = x \/ In x t) in H
+| H:context [In ?x []] |- _ => change (In x []) with False in H
+end.
+
+(* Definitions in the context that involve proof for other constraints can
+   break some of the constraint solving tactics, so prune definition bodies
+   down to integer types. *)
+Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end.
+Ltac clear_non_Z_defns := 
+  repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end.
+
+Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0).
+constructor.
+destruct a.
+auto with zarith.
+auto using Z.le_ge, Zle_0_pos.
+destruct w.
+Qed.
+Ltac unwrap_ArithFacts :=
+  repeat match goal with H:(ArithFact _) |- _ => let H' := fresh H in case H as [H'] end.
+Ltac unbool_comparisons :=
+  repeat match goal with
+  | H:context [Z.geb _ _] |- _ => rewrite Z.geb_leb in H
+  | H:context [Z.gtb _ _] |- _ => rewrite Z.gtb_ltb in H
+  | H:context [Z.leb _ _ = true] |- _ => rewrite Z.leb_le in H
+  | H:context [Z.ltb _ _ = true] |- _ => rewrite Z.ltb_lt in H
+  | H:context [Z.eqb _ _ = true] |- _ => rewrite Z.eqb_eq in H
+  | H:context [Z.leb _ _ = false] |- _ => rewrite Z.leb_gt in H
+  | H:context [Z.ltb _ _ = false] |- _ => rewrite Z.ltb_ge in H
+  | H:context [Z.eqb _ _ = false] |- _ => rewrite Z.eqb_neq in H
+  | H:context [orb _ _ = true] |- _ => rewrite Bool.orb_true_iff in H
+  | H:context [andb _ _ = true] |- _ => apply andb_prop in H
+  | H:context [generic_eq _ _ = true] |- _ => apply generic_eq_true in H
+  | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H
+  | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H
+  | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H
+  end.
+(* Split up dependent pairs to get at proofs of properties *)
+Ltac extract_properties :=
+  repeat match goal with H := (projT1 ?X) |- _ =>
+    let x := fresh "x" in
+    let Hx := fresh "Hx" in
+    destruct X as [x Hx] in *;
+    change (projT1 (existT _ x Hx)) with x in *; unfold H in * end;
+  repeat match goal with |- context [projT1 ?X] =>
+    let x := fresh "x" in
+    let Hx := fresh "Hx" in
+    destruct X as [x Hx] in *;
+    change (projT1 (existT _ x Hx)) with x in * end.
+(* TODO: hyps, too? *)
+Ltac reduce_list_lengths :=
+  repeat match goal with |- context [length_list ?X] => 
+    let r := (eval cbn in (length_list X)) in
+    change (length_list X) with r
+  end.
+(* TODO: can we restrict this to concrete terms? *)
+Ltac reduce_pow :=
+  repeat match goal with H:context [Z.pow ?X ?Y] |- _ => 
+    let r := (eval cbn in (Z.pow X Y)) in
+    change (Z.pow X Y) with r in H
+  end;
+  repeat match goal with |- context [Z.pow ?X ?Y] => 
+    let r := (eval cbn in (Z.pow X Y)) in
+    change (Z.pow X Y) with r
+  end.
+Ltac dump_context :=
+  repeat match goal with
+  | H:=?X |- _ => idtac H ":=" X; fail
+  | H:?X |- _ => idtac H ":" X; fail end;
+  match goal with |- ?X => idtac "Goal:" X end.
+Ltac solve_arithfact :=
+(*dump_context;*)
+ clear_non_Z_defns;
+ extract_properties;
+ repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
+ unwrap_ArithFacts;
+ unfold_In;
+ autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
+ unbool_comparisons;
+ reduce_list_lengths;
+ reduce_pow;
+(*dump_context;*)
+ solve [apply ArithFact_mword; assumption
+       | constructor; omega with Z
+         (* The datatypes hints give us some list handling, esp In *)
+       | constructor; auto with datatypes zbool zarith sail].
+Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
+
+Hint Unfold length_mword : sail.
+
+Lemma ReasonableSize_witness (a : Z) (w : mword a) : ReasonableSize a.
+constructor.
+destruct a.
+auto with zarith.
+auto using Z.le_ge, Zle_0_pos.
+destruct w.
+Qed.
+
+Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
+
+Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := {
+  bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v));
+  of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v));
+  of_bools v := to_word isPositive (fit_bbv_word (wordFromBitlist v));
+  of_int len z := mword_of_int z; (* cheat a little *)
+  length v := a;
+  unsigned v := Some (Z.of_N (wordToN (get_word v)));
+  signed v := Some (wordToZ (get_word v));
+  arith_op_bv op sign l r := mword_of_int (op (int_of_mword sign l) (int_of_mword sign r))
+}.
+
+Section Bitvector_defs.
+Context {a b} `{Bitvector a} `{Bitvector b}.
+
+Definition opt_def {a} (def:a) (v:option a) :=
+match v with
+| Some x => x
+| None => def
+end.
+
+(* The Lem version is partial, but lets go with BU here to avoid constraints for now *)
+Definition access_bv_inc (v : a) n := opt_def BU (access_list_opt_inc (bits_of v) n).
+Definition access_bv_dec (v : a) n := opt_def BU (access_list_opt_dec (bits_of v) n).
+
+Definition update_bv_inc (v : a) n b := update_list true  (bits_of v) n b.
+Definition update_bv_dec (v : a) n b := update_list false (bits_of v) n b.
+
+Definition subrange_bv_inc (v : a) i j := subrange_list true  (bits_of v) i j.
+Definition subrange_bv_dec (v : a) i j := subrange_list true  (bits_of v) i j.
+
+Definition update_subrange_bv_inc (v : a) i j (v' : b) := update_subrange_list true  (bits_of v) i j (bits_of v').
+Definition update_subrange_bv_dec (v : a) i j (v' : b) := update_subrange_list false (bits_of v) i j (bits_of v').
+
+(*val extz_bv : forall a b. Bitvector a, Bitvector b => Z -> a -> b*)
+Definition extz_bv n (v : a) : option b := of_bits (extz_bits n (bits_of v)).
+
+(*val exts_bv : forall a b. Bitvector a, Bitvector b => Z -> a -> b*)
+Definition exts_bv n (v : a) : option b := of_bits (exts_bits n (bits_of v)).
+
+(*val string_of_bv : forall a. Bitvector a => a -> string *)
+Definition string_of_bv v := show_bitlist (bits_of v).
+
+End Bitvector_defs.
+
+(*** Bytes and addresses *)
+
+Definition memory_byte := list bitU.
+
+(*val byte_chunks : forall a. list a -> option (list (list a))*)
+Fixpoint byte_chunks {a} (bs : list a) := match bs with
+  | [] => Some []
+  | a::b::c::d::e::f::g::h::rest =>
+     match byte_chunks rest with
+     | None => None
+     | Some rest => Some ([a;b;c;d;e;f;g;h] :: rest)
+     end
+  | _ => None
+end.
+(*declare {isabelle} termination_argument byte_chunks = automatic*)
+
+Section BytesBits.
+Context {a} `{Bitvector a}.
+
+(*val bytes_of_bits : forall a. Bitvector a => a -> option (list memory_byte)*)
+Definition bytes_of_bits (bs : a) := byte_chunks (bits_of bs).
+
+(*val bits_of_bytes : forall a. Bitvector a => list memory_byte -> a*)
+Definition bits_of_bytes (bs : list memory_byte) : list bitU := List.concat (List.map bits_of bs).
+
+Definition mem_bytes_of_bits (bs : a) := option_map (@rev (list bitU)) (bytes_of_bits bs).
+Definition bits_of_mem_bytes (bs : list memory_byte) := bits_of_bytes (List.rev bs).
+
+End BytesBits.
+
+(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
+Definition bitv_of_byte_lifteds v :=
+  foldl (fun x (Byte_lifted y) => x ++ (List.map bitU_of_bit_lifted y)) [] v
+
+val bitv_of_bytes : list Sail_impl_base.byte -> list bitU
+Definition bitv_of_bytes v :=
+  foldl (fun x (Byte y) => x ++ (List.map bitU_of_bit y)) [] v
+
+val byte_lifteds_of_bitv : list bitU -> list byte_lifted
+Definition byte_lifteds_of_bitv bits :=
+  let bits := List.map bit_lifted_of_bitU bits in
+  byte_lifteds_of_bit_lifteds bits
+
+val bytes_of_bitv : list bitU -> list byte
+Definition bytes_of_bitv bits :=
+  let bits := List.map bit_of_bitU bits in
+  bytes_of_bits bits
+
+val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
+Definition bit_lifteds_of_bitUs bits := List.map bit_lifted_of_bitU bits
+
+val bit_lifteds_of_bitv : list bitU -> list bit_lifted
+Definition bit_lifteds_of_bitv v := bit_lifteds_of_bitUs v
+
+
+val address_lifted_of_bitv : list bitU -> address_lifted
+Definition address_lifted_of_bitv v :=
+  let byte_lifteds := byte_lifteds_of_bitv v in
+  let maybe_address_integer :=
+    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
+    | Some bs => Some (integer_of_byte_list bs)
+    | _ => None
+    end in
+  Address_lifted byte_lifteds maybe_address_integer
+
+val bitv_of_address_lifted : address_lifted -> list bitU
+Definition bitv_of_address_lifted (Address_lifted bs _) := bitv_of_byte_lifteds bs
+
+val address_of_bitv : list bitU -> address
+Definition address_of_bitv v :=
+  let bytes := bytes_of_bitv v in
+  address_of_byte_list bytes*)
+
+Fixpoint reverse_endianness_list (bits : list bitU) :=
+  match bits with
+  | _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: t =>
+    reverse_endianness_list t ++ firstn 8 bits
+  | _ => bits
+  end.
+
+(*** Registers *)
+
+Definition register_field := string.
+Definition register_field_index : Type := string * (Z * Z). (* name, start and end *)
+
+Inductive register :=
+  | Register : string * (* name *)
+               Z * (* length *)
+               Z * (* start index *)
+               bool * (* is increasing *)
+               list register_field_index
+               -> register
+  | UndefinedRegister : Z -> register (* length *)
+  | RegisterPair : register * register -> register.
+
+Record register_ref regstate regval a :=
+   { name : string;
+     (*is_inc : bool;*)
+     read_from : regstate -> a;
+     write_to : a -> regstate -> regstate;
+     of_regval : regval -> option a;
+     regval_of : a -> regval }.
+Notation "{[ r 'with' 'name' := e ]}" := ({| name := e; read_from := read_from r; write_to := write_to r; of_regval := of_regval r; regval_of := regval_of r |}).
+Notation "{[ r 'with' 'read_from' := e ]}" := ({| read_from := e; name := name r; write_to := write_to r; of_regval := of_regval r; regval_of := regval_of r |}).
+Notation "{[ r 'with' 'write_to' := e ]}" := ({| write_to := e; name := name r; read_from := read_from r; of_regval := of_regval r; regval_of := regval_of r |}).
+Notation "{[ r 'with' 'of_regval' := e ]}" := ({| of_regval := e; name := name r; read_from := read_from r; write_to := write_to r; regval_of := regval_of r |}).
+Notation "{[ r 'with' 'regval_of' := e ]}" := ({| regval_of := e; name := name r; read_from := read_from r; write_to := write_to r; of_regval := of_regval r |}).
+Arguments name [_ _ _].
+Arguments read_from [_ _ _].
+Arguments write_to [_ _ _].
+Arguments of_regval [_ _ _].
+Arguments regval_of [_ _ _].
+
+(* Register accessors: pair of functions for reading and writing register values *)
+Definition register_accessors regstate regval : Type :=
+  ((string -> regstate -> option regval) *
+   (string -> regval -> regstate -> option regstate)).
+
+Record field_ref regtype a :=
+   { field_name : string;
+     field_start : Z;
+     field_is_inc : bool;
+     get_field : regtype -> a;
+     set_field : regtype -> a -> regtype }.
+Arguments field_name [_ _].
+Arguments field_start [_ _].
+Arguments field_is_inc [_ _].
+Arguments get_field [_ _].
+Arguments set_field [_ _].
+
+(*
+(*let name_of_reg := function
+  | Register name _ _ _ _ => name
+  | UndefinedRegister _ => failwith "name_of_reg UndefinedRegister"
+  | RegisterPair _ _ => failwith "name_of_reg RegisterPair"
+end
+
+Definition size_of_reg := function
+  | Register _ size _ _ _ => size
+  | UndefinedRegister size => size
+  | RegisterPair _ _ => failwith "size_of_reg RegisterPair"
+end
+
+Definition start_of_reg := function
+  | Register _ _ start _ _ => start
+  | UndefinedRegister _ => failwith "start_of_reg UndefinedRegister"
+  | RegisterPair _ _ => failwith "start_of_reg RegisterPair"
+end
+
+Definition is_inc_of_reg := function
+  | Register _ _ _ is_inc _ => is_inc
+  | UndefinedRegister _ => failwith "is_inc_of_reg UndefinedRegister"
+  | RegisterPair _ _ => failwith "in_inc_of_reg RegisterPair"
+end
+
+Definition dir_of_reg := function
+  | Register _ _ _ is_inc _ => dir_of_bool is_inc
+  | UndefinedRegister _ => failwith "dir_of_reg UndefinedRegister"
+  | RegisterPair _ _ => failwith "dir_of_reg RegisterPair"
+end
+
+Definition size_of_reg_nat reg := Z.to_nat (size_of_reg reg)
+Definition start_of_reg_nat reg := Z.to_nat (start_of_reg reg)
+
+val register_field_indices_aux : register -> register_field -> option (Z * Z)
+Fixpoint register_field_indices_aux register rfield :=
+  match register with
+  | Register _ _ _ _ rfields => List.lookup rfield rfields
+  | RegisterPair r1 r2 =>
+      let m_indices := register_field_indices_aux r1 rfield in
+      if isSome m_indices then m_indices else register_field_indices_aux r2 rfield
+  | UndefinedRegister _ => None
+  end
+
+val register_field_indices : register -> register_field -> Z * Z
+Definition register_field_indices register rfield :=
+  match register_field_indices_aux register rfield with
+  | Some indices => indices
+  | None => failwith "Invalid register/register-field combination"
+  end
+
+Definition register_field_indices_nat reg regfield=
+  let (i,j) := register_field_indices reg regfield in
+  (Z.to_nat i,Z.to_nat j)*)
+
+(*let rec external_reg_value reg_name v :=
+  let (internal_start, external_start, direction) :=
+    match reg_name with
+     | Reg _ start size dir =>
+        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
+     | Reg_slice _ reg_start dir (slice_start, _) =>
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     | Reg_field _ reg_start dir _ (slice_start, _) =>
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     | Reg_f_slice _ reg_start dir _ _ (slice_start, _) =>
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     end in
+  let bits := bit_lifteds_of_bitv v in
+  <| rv_bits           := bits;
+     rv_dir            := direction;
+     rv_start          := external_start;
+     rv_start_internal := internal_start |>
+
+val internal_reg_value : register_value -> list bitU
+Definition internal_reg_value v :=
+  List.map bitU_of_bit_lifted v.rv_bits
+         (*(Z.of_nat v.rv_start_internal)
+         (v.rv_dir = D_increasing)*)
+
+
+Definition external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) :=
+  match d with
+  (*This is the case the thread/concurrecny model expects, so no change needed*)
+  | D_increasing => (i,j)
+  | D_decreasing => let slice_i = start - i in
+                    let slice_j = (i - j) + slice_i in
+                    (slice_i,slice_j)
+  end *)
+
+(* TODO
+Definition external_reg_whole r :=
+  Reg (r.name) (Z.to_nat r.start) (Z.to_nat r.size) (dir_of_bool r.is_inc)
+
+Definition external_reg_slice r (i,j) :=
+  let start := Z.to_nat r.start in
+  let dir := dir_of_bool r.is_inc in
+  Reg_slice (r.name) start dir (external_slice dir start (i,j))
+
+Definition external_reg_field_whole reg rfield :=
+  let (m,n) := register_field_indices_nat reg rfield in
+  let start := start_of_reg_nat reg in
+  let dir := dir_of_reg reg in
+  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
+
+Definition external_reg_field_slice reg rfield (i,j) :=
+  let (m,n) := register_field_indices_nat reg rfield in
+  let start := start_of_reg_nat reg in
+  let dir := dir_of_reg reg in
+  Reg_f_slice (name_of_reg reg) start dir rfield
+              (external_slice dir start (m,n))
+              (external_slice dir start (i,j))*)
+
+(*val external_mem_value : list bitU -> memory_value
+Definition external_mem_value v :=
+  byte_lifteds_of_bitv v $> List.reverse
+
+val internal_mem_value : memory_value -> list bitU
+Definition internal_mem_value bytes :=
+  List.reverse bytes $> bitv_of_byte_lifteds*)
+
+
+val foreach : forall a vars.
+  (list a) -> vars -> (a -> vars -> vars) -> vars*)
+Fixpoint foreach {a Vars} (l : list a) (vars : Vars) (body : a -> Vars -> Vars) : Vars :=
+match l with
+| [] => vars
+| (x :: xs) => foreach xs (body x vars) body
+end.
+
+(*declare {isabelle} termination_argument foreach = automatic
+
+val index_list : Z -> Z -> Z -> list Z*)
+Fixpoint index_list' from to step n :=
+  if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then
+    match n with
+    | O => []
+    | S n => from :: index_list' (from + step) to step n
+    end
+  else [].
+
+Definition index_list from to step :=
+  if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then
+    index_list' from to step (S (Z.abs_nat (from - to)))
+  else [].
+
+Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Vars) : Vars :=
+  if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then
+    match n with
+    | O => vars
+    | S n => let vars := body from vars in foreach_Z' (from + step) to step n vars body
+    end
+  else vars.
+
+Definition foreach_Z {Vars} from to step vars body :=
+  foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body.
+
+Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars :=
+  if sumbool_of_bool (from + off <=? to) then
+    match n with
+    | O => vars
+    | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body
+    end
+  else vars.
+
+Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars :=
+  if sumbool_of_bool (to <=? from + off) then
+    match n with
+    | O => vars
+    | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body
+    end
+  else vars.
+
+Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} :=
+    foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} :=
+    foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+
+(*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars
+Fixpoint while vars cond body :=
+  if cond vars then while (body vars) cond body else vars
+
+val until : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars
+Fixpoint until vars cond body :=
+  let vars := body vars in
+  if cond vars then vars else until (body vars) cond body
+
+
+Definition assert' b msg_opt :=
+  let msg := match msg_opt with
+  | Some msg => msg
+  | None  => "unspecified error"
+  end in
+  if b then () else failwith msg
+
+(* convert numbers unsafely to naturals *)
+
+class (ToNatural a) val toNatural : a -> natural end
+(* eta-expanded for Isabelle output, otherwise it breaks *)
+instance (ToNatural Z) let toNatural := (fun n => naturalFromInteger n) end
+instance (ToNatural int)     let toNatural := (fun n => naturalFromInt n)     end
+instance (ToNatural nat)     let toNatural := (fun n => naturalFromNat n)     end
+instance (ToNatural natural) let toNatural := (fun n => n)                    end
+
+Definition toNaturalFiveTup (n1,n2,n3,n4,n5) :=
+  (toNatural n1,
+   toNatural n2,
+   toNatural n3,
+   toNatural n4,
+   toNatural n5)
+
+(* Let the following types be generated by Sail per spec, using either bitlists
+   or machine words as bitvector representation *)
+(*type regfp :=
+  | RFull of (string)
+  | RSlice of (string * Z * Z)
+  | RSliceBit of (string * Z)
+  | RField of (string * string)
+
+type niafp :=
+  | NIAFP_successor
+  | NIAFP_concrete_address of vector bitU
+  | NIAFP_indirect_address
+
+(* only for MIPS *)
+type diafp :=
+  | DIAFP_none
+  | DIAFP_concrete of vector bitU
+  | DIAFP_reg of regfp
+
+Definition regfp_to_reg (reg_info : string -> option string -> (nat * nat * direction * (nat * nat))) := function
+  | RFull name =>
+     let (start,length,direction,_) := reg_info name None in
+     Reg name start length direction
+  | RSlice (name,i,j) =>
+     let i = Z.to_nat i in
+     let j = Z.to_nat j in
+     let (start,length,direction,_) = reg_info name None in
+     let slice = external_slice direction start (i,j) in
+     Reg_slice name start direction slice
+  | RSliceBit (name,i) =>
+     let i = Z.to_nat i in
+     let (start,length,direction,_) = reg_info name None in
+     let slice = external_slice direction start (i,i) in
+     Reg_slice name start direction slice
+  | RField (name,field_name) =>
+     let (start,length,direction,span) = reg_info name (Some field_name) in
+     let slice = external_slice direction start span in
+     Reg_field name start direction field_name slice
+end
+
+Definition niafp_to_nia reginfo = function
+  | NIAFP_successor => NIA_successor
+  | NIAFP_concrete_address v => NIA_concrete_address (address_of_bitv v)
+  | NIAFP_indirect_address => NIA_indirect_address
+end
+
+Definition diafp_to_dia reginfo = function
+  | DIAFP_none => DIA_none
+  | DIAFP_concrete v => DIA_concrete_address (address_of_bitv v)
+  | DIAFP_reg r => DIA_register (regfp_to_reg reginfo r)
+end
+*)
+*)
+
+(* Arithmetic functions which return proofs that match the expected Sail
+   types in smt.sail. *)
+
+Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m).
+Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m).
+Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
+
+(* Similarly, for ranges (currently in MIPS) *)
+
+Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool :=
+  (projT1 l) =? (projT1 r).
+Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
+  : {x & ArithFact (n+o <= x <= m+p)} :=
+  build_ex ((projT1 l) + (projT1 r)).
+Definition sub_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
+  : {x & ArithFact (n-p <= x <= m-o)} :=
+  build_ex ((projT1 l) - (projT1 r)).
+Definition negate_range {n m} (l : {l : Z & ArithFact (n <= l <= m)})
+  : {x : Z & ArithFact ((- m) <= x <= (- n))} :=
+  build_ex (- (projT1 l)).
+
+Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <= a /\ c <= b)} :=
+  build_ex (Z.min a b).
+Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} :=
+  build_ex (Z.max a b).
+
+
+(*** Generic vectors *)
+
+Definition vec (T:Type) (n:Z) := { l : list T & length_list l = n }.
+Definition vec_length {T n} (v : vec T n) := n.
+Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+  access_list_dec (projT1 v) m.
+Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+  access_list_inc (projT1 v) m.
+
+Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >= 0)} : vec T n :=
+  existT _ (repeat [t] n) _.
+Next Obligation.
+rewrite repeat_length; auto using fact.
+unfold length_list.
+simpl.
+auto with zarith.
+Qed.
+
+Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat.
+revert l.
+induction n.
+* simpl. auto with arith.
+* intros l H.
+  destruct l.
+  + inversion H.
+  + simpl in H.
+    simpl.
+    rewrite IHn; auto with arith.
+Qed.
+Lemma update_list_inc_length {T} {l:list T} {m x} : 0 <= m < length_list l -> length_list (update_list_inc l m x) = length_list l.
+unfold update_list_inc, list_update, length_list.
+intro H.
+f_equal.
+assert ((0 <= Z.to_nat m < Datatypes.length l)%nat).
+{ destruct H as [H1 H2].
+  split.
+  + change 0%nat with (Z.to_nat 0).
+    apply Z2Nat.inj_le; auto with zarith.
+  + rewrite <- Nat2Z.id.
+    apply Z2Nat.inj_lt; auto with zarith.
+}
+rewrite app_length.
+rewrite firstn_length_le; only 2:omega.
+cbn -[skipn].
+rewrite skipn_length;
+omega.
+Qed.
+
+Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _.
+Next Obligation.
+unfold update_list_dec.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+  destruct v. simpl (projT1 _). rewrite e.
+  omega.
+Qed.
+
+Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _.
+Next Obligation.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+  destruct v. simpl (projT1 _). rewrite e.
+  omega.
+Qed.
+
+Program Definition vec_map {S T} (f : S -> T) {n} (v : vec S n) : vec T n := existT _ (List.map f (projT1 v)) _.
+Next Obligation.
+destruct v as [l H].
+cbn.
+unfold length_list.
+rewrite map_length.
+apply H.
+Qed.
+
+Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) :=
+  match just_list (projT1 v) with
+  | None => None
+  | Some v' => Some (existT _ v' _)
+  end.
+Next Obligation.
+rewrite <- (just_list_length_Z _ _ Heq_anonymous).
+destruct v.
+assumption.
+Qed.
+
+Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
+
+Program Definition vec_of_list {A} n (l : list A) : option (vec A n) :=
+  if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None.
+Next Obligation.
+symmetry.
+apply Z.eqb_eq.
+assumption.
+Qed.
+
+Definition vec_of_list_len {A} (l : list A) : vec A (length_list l) := existT _ l (eq_refl _).
+
+Definition map_bind {A B} (f : A -> option B) (a : option A) : option B :=
+match a with
+| Some a' => f a'
+| None => None
+end.
\ No newline at end of file
diff --git a/snapshots/coq/lib/coq/_CoqProject b/snapshots/coq/lib/coq/_CoqProject
new file mode 100644
index 00000000..9f5d26b8
--- /dev/null
+++ b/snapshots/coq/lib/coq/_CoqProject
@@ -0,0 +1,2 @@
+-R . Sail
+-R ../../../bbv/theories bbv