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

6 files changed, 289 insertions, 317 deletions

diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
index fd0fc17b..abab2163 100644
--- a/src/gen_lib/armv8_extras.lem
+++ b/src/gen_lib/armv8_extras.lem
@@ -1,31 +1,53 @@
 open import Pervasives
-open import State
+open import Sail_impl_base
+open import Vector
 open import Sail_values
+open import Prompt
 
-let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
-let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
-let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
-let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
-let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
-
-let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
-let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
-
-let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
-let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
-
-let wMem_Val_NORMAL (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return ()
-let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O
-
-let DataMemoryBarrier_Reads () = return ()
-let DataMemoryBarrier_Writes () = return ()
-let DataMemoryBarrier_All () = return ()
-let DataSynchronizationBarrier_Reads () = return ()
-let DataSynchronizationBarrier_Writes () = return ()
-let DataSynchronizationBarrier_All () = return ()
-let InstructionSynchronizationBarrier () = return ()
+val rMem_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_STREAM         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ATOMICL        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+
+let rMem_NORMAL (addr,size)         = read_memory Read_plain addr size
+let rMem_STREAM (addr,size)         = read_memory Read_stream addr size
+let rMem_ORDERED (addr,size)        = read_memory Read_acquire addr size
+let rMem_ATOMIC (addr,size)         = read_memory Read_exclusive addr size
+let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size
+
+val wMem_Addr_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ATOMIC         : forall 'e. (vector bitU * integer) -> M 'e unit
+val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit
+
+let wMem_Addr_NORMAL (addr,size)         = write_memory_ea Write_plain addr size
+let wMem_Addr_ORDERED (addr,size)        = write_memory_ea Write_release addr size
+let wMem_Addr_ATOMIC (addr,size)         = write_memory_ea Write_exclusive addr size
+let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size
+
+
+val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit
+val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU
+
+let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return ()
+(* in ARM the status returned is inversed *)
+let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I)
+
+
+val DataMemoryBarrier_Reads            : forall 'e. unit -> M 'e unit
+val DataMemoryBarrier_Writes           : forall 'e. unit -> M 'e unit
+val DataMemoryBarrier_All              : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_Reads   : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_Writes  : forall 'e. unit -> M 'e unit
+val DataSynchronizationBarrier_All     : forall 'e. unit -> M 'e unit
+val InstructionSynchronizationBarrier  : forall 'e. unit -> M 'e unit
+
+let DataMemoryBarrier_Reads ()           = barrier DMB_LD
+let DataMemoryBarrier_Writes ()          = barrier DMB_ST
+let DataMemoryBarrier_All ()             = barrier DMB
+let DataSynchronizationBarrier_Reads ()  = barrier DSB_LD
+let DataSynchronizationBarrier_Writes () = barrier DSB_ST
+let DataSynchronizationBarrier_All ()    = barrier DSB
+let InstructionSynchronizationBarrier () = barrier Isync
 
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index e08da230..2e255db7 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -1,49 +1,47 @@
 open import Pervasives
+open import Sail_impl_base
 open import Vector
-open import State
 open import Sail_values
+open import Prompt
 
-(*
-let rec countLeadingZeros_helper bits =  
-((match bits with
-    | (Interp.V_lit (L_aux( L_zero, _)))::bits -> 
-      let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
-      Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
-    | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
-))
-let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
-  | [Interp.V_track( v, r);Interp.V_track( v2, r2)] -> 
-    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
-  | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
-  | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
-  | [Interp.V_unknown;_] -> Interp.V_unknown
-  | [_;Interp.V_unknown] -> Interp.V_unknown
-  | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] -> 
-    countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
-))
- *)
-
-let MEMr (addr,l) = read_memory (unsigned addr) l
-let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
-
-let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
-let MEMw_EA_cond (addr,l) = write_writeEA (unsigned addr) l
-                                        
-let MEMw (addr,l,value) = write_memory (unsigned addr) l value
-let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return I
-
-let I_Sync () = return ()
-let H_Sync () = return ()
-let LW_Sync () = return ()
-let EIEIO_Sync () = return ()
-
-let recalculate_dependency () = return ()
+val MEMr         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
+
+let MEMr (addr,size) = read_memory Read_plain addr size
+let MEMr_reserve (addr,size) = read_memory Read_reserve addr size
+
+
+val MEMw_EA      : forall 'e. (vector bitU * integer) -> M 'e unit
+val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit
+                                                           
+let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size
+let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size
+
+
+val MEMw             : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit
+val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU
+
+let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return ()
+let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b)
+
+
+val I_Sync     : forall 'e unit -> M 'e unit
+val H_Sync     : forall 'e unit -> M 'e unit
+val LW_Sync    : forall 'e unit -> M 'e unit
+val EIEIO_Sync : forall 'e unit -> M 'e unit
+
+let I_Sync ()     = barrier Isync
+let H_Sync ()     = barrier Sync
+let LW_Sync ()    = barrier LwSync
+let EIEIO_Sync () = barrier Eieio
+
+let recalculate_dependency () = footprint
 
 let trap () = exit "error"
 (* this needs to change, but for that we'd have to make the type checker know about trap 
  * as an effect *)
 
-val countLeadingZeroes : vector bit * integer -> integer
+val countLeadingZeroes : vector bitU * integer -> integer
 let countLeadingZeroes (Vector bits _ _ ,n)  = 
   let (_,bits) = List.splitAt (natFromInteger n) bits in
   integerFromNat (List.length (takeWhile ((=) O) bits))
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index e1e8658e..02a83d8a 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,251 +1,134 @@
 open import Pervasives_extra
+open import Sail_impl_base
 open import Vector
+open import Sail_values
 open import Arch
 
-let compose f g x = f (g x)
-
-type end_flag =
-  | E_big_endian
-  | E_little_endian
-
-type direction = 
-  | D_increasing
-  | D_decreasing
-
-type register_value = <| 
-    rv_bits: list bit (* MSB first, smallest index number *); 
-    rv_dir: direction; 
-    rv_start: nat ;
-    rv_start_internal: nat; 
-    (*when dir is increasing, rv_start = rv_start_internal. 
-      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
-    |>
-
-type byte = list bit (* of length 8 *)  (*MSB first everywhere*)
-
-type address = integer
-type address_lifted = address
-
-type memory_value = list byte
-(* the list is of length >=1 *)
-(* for both big-endian (Power) and little-endian (ARM), the head of the
-     list is the byte stored at the lowest address *)
-(* for big-endian Power the head of the list is the most-significant
-   byte, in both the interpreter and machineDef* code. *)
-(* For little-endian ARM, the head of the list is the
-   least-significant byte in machineDef* code and the
-   most-significant byte in interpreter code, with the switch over
-   (a list-reverse) being done just inside the interpreter interface*)
-(* In other words, in the machineDef* code the lowest-address byte is first,
-   and in the interpreter code the most-significant byte is first *)
-
-type opcode = Opcode of list byte (* of length 4 *)
-
-type read_kind =
-  (* common reads *)
-  | Read_plain
-  (* Power reads *)
-  | Read_reserve
-  (* AArch64 reads *)
-  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
-
-type write_kind =
-  (* common writes *)
-  | Write_plain
-  (* Power writes *)
-  | Write_conditional
-  (* AArch64 writes *)
-  | Write_release | Write_exclusive | Write_exclusive_release
-
-type barrier_kind =
-  (* Power barriers *)
-  | Sync | LwSync | Eieio | Isync
-  (* AArch64 barriers *)
-  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
-
-type slice = (nat * nat)
-
-type reg_name = 
-  (* Name of the register, accessing the entire register, the start and size of this register, 
-   * and its direction *)
-  | Reg of string * nat * nat * direction
-                                  
-  (* Name of the register, accessing from the bit indexed by the first
-   * to the bit indexed by the second integer of the slice, inclusive. For
-   * machineDef* the first is a smaller number or equal to the second.  *)
-  | Reg_slice of string * nat * direction * slice 
-                                              
-  (* Name of the register, start and direction, and name of the field of the register
-   * accessed. The slice specifies where this field is in the register*)
-  | Reg_field of string * nat * direction * string * slice 
-
-  (* The first four components are as in Reg_field; the final slice
-   * specifies a part of the field, indexed w.r.t. the register as a whole *)
-  | Reg_f_slice of string * nat * direction * string * slice * slice 
-
-type outcome 'e 'a =
-  (* Request to read memory, value is location to read followed by registers that location depended 
-   * on when mode.track_values, integer is size to read, followed by registers that were used in 
-   * computing that size *)
-  (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
-  | Read_mem of read_kind * address_lifted * nat * (memory_value -> outcome 'e 'a)
-                    
-  (* Request to write memory, first value and dependent registers is location, second is the value 
-   * to write *)
-  | Write_mem of write_kind * address_lifted * nat * memory_value * (bool -> outcome 'e 'a)
-                                             
-  (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
-  | Write_ea of write_kind * address_lifted * nat * outcome 'e 'a
-                                                                              
-  (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
-   * ea signal *)
-  | Write_memv of memory_value * (bool -> outcome 'e 'a)
-                                                           
-  (* Request a memory barrier *)
-  (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
-   * need that *)
-  | Barrier of barrier_kind * outcome 'e 'a
-                                
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome 'e 'a
-                   
-  (* Request to read register *)
-  | Read_reg of reg_name * (register_value -> outcome 'e 'a)
-                             
-  (* Request to write register *)
-  | Write_reg of reg_name * register_value * outcome 'e 'a
-                                               
-  (* List of instruction states to be run in parrallel, any order permitted.
-     Expects concurrency model to choose an order: a permutation of the original list *)
-  | Nondet_choice of unit
-                                                
-  (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
-   * provide a handler. *)
-  | Escape of 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
-
-  (* Stop for incremental stepping, function can be used to display function call data *)
-  | Done of 'a
-
-type M 'e 'a = outcome 'e 'a
-
-val return : forall 'e 'a. 'a -> M 'e 'a
+val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a
 let return a = Done a
 
-val (>>=) : forall 'e 'a 'b. M 'e 'a -> ('a -> M 'e 'b) -> M 'e 'b
-let rec (>>=) m f = match m with
-  | Done a -> f a
-  | Read_mem rk addr sz k ->    Read_mem rk addr sz    (fun v -> (k v) >>= f)
-  | Write_mem wk addr sz v k -> Write_mem wk addr sz v (fun b -> (k b) >>= f)
-  | Write_ea wk addr sz k ->    Write_ea wk addr sz    (k >>= f)
-  | Write_memv v k ->           Write_memv v           (fun b -> (k b) >>= f)
-  | Barrier bk k ->             Barrier bk             (k >>= f)
-  | Footprint k ->              Footprint              (k >>= f)
-  | Read_reg reg k ->           Read_reg reg           (fun v -> (k v) >>= f)
-  | Write_reg reg v k ->        Write_reg reg v        (k >>= f)
-  | Nondet_choice () ->         Nondet_choice ()
-  | Escape e ->                 Escape e
-  end
-
-val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
-let (>>) m n = m >>= fun _ -> n
-
-val exit : forall 'a 'e. 'e -> M 'e 'a
-let exit = Escape
-
-val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
-let rec byte_chunks n list = match (n,list) with
-  | (0,_) -> []
-  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
-  | _ -> failwith "byte_chunks not given enough bits"
+val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b
+let rec bind m f = match m with
+  | Done a ->              f a 
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s  in (bind o f,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s  in (bind o f,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s  in (bind o f,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s  in (bind o f,opt))
+  | Escape o_s  ->         Escape o_s
 end
 
-val bitvFromBytes : list byte -> vector bit
-let bitvFromBytes v = Vector (foldl (++) [] v) 0 defaultDir
 
-let dir is_inc = if is_inc then D_increasing else D_decreasing
+type M 'e 'a = Sail_impl_base.outcome unit 'e 'a
 
-val bitvFromRegisterValue : register_value -> vector bit
-let bitvFromRegisterValue v =
-  Vector (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+let (>>=) = bind
+val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
+let (>>) m n = m >>= fun _ -> n
 
-val registerValueFromBitv : vector bit -> register -> register_value
-let registerValueFromBitv (Vector bits start is_inc) reg = 
-  let start = natFromInteger start in
-  <| rv_bits = bits;
-     rv_dir = dir is_inc;
-     rv_start_internal = start;
-     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+val exit : forall 'a 'e. 'e -> M 'e 'a
+let exit e = Escape (Just (return e,Nothing))
 
-val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (vector bit)
+val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU)
 let read_memory rk addr sz =
+  let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
-  Read_mem rk addr sz (compose Done bitvFromBytes)
-
-val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool
-let write_memory wk addr sz (Vector v _ _) =
+  let k memory_value =
+    let bitv = bitv_of_byte_lifteds memory_value in
+    (Done bitv,Nothing) in
+  Read_mem (rk,addr,sz) k
+
+val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer  -> M 'e unit
+let write_memory_ea wk addr sz =
+  let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
-  Write_mem wk addr sz (byte_chunks sz v) Done
+  Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val read_reg_range : forall 'e. register -> (integer * integer) -> M 'e (vector bit)
-let read_reg_range reg (i,j) =
-  let (i,j) = (natFromInteger i,natFromInteger j) in
-  let start = natFromInteger (start_index_reg reg) in
-  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
+val write_memory_val : forall 'e. vector bitU -> M 'e bool
+let write_memory_val v =
+  let v = byte_lifteds_of_bitv v in
+  let k successful = (return successful,Nothing) in
+  Write_memv v k
 
-val write_reg_range : forall 'e. register -> (integer * integer) -> vector bit -> M 'e unit
-let write_reg_range reg (i,j) v =
-  let rv = registerValueFromBitv v reg in
-  let start = natFromInteger (start_index_reg reg) in
+
+val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU)
+let read_reg_range reg i j =
   let (i,j) = (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Write_reg reg rv (Done ())
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_bit : forall 'e. register -> integer -> M 'e bit
+val read_reg_bit : forall 'e. register -> integer -> M 'e bitU
 let read_reg_bit reg i = 
-  let i = natFromInteger i in
-  let start = natFromInteger (start_index_reg reg) in
-  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
-  Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
+  read_reg_range reg i i >>= fun v -> return (access v i)
 
-val write_reg_bit : forall 'e. register -> integer -> bit -> M 'e unit
-let write_reg_bit reg i bit = write_reg_range reg (i,i) (Vector [bit] 0 true)
-
-val read_reg : forall 'e. register -> M 'e (vector bit)
+val read_reg : forall 'e. register -> M 'e (vector bitU)
 let read_reg reg =
   let start = natFromInteger (start_index_reg reg) in
   let sz = natFromInteger (length_reg reg) in
   let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
-
-val write_reg : forall 'e. register -> vector bit -> M 'e unit
-let write_reg reg v =
-  let rv = registerValueFromBitv v reg in
-  let start = natFromInteger (start_index_reg reg) in
-  let sz = natFromInteger (length_reg reg) in
-  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
-  Write_reg reg rv (Done ())
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU)
 let read_reg_field reg rfield = 
   let (i,j) =
     let (i,j) = field_indices rfield in
     (natFromInteger i,natFromInteger j) in
   let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
-  Read_reg reg (compose Done bitvFromRegisterValue)
-
-val write_reg_field : forall 'e. register -> register_field -> vector bit -> M 'e unit
-let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+  let k register_value =
+    let v = bitvFromRegisterValue register_value in
+    (Done v,Nothing) in
+  Read_reg reg k
 
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bitU
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e unit
+
+
+val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit
+let write_reg_range reg i j v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Write_reg (reg,rv) (Done (),Nothing)
+
+val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit
+let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)
+
+val write_reg : forall 'e. register -> vector bitU -> M 'e unit
+let write_reg reg v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Write_reg (reg,rv) (Done (),Nothing)
+
+val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit
+let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
+
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> M 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
-val foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
+
+val barrier : forall 'e. barrier_kind -> M 'e unit
+let barrier bk = Barrier bk (Done (), Nothing)
+
+
+val footprint : forall 'e. M 'e unit
+let footprint = Footprint (Done (),Nothing)
+
+
+val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
@@ -254,8 +137,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
+val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 46c3a10c..98b68e1b 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,10 +1,36 @@
 open import Pervasives_extra
+open import Sail_impl_base
 open import Vector
 open import Arch
 
 type i = integer
 type n = natural
 
+let to_bool = function
+  | O -> false
+  | I  -> true
+  | Undef -> failwith "to_bool applied to Undef"
+  end
+
+
+let bit_lifted_of_bitU = function
+  | O -> Bitl_zero
+  | I -> Bitl_one
+  | Undef -> Bitl_undef
+  end
+
+let bitU_of_bit = function
+  | Bitc_zero -> O
+  | Bitc_one  -> I
+  end
+
+let bitU_of_bit_lifted = function
+  | Bitl_zero -> O
+  | Bitl_one  -> I
+  | Bitl_undef -> Undef
+  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
+  end
+
 let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
 let most_significant = function
@@ -27,7 +53,7 @@ let pow m n = m ** (natFromInteger n)
 let bitwise_not (Vector bs start is_inc) =
   Vector (List.map bitwise_not_bit bs) start is_inc
 
-val is_one : integer -> bit
+val is_one : integer -> bitU
 let is_one i =
   if i = 1 then I else O
 
@@ -39,22 +65,22 @@ let bitwise_binop_bit op = function
   | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
   end
 
-val bitwise_and_bit : bit * bit -> bit
+val bitwise_and_bit : bitU * bitU -> bitU
 let bitwise_and_bit = bitwise_binop_bit (&&)
 
-val bitwise_or_bit : bit * bit -> bit
+val bitwise_or_bit : bitU * bitU -> bitU
 let bitwise_or_bit = bitwise_binop_bit (||)
 
-val bitwise_xor_bit : bit * bit -> bit
+val bitwise_xor_bit : bitU * bitU -> bitU
 let bitwise_xor_bit = bitwise_binop_bit xor
 
-val (&.) : bit -> bit -> bit
+val (&.) : bitU -> bitU -> bitU
 let (&.) x y = bitwise_and_bit (x,y)
 
-val (|.) : bit -> bit -> bit
+val (|.) : bitU -> bitU -> bitU
 let (|.) x y = bitwise_or_bit (x,y)
 
-val (+.) : bit -> bit -> bit
+val (+.) : bitU -> bitU -> bitU
 let (+.) x y = bitwise_xor_bit (x,y)
 
 let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
@@ -474,7 +500,7 @@ let make_indexed_vector entries default start length =
   let length = natFromInteger length in
   Vector (List.foldl replace (replicate length default) entries) start defaultDir
 
-val make_bit_vector_undef : integer -> vector bit
+val make_bit_vector_undef : integer -> vector bitU
 let make_bitvector_undef length =
   Vector (replicate (natFromInteger length) Undef) 0 true
 
@@ -485,6 +511,55 @@ let mask (n,Vector bits start dir) =
   Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
 
 
+let bit_of_bit_lifted = function
+  | Bitl_zero -> O
+  | Bitl_one  -> I
+  | Bitl_undef -> Undef
+  | _ -> failwith "bit_of_bit_lifted: unexpected Bitl_unknown"
+end
+
+val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
+let rec byte_chunks n list = match (n,list) with
+  | (0,_) -> []
+  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
+  | _ -> failwith "byte_chunks not given enough bits"
+end
+
+
+val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> vector bitU
+let bitv_of_byte_lifteds v =
+  Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 defaultDir
+
+val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
+let byte_lifteds_of_bitv (Vector bits length is_inc) = 
+  let bits = List.map bit_lifted_of_bitU bits in
+  byte_lifteds_of_bit_lifteds bits
+
+val address_lifted_of_bitv : vector bitU -> address_lifted
+let address_lifted_of_bitv v =
+  Address_lifted (byte_lifteds_of_bitv v) Nothing
+
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+
+val bitvFromRegisterValue : register_value -> vector bitU
+let bitvFromRegisterValue v =
+  Vector (List.map bitU_of_bit_lifted v.rv_bits)
+         (integerFromNat (v.rv_start))
+         (v.rv_dir = D_increasing)
+
+
+val registerValueFromBitv : vector bitU -> register -> register_value
+let registerValueFromBitv (Vector bits start is_inc) reg = 
+  let start = natFromInteger start in
+  <| rv_bits = List.map bit_lifted_of_bitU bits;
+     rv_dir = dir is_inc;
+     rv_start_internal = start;
+     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+
+
+
 
 
 class (ToNatural 'a)
@@ -533,4 +608,9 @@ let rec foreach_dec (i,stop,by) vars body =
        foreach_dec (i - by,stop,by) vars body
   else vars
 
-
+let assert' b msg_opt =
+  let msg = match msg_opt with
+  | Just msg -> msg
+  | Nothing  -> "unspecified error"
+  end in
+  if to_bool b then failwith msg else ()
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 5fc59207..1e7b9db4 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -6,7 +6,7 @@ open import Sail_values
 (* 'a is result type, 'e is error type *)
 type State 's 'e 'a = 's -> (either 'a 'e * 's)
 
-type memstate = map integer (list bit)
+type memstate = map integer (list bitU)
 
 type state =
   <| regstate : regstate;
@@ -39,13 +39,6 @@ let (>>) m n = m >>= fun _ -> n
 val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
 let exit e s = (Right e,s)
 
-let assert' b msg_opt =
-  let msg = match msg_opt with
-  | Just msg -> msg
-  | Nothing  -> "unspecified error"
-  end in
-  if to_bool b then failwith msg else ()
-
 val read_writeEA : forall 'e. unit -> State state 'e (integer * integer)
 let read_writeEA () s = (Left s.writeEA,s)
 
@@ -61,82 +54,82 @@ let rec byte_chunks n l =
     | _ -> failwith "byte_chunks not given enough bits"
     end
 
-val read_regstate : state -> register -> vector bit
+val read_regstate : state -> register -> vector bitU
 let read_regstate s = read_regstate_aux s.regstate
 
-val write_regstate : state -> register -> vector bit -> state
+val write_regstate : state -> register -> vector bitU -> state
 let write_regstate s reg v = <| s with regstate = (write_regstate_aux s.regstate reg v) |>
 
-val read_memstate : memstate -> integer -> list bit
+val read_memstate : memstate -> integer -> list bitU
 let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s
 
-val write_memstate : memstate -> (integer * list bit) -> memstate
+val write_memstate : memstate -> (integer * list bitU) -> memstate
 let write_memstate s (addr,bits) = Map.insert addr bits s
 
-val read_memory : forall 'e. integer -> integer -> State state 'e (vector bit)
+val read_memory : forall 'e. integer -> integer -> State state 'e (vector bitU)
 let read_memory addr l s =
   let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in
   (Left (Vector (foldl (++) [] bytes) 0 defaultDir),s)
 
-val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit
+val write_memory : forall 'e. integer -> integer -> vector bitU -> State state 'e unit
 let write_memory addr l (Vector bits _ _) s =
   let addrs = List.map ((+) addr) (ints l) in
   let bytes = byte_chunks l bits in
   (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>)
 
-val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bit)
+val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bitU)
 let read_reg_range reg i j s =
   let v = slice (read_regstate s reg) i j in
   (Left v,s)
 
-val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bit
+val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bitU
 let read_reg_bit reg i s =
   let v = access (read_regstate s reg) i in
   (Left v,s)
 
-val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> State state 'e unit
+val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bitU -> State state 'e unit
 let write_reg_range reg i j v s =
   let v' = update (read_regstate s reg) i j v in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> State state 'e unit
+val write_reg_bit : forall 'e. register -> integer (*nat*) -> bitU -> State state 'e unit
 let write_reg_bit reg i bit s =
   let v = read_regstate s reg in
   let v' = update_pos v i bit in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val read_reg : forall 'e. register -> State state 'e (vector bit)
+val read_reg : forall 'e. register -> State state 'e (vector bitU)
 let read_reg reg s =
   let v = read_regstate s reg in
   (Left v,s)
 
-val write_reg : forall 'e. register -> vector bit -> State state 'e unit
+val write_reg : forall 'e. register -> vector bitU -> State state 'e unit
 let write_reg reg v s =
   let s' = write_regstate s reg v in
   (Left (),s')
 
-val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bitU)
 let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
 
-val write_reg_field : forall 'e. register -> register_field -> vector bit -> State state 'e unit
+val write_reg_field : forall 'e. register -> register_field -> vector bitU -> State state 'e unit
 let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
 
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bitU
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> State state 'e unit
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> State state 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
 val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer ->
-                            vector bit -> State state 'e unit
+                            vector bitU -> State state 'e unit
 let write_reg_field_range reg rfield i j v =
   let (i',j') = field_indices rfield in
   write_reg_range reg i' j' v
 
 val write_reg_field_bit : forall 'e. register -> register_field -> integer ->
-                            bit -> State state 'e unit
+                            bitU -> State state 'e unit
 let write_reg_field_bit reg rfield i v =
   let (i',_) = field_indices rfield in
   write_reg_bit reg (i + i') v
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index b2d68132..6acb4aa0 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,7 @@
 open import Pervasives_extra
 
-type bit = O | I | Undef
+(* this is here to avoid circular dependencies when Sail_values imports Arch.lem *)
+type bitU = O | I | Undef
 
 (* element list * start * has increasing direction *)
 type vector 'a = Vector of list 'a * integer * bool
@@ -11,11 +12,6 @@ let rec nth xs (n : integer) =
   | _ -> failwith "nth applied to empty list"
   end
 
-let to_bool = function
-  | O -> false
-  | I  -> true
-  | Undef -> failwith "to_bool applied to Undef"
-  end
 
 let get_start (Vector _ s _) = s
 let length (Vector bs _ _) = integerFromNat (length bs)