SMT: Refactor Jib values to make inlining work

Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing

function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

is always true.

11 files changed, 460 insertions, 433 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 0a410249..4bb24032 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -103,7 +103,7 @@ and 'a aval =
   | AV_list of ('a aval) list * 'a
   | AV_vector of ('a aval) list * 'a
   | AV_record of ('a aval) Bindings.t * 'a
-  | AV_C_fragment of fragment * 'a * ctyp
+  | AV_cval of cval * 'a
 
 (* Renaming variables in ANF expressions *)
 
@@ -163,7 +163,7 @@ let rec aval_rename from_id to_id = function
   | AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ)
   | AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ)
   | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ)
-  | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename (name from_id) (name to_id) fragment, typ, ctyp)
+  | AV_cval (cval, typ) -> AV_cval (cval_rename (name from_id) (name to_id) cval, typ)
 
 let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) =
   let recur = aexp_rename from_id to_id in
@@ -404,8 +404,8 @@ and pp_aval = function
   | AV_id (id, lvar) -> pp_lvar lvar (pp_id id)
   | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals)
   | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id)
-  | AV_C_fragment (frag, typ, ctyp) ->
-     pp_annot typ (string ("(" ^ string_of_ctyp ctyp ^ ")" ^ string_of_fragment frag |> Util.cyan |> Util.clear))
+  | AV_cval (cval, typ) ->
+     pp_annot typ (string (string_of_cval cval |> Util.cyan |> Util.clear))
   | AV_vector (avals, typ) ->
      pp_annot typ (string "[" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "]")
   | AV_list (avals, typ) ->
diff --git a/src/jib/anf.mli b/src/jib/anf.mli
index 26b847e2..6bc274e6 100644
--- a/src/jib/anf.mli
+++ b/src/jib/anf.mli
@@ -116,7 +116,7 @@ and 'a apat_aux =
   | AP_wild of 'a
 
 (** We allow ANF->ANF optimization to insert fragments of C code
-   directly in the ANF grammar via [AV_C_fragment]. Such fragments
+   directly in the ANF grammar via [AV_cval]. Such fragments
    must be side-effect free expressions. *)
 and 'a aval =
   | AV_lit of lit * 'a
@@ -126,7 +126,7 @@ and 'a aval =
   | AV_list of ('a aval) list * 'a
   | AV_vector of ('a aval) list * 'a
   | AV_record of ('a aval) Bindings.t * 'a
-  | AV_C_fragment of fragment * 'a * ctyp
+  | AV_cval of cval * 'a
 
 (** Function for generating unique identifiers during ANF
    translation. *)
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index ee16e2e6..f6d8dd80 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -241,15 +241,15 @@ let hex_char =
 let literal_to_fragment (L_aux (l_aux, _) as lit) =
   match l_aux with
   | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
-     Some (F_lit (V_int n), CT_fint 64)
+     Some (V_lit (VL_int n, CT_fint 64))
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
      let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
      let content = Util.string_to_list str |> List.map hex_char |> List.concat in
-     Some (F_lit (V_bits (padding @ content)), CT_fbits (String.length str * 4, true))
-  | L_unit -> Some (F_lit V_unit, CT_unit)
-  | L_true -> Some (F_lit (V_bool true), CT_bool)
-  | L_false -> Some (F_lit (V_bool false), CT_bool)
+     Some (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true)))
+  | L_unit -> Some (V_lit (VL_unit, CT_unit))
+  | L_true -> Some (V_lit (VL_bool true, CT_bool))
+  | L_false -> Some (V_lit (VL_bool false, CT_bool))
   | _ -> None
 
 let c_literals ctx =
@@ -257,7 +257,7 @@ let c_literals ctx =
     | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ { ctx with local_env = env } typ) ->
        begin
          match literal_to_fragment lit with
-         | Some (frag, ctyp) -> AV_C_fragment (frag, typ, ctyp)
+         | Some cval -> AV_cval (cval, typ)
          | None -> v
        end
     | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
@@ -292,10 +292,10 @@ let rec c_aval ctx = function
   | AV_lit (lit, typ) as v ->
      begin
        match literal_to_fragment lit with
-       | Some (frag, ctyp) -> AV_C_fragment (frag, typ, ctyp)
+       | Some cval -> AV_cval (cval, typ)
        | None -> v
      end
-  | AV_C_fragment (str, typ, ctyp) -> AV_C_fragment (str, typ, ctyp)
+  | AV_cval (cval, typ) -> AV_cval (cval, typ)
   (* An id can be converted to a C fragment if it's type can be
      stack-allocated. *)
   | AV_id (id, lvar) as v ->
@@ -309,40 +309,36 @@ let rec c_aval ctx = function
                 (* We need to check that id's type hasn't changed due to flow typing *)
                 let _, ctyp' = Bindings.find id ctx.locals in
                 if ctyp_equal ctyp ctyp' then
-                  AV_C_fragment (F_id (name id), typ, ctyp)
+                  AV_cval (V_id (name id, ctyp), typ)
                 else
                   (* id's type changed due to flow
                      typing, so it's really still heap allocated!  *)
                   v
               with
                 (* Hack: Assuming global letbindings don't change from flow typing... *)
-                Not_found -> AV_C_fragment (F_id (name id), typ, ctyp)
+                Not_found -> AV_cval (V_id (name id, ctyp), typ)
             end
           else
             v
        | Register (_, _, typ) when is_stack_typ ctx typ ->
           let ctyp = ctyp_of_typ ctx typ in
           if is_stack_ctyp ctyp then
-            AV_C_fragment (F_id (name id), typ, ctyp)
+            AV_cval (V_id (name id, ctyp), typ)
           else
             v
        | _ -> v
      end
   | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 ->
-     let bitstring = F_lit (V_bits (List.map value_of_aval_bit v)) in
-     AV_C_fragment (bitstring, typ, CT_fbits (List.length v, true))
+     let bitstring = VL_bits (List.map value_of_aval_bit v, true) in
+     AV_cval (V_lit (bitstring, CT_fbits (List.length v, true)), typ)
   | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals)
   | aval -> aval
 
-let is_c_fragment = function
-  | AV_C_fragment _ -> true
-  | _ -> false
-
 let c_fragment = function
-  | AV_C_fragment (frag, _, _) -> frag
+  | AV_cval (cval, _) -> cval
   | _ -> assert false
 
-let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail2_values.B1)))
+let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
 
 (* Map over all the functions in an aexp. *)
 let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
@@ -402,24 +398,25 @@ let analyze_primop' ctx id args typ =
   let args = List.map (c_aval ctx) args in
   let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in
 
-  let v_one = F_lit (V_int (Big_int.of_int 1)) in
-  let v_int n = F_lit (V_int (Big_int.of_int n)) in
+  let v_one = V_lit (VL_int (Big_int.of_int 1), CT_fint 64) in
+  let v_int n = V_lit (VL_int (Big_int.of_int n), CT_fint 64) in
 
   c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")"));
 
   match extern, args with
-  | "eq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] ->
-     AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool))
-  | "eq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] ->
-     AE_val (AV_C_fragment (F_call ("eq_sbits", [v1; v2]), typ, CT_bool))
+    (*
+  | "eq_bits", [AV_cval (v1, _, CT_fbits _); AV_cval (v2, _, _)] ->
+     AE_val (AV_cval (F_op (v1, "==", v2), typ, CT_bool))
+  | "eq_bits", [AV_cval (v1, _, CT_sbits _); AV_cval (v2, _, _)] ->
+     AE_val (AV_cval (F_call ("eq_sbits", [v1; v2]), typ, CT_bool))
 
-  | "neq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] ->
-     AE_val (AV_C_fragment (F_op (v1, "!=", v2), typ, CT_bool))
-  | "neq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] ->
-     AE_val (AV_C_fragment (F_call ("neq_sbits", [v1; v2]), typ, CT_bool))
+  | "neq_bits", [AV_cval (v1, _, CT_fbits _); AV_cval (v2, _, _)] ->
+     AE_val (AV_cval (F_op (v1, "!=", v2), typ, CT_bool))
+  | "neq_bits", [AV_cval (v1, _, CT_sbits _); AV_cval (v2, _, _)] ->
+     AE_val (AV_cval (F_call ("neq_sbits", [v1; v2]), typ, CT_bool))
 
-  | "eq_int", [AV_C_fragment (v1, typ1, _); AV_C_fragment (v2, typ2, _)] ->
-     AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool))
+  | "eq_int", [AV_cval (v1, typ1, _); AV_cval (v2, typ2, _)] ->
+     AE_val (AV_cval (F_op (v1, "==", v2), typ, CT_bool))
 
   | "zeros", [_] ->
      begin match destruct_vector ctx.tc_env typ with
@@ -596,7 +593,7 @@ let analyze_primop' ctx id args typ =
 
   | "undefined_bool", _ ->
      AE_val (AV_C_fragment (F_lit (V_bool false), typ, CT_bool))
-
+ *)
   | _, _ ->
      c_debug (lazy ("No optimization routine found"));
      no_change
@@ -685,7 +682,7 @@ let fix_early_stack_return ret ret_ctyp instrs =
        @ rewrite_return after
     | before, I_aux (I_end _, _) :: after ->
        before
-       @ [ireturn (F_id ret, ret_ctyp)]
+       @ [ireturn (V_id (ret, ret_ctyp))]
        @ rewrite_return after
     | before, (I_aux ((I_copy _ | I_funcall _), _) as instr) :: after ->
        before @ instr :: rewrite_return after
@@ -803,92 +800,6 @@ let hoist_allocations recursive_functions = function
 
   | cdef -> [cdef]
 
-let rec specialize_variants ctx prior =
-  let unifications = ref (Bindings.empty) in
-
-  let fix_variant_ctyp var_id new_ctors = function
-    | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors)
-    | ctyp -> ctyp
-  in
-
-  let specialize_constructor ctx ctor_id ctyp =
-    function
-    | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
-       (* Work out how each call to a constructor in instantiated and add that to unifications *)
-       let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
-       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in
-       unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
-
-       (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
-       let casts =
-         let cast_to_suprema (frag, ctyp) =
-           let suprema = ctyp_suprema ctyp in
-           if ctyp_equal ctyp suprema then
-             [], (unpoly frag, ctyp), []
-           else
-             let gs = ngensym () in
-             [idecl suprema gs;
-              icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
-             (F_id gs, suprema),
-             [iclear suprema gs]
-         in
-         List.map cast_to_suprema [cval]
-       in
-       let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in
-       let cvals = List.map (fun (_, cval, _) -> cval) casts in
-       let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in
-
-       let mk_funcall instr =
-         if List.length setup = 0 then
-           instr
-         else
-           iblock (setup @ [instr] @ cleanup)
-       in
-
-       mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux))
-
-    | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
-       c_error ~loc:l "Multiple argument constructor found"
-
-    | instr -> instr
-  in
-
-  function
-  | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
-     let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
-
-     let cdefs =
-       List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
-                      cdefs
-                      polymorphic_ctors
-     in
-
-     let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in
-     let specialized_ctors = Bindings.bindings !unifications in
-     let new_ctors = monomorphic_ctors @ specialized_ctors in
-
-     let ctx = {
-         ctx with variants = Bindings.add var_id
-                               (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors)
-                               ctx.variants
-       } in
-
-     let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in
-     let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in
-     specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs
-
-  | cdef :: cdefs ->
-     let remove_poly (I_aux (instr, aux)) =
-       match instr with
-       | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp ->
-          I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux)
-       | instr -> I_aux (instr, aux)
-     in
-     let cdef = cdef_map_instr remove_poly cdef in
-     specialize_variants ctx (cdef :: prior) cdefs
-
-  | [] -> List.rev prior, ctx
-
 (** Once we specialize variants, there may be additional type
    dependencies which could be in the wrong order. As such we need to
    sort the type definitions in the list of cdefs. *)
@@ -951,12 +862,12 @@ let remove_alias =
     let alias = ref None in
     let rec scan ctyp id n instrs =
       match n, !alias, instrs with
-      | 0, None, I_aux (I_copy (CL_id (id', ctyp'), (F_id a, ctyp'')), _) :: instrs
+      | 0, None, I_aux (I_copy (CL_id (id', ctyp'), V_id (a, ctyp'')), _) :: instrs
            when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          alias := Some a;
          scan ctyp id 1 instrs
 
-      | 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), (F_id id', ctyp'')), _) :: instrs
+      | 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), V_id (id', ctyp'')), _) :: instrs
            when Name.compare a a' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          scan ctyp id 2 instrs
 
@@ -985,9 +896,9 @@ let remove_alias =
     scan ctyp id 0
   in
   let remove_alias id alias = function
-    | I_aux (I_copy (CL_id (id', _), (F_id alias', _)), _)
+    | I_aux (I_copy (CL_id (id', _), V_id (alias', _)), _)
          when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
-    | I_aux (I_copy (CL_id (alias', _), (F_id id', _)), _)
+    | I_aux (I_copy (CL_id (alias', _), V_id (id', _)), _)
          when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
     | I_aux (I_clear (_, id'), _) -> removed
     | instr -> instr
@@ -1089,7 +1000,7 @@ let combine_variables =
          combine := Some id';
          scan id 1 instrs
 
-      | 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), (F_id c', ctyp'')), _) :: instrs
+      | 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), V_id (c', ctyp'')), _) :: instrs
            when Name.compare c c' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          scan id 2 instrs
 
@@ -1127,7 +1038,7 @@ let combine_variables =
     | instr -> instr
   in
   let is_not_self_assignment = function
-    | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Name.compare id id' = 0 -> false
+    | I_aux (I_copy (CL_id (id, _), V_id (id', _)), _) when Name.compare id id' = 0 -> false
     | _ -> true
   in
   let rec opt = function
@@ -1220,18 +1131,18 @@ let rec sgen_ctyp_name = function
   | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
   | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
 
-let sgen_cval_param (frag, ctyp) =
-  match ctyp with
+let sgen_cval cval = string_of_cval cval
+
+let sgen_cval_param cval =
+  match cval_ctyp cval with
   | CT_lbits direction ->
-     string_of_fragment frag ^ ", " ^ string_of_bool direction
+     string_of_cval cval ^ ", " ^ string_of_bool direction
   | CT_sbits (_, direction) ->
-     string_of_fragment frag ^ ", " ^ string_of_bool direction
+     string_of_cval cval ^ ", " ^ string_of_bool direction
   | CT_fbits (len, direction) ->
-     string_of_fragment frag ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
+     string_of_cval cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
   | _ ->
-     string_of_fragment frag
-
-let sgen_cval = function (frag, _) -> string_of_fragment frag
+     string_of_cval cval
 
 let rec sgen_clexp = function
   | CL_id (Have_exception _, _) -> "have_exception"
@@ -1274,8 +1185,9 @@ let rec codegen_conversion l clexp cval =
 
   (* If we have to convert between tuple types, convert the fields individually. *)
   | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from ->
+     let len = List.length ctyps_to in
      let conversions =
-       List.mapi (fun i ctyp -> codegen_conversion l (CL_tuple (clexp, i)) (F_field (fst cval, "ztup" ^ string_of_int i), ctyp)) ctyps_from
+       List.mapi (fun i ctyp -> codegen_conversion l (CL_tuple (clexp, i)) (V_tuple_member (cval, len, i))) ctyps_from
      in
      string "  /* conversions */"
      ^^ hardline
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 13e7334a..b4d7fb51 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -179,56 +179,57 @@ let rec chunkify n xs =
   | xs, ys -> xs :: chunkify n ys
 
 let rec compile_aval l ctx = function
-  | AV_C_fragment (frag, typ, ctyp) ->
+  | AV_cval (cval, typ) ->
+     let ctyp = cval_ctyp cval in
      let ctyp' = ctyp_of_typ ctx typ in
      if not (ctyp_equal ctyp ctyp') then
        raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp'));
-     [], (frag, ctyp_of_typ ctx typ), []
+     [], cval, []
 
   | AV_id (id, typ) ->
      begin
        try
          let _, ctyp = Bindings.find id ctx.locals in
-         [], (F_id (name id), ctyp), []
+         [], V_id (name id, ctyp), []
        with
        | Not_found ->
-          [], (F_id (name id), ctyp_of_typ ctx (lvar_typ typ)), []
+          [], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), []
      end
 
   | AV_ref (id, typ) ->
-     [], (F_ref (name id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
+     [], V_ref (name id, ctyp_of_typ ctx (lvar_typ typ)), []
 
   | AV_lit (L_aux (L_string str, _), typ) ->
-     [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), []
+     [], V_lit ((VL_string (String.escaped str)), ctyp_of_typ ctx typ), []
 
   | AV_lit (L_aux (L_num n, _), typ) when ctx.ignore_64 ->
-     [], (F_lit (V_int n), ctyp_of_typ ctx typ), []
+     [], V_lit ((VL_int n), ctyp_of_typ ctx typ), []
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
      let gs = ngensym () in
-     [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
-     (F_id gs, CT_lint),
+     [iinit CT_lint gs (V_lit (VL_int n, CT_fint 64))],
+     V_id (gs, CT_lint),
      [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
      let gs = ngensym () in
-     [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
-     (F_id gs, CT_lint),
+     [iinit CT_lint gs (V_lit (VL_string (Big_int.to_string n), CT_string))],
+     V_id (gs, CT_lint),
      [iclear CT_lint gs]
 
-  | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), []
-  | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), []
+  | AV_lit (L_aux (L_zero, _), _) -> [], V_lit (VL_bit Sail2_values.B0, CT_bit), []
+  | AV_lit (L_aux (L_one, _), _) -> [], V_lit (VL_bit Sail2_values.B1, CT_bit), []
 
-  | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), []
-  | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), []
+  | AV_lit (L_aux (L_true, _), _) -> [], V_lit (VL_bool true, CT_bool), []
+  | AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), []
 
   | AV_lit (L_aux (L_real str, _), _) ->
      let gs = ngensym () in
-     [iinit CT_real gs (F_lit (V_string str), CT_string)],
-     (F_id gs, CT_real),
+     [iinit CT_real gs (V_lit (VL_string str, CT_string))],
+     V_id (gs, CT_real),
      [iclear CT_real gs]
 
-  | AV_lit (L_aux (L_unit, _), _) -> [], (F_lit V_unit, CT_unit), []
+  | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), []
 
   | AV_lit (L_aux (_, l) as lit, _) ->
      raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR"))
@@ -243,7 +244,7 @@ let rec compile_aval l ctx = function
      setup
      @ [idecl tup_ctyp gs]
      @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals,
-     (F_id gs, CT_tup (List.map cval_ctyp cvals)),
+     V_id (gs, CT_tup (List.map cval_ctyp cvals)),
      [iclear tup_ctyp gs]
      @ cleanup
 
@@ -258,7 +259,7 @@ let rec compile_aval l ctx = function
      in
      [idecl ctyp gs]
      @ List.concat (List.map compile_fields (Bindings.bindings fields)),
-     (F_id gs, ctyp),
+     V_id (gs, ctyp),
      [iclear ctyp gs]
 
   | AV_vector ([], _) ->
@@ -267,13 +268,13 @@ let rec compile_aval l ctx = function
   (* Convert a small bitvector to a uint64_t literal. *)
   | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || ctx.ignore_64) ->
      begin
-       let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in
+       let bitstring = List.map value_of_aval_bit avals in
        let len = List.length avals in
        match destruct_vector ctx.tc_env typ with
        | Some (_, Ord_aux (Ord_inc, _), _) ->
-          [], (bitstring, CT_fbits (len, false)), []
+          [], V_lit (VL_bits (bitstring, false), CT_fbits (len, false)), []
        | Some (_, Ord_aux (Ord_dec, _), _) ->
-          [], (bitstring, CT_fbits (len, true)), []
+          [], V_lit (VL_bits (bitstring, true), CT_fbits (len, true)), []
        | Some _ ->
           raise (Reporting.err_general l "Encountered order polymorphic bitvector literal")
        | None ->
@@ -284,15 +285,15 @@ let rec compile_aval l ctx = function
      variable size bitvector, converting it in 64-bit chunks. *)
   | AV_vector (avals, typ) when is_bitvector avals ->
      let len = List.length avals in
-     let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in
+     let bitstring avals = VL_bits (List.map value_of_aval_bit avals, true) in
      let first_chunk = bitstring (Util.take (len mod 64) avals) in
      let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
      let gs = ngensym () in
-     [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))]
+     [iinit (CT_lbits true) gs (V_lit (first_chunk, CT_fbits (len mod 64, true)))]
      @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true))
                                        (mk_id "append_64")
-                                       [(F_id gs, CT_lbits true); (chunk, CT_fbits (64, true))]) chunks,
-     (F_id gs, CT_lbits true),
+                                       [V_id (gs, CT_lbits true); V_lit (chunk, CT_fbits (64, true))]) chunks,
+     V_id (gs, CT_lbits true),
      [iclear (CT_lbits true) gs]
 
   (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *)
@@ -306,20 +307,20 @@ let rec compile_aval l ctx = function
      in
      let gs = ngensym () in
      let ctyp = CT_fbits (len, direction) in
-     let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in
+     let mask i = VL_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0), direction) in
      let aval_mask i aval =
        let setup, cval, cleanup = compile_aval l ctx aval in
        match cval with
-       | (F_lit (V_bit Sail2_values.B0), _) -> []
-       | (F_lit (V_bit Sail2_values.B1), _) ->
-          [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)]
+       | V_lit (VL_bit Sail2_values.B0, _) -> []
+       | V_lit (VL_bit Sail2_values.B1, _) ->
+          [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))]
        | _ ->
-          setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup
+          setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] [] CT_unit] @ cleanup
      in
      [idecl ctyp gs;
-      icopy l (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)]
+      icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))]
      @ List.concat (List.mapi aval_mask (List.rev avals)),
-     (F_id gs, ctyp),
+     V_id (gs, ctyp),
      []
 
   (* Compiling a vector literal that isn't a bitvector *)
@@ -338,17 +339,17 @@ let rec compile_aval l ctx = function
        setup
        @ [iextern (CL_id (gs, vector_ctyp))
                   (mk_id "internal_vector_update")
-                  [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]]
+                  [V_id (gs, vector_ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
        @ cleanup
      in
      [idecl vector_ctyp gs;
-      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]]
+      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [V_lit (VL_int (Big_int.of_int len), CT_fint 64)]]
      @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)),
-     (F_id gs, vector_ctyp),
+     V_id (gs, vector_ctyp),
      [iclear vector_ctyp gs]
 
   | AV_vector _ as aval ->
-     raise (Reporting.err_general l ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type"))
+     raise (Reporting.err_general l ("Have AVL_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type"))
 
   | AV_list (avals, Typ_aux (typ, _)) ->
      let ctyp = match typ with
@@ -358,11 +359,11 @@ let rec compile_aval l ctx = function
      let gs = ngensym () in
      let mk_cons aval =
        let setup, cval, cleanup = compile_aval l ctx aval in
-       setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup
+       setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
      in
      [idecl (CT_list ctyp) gs]
      @ List.concat (List.map mk_cons (List.rev avals)),
-     (F_id gs, CT_list ctyp),
+     V_id (gs, CT_list ctyp),
      [iclear (CT_list ctyp) gs]
 
 let compile_funcall l ctx id args typ =
@@ -389,14 +390,14 @@ let compile_funcall l ctx id args typ =
     cleanup := arg_cleanup @ !cleanup;
     let have_ctyp = cval_ctyp cval in
     if is_polymorphic ctyp then
-      (F_poly (fst cval), have_ctyp)
+      V_poly (cval, have_ctyp)
     else if ctx.specialize_calls || ctyp_equal ctyp have_ctyp then
       cval
     else
       let gs = ngensym () in
       setup := iinit ctyp gs cval :: !setup;
       cleanup := iclear ctyp gs :: !cleanup;
-      (F_id gs, ctyp)
+      V_id (gs, ctyp)
   in
 
   assert (List.length arg_ctyps = List.length args);
@@ -411,7 +412,7 @@ let compile_funcall l ctx id args typ =
     let gs = ngensym () in
     iblock [idecl ret_ctyp gs;
             ifuncall (CL_id (gs, ret_ctyp)) id setup_args;
-            icopy l clexp (F_id gs, ret_ctyp);
+            icopy l clexp (V_id (gs, ret_ctyp));
             iclear ret_ctyp gs]
   end,
   !cleanup
@@ -427,39 +428,39 @@ let rec apat_ctyp ctx (AP_aux (apat, _, _)) =
 
 let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   let ctx = { ctx with local_env = env } in
-  match apat_aux, cval with
-  | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
-     [ijump (F_ctor_kind (frag, pid, [], ctyp), CT_bool) case_label],
+  let ctyp = cval_ctyp cval in
+  match apat_aux with
+  | AP_id (pid, _) when Env.is_union_constructor pid ctx.tc_env ->
+     [ijump (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label],
      [],
      ctx
 
-  | AP_global (pid, typ), (frag, ctyp) ->
+  | AP_global (pid, typ) ->
      let global_ctyp = ctyp_of_typ ctx typ in
      [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx
 
-  | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp ->
+  | AP_id (pid, _) when is_ct_enum ctyp ->
      begin match Env.lookup_id pid ctx.tc_env with
-     | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) (frag, ctyp)], [], ctx
-     | _ -> [ijump (F_op (F_id (name pid), "!=", frag), CT_bool) case_label], [], ctx
+     | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx
+     | _ -> [ijump (V_op (V_id (name pid, ctyp), "!=", cval)) case_label], [], ctx
      end
 
-  | AP_id (pid, typ), _ ->
-     let ctyp = cval_ctyp cval in
+  | AP_id (pid, typ) ->
      let id_ctyp = ctyp_of_typ ctx typ in
      let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
      [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx
 
-  | AP_as (apat, id, typ), _ ->
+  | AP_as (apat, id, typ) ->
      let id_ctyp = ctyp_of_typ ctx typ in
      let instrs, cleanup, ctx = compile_match ctx apat cval case_label in
      let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in
      instrs @ [idecl id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx
 
-  | AP_tup apats, (frag, ctyp) ->
+  | AP_tup apats ->
      begin
-       let get_tup n ctyp = (F_tuple_member (frag, List.length apats, n), ctyp) in
+       let get_tup n = V_tuple_member (cval, List.length apats, n) in
        let fold (instrs, cleanup, n, ctx) apat ctyp =
-         let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in
+         let instrs', cleanup', ctx = compile_match ctx apat (get_tup n) case_label in
          instrs @ instrs', cleanup' @ cleanup, n + 1, ctx
        in
        match ctyp with
@@ -469,7 +470,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
        | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp)
      end
 
-  | AP_app (ctor, apat, variant_typ), (frag, ctyp) ->
+  | AP_app (ctor, apat, variant_typ) ->
      begin match ctyp with
      | CT_variant (_, ctors) ->
         let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in
@@ -481,12 +482,12 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
         let unifiers, ctor_ctyp =
           if is_polymorphic ctor_ctyp then
             let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in
-            unifiers, ctyp_suprema (apat_ctyp ctx apat)
+            unifiers, ctyp_suprema pat_ctyp
           else
             [], ctor_ctyp
         in
-        let instrs, cleanup, ctx = compile_match ctx apat (F_ctor_unwrap (ctor, unifiers, frag), ctor_ctyp) case_label in
-        [ijump (F_ctor_kind (frag, ctor, unifiers, pat_ctyp), CT_bool) case_label]
+        let instrs, cleanup, ctx = compile_match ctx apat (V_ctor_unwrap (ctor, cval, unifiers, ctor_ctyp)) case_label in
+        [ijump (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label]
         @ instrs,
         cleanup,
         ctx
@@ -494,23 +495,25 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
         raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s"
                                                        (string_of_id ctor)
                                                        (string_of_typ variant_typ)
-                                                       (string_of_fragment ~zencode:false frag)
+                                                       (string_of_cval ~zencode:false cval)
                                                        (string_of_ctyp ctyp)))
      end
 
-  | AP_wild _, _ -> [], [], ctx
+  | AP_wild _ -> [], [], ctx
 
-  | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) ->
-     let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in
-     let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in
-     [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
-
-  | AP_cons _, (_, _) ->
-     raise (Reporting.err_general l "Tried to pattern match cons on non list type")
+  | AP_cons (hd_apat, tl_apat) ->
+     begin match ctyp with
+     | CT_list ctyp ->
+        let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_hd cval) case_label in
+        let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_tl cval) case_label in
+        [ijump (V_op (cval, "==", V_lit (VL_null, CT_list ctyp))) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
+     | _ ->
+        raise (Reporting.err_general l "Tried to pattern match cons on non list type")
+     end
 
-  | AP_nil _, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx
+  | AP_nil _ -> [ijump (V_op (cval, "!=", V_lit (VL_null, ctyp))) case_label], [], ctx
 
-let unit_fragment = (F_lit V_unit, CT_unit)
+let unit_cval = V_lit (VL_unit, CT_unit)
 
 let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   let ctx = { ctx with local_env = env } in
@@ -543,7 +546,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
-           | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
+           | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> true
          | _ -> false
        in
        let case_label = label "case_" in
@@ -555,7 +558,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          destructure
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
-              @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
+              @ [iif (V_unary ("!", V_id (gs, CT_bool))) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
             else [])
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
@@ -569,7 +572,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ List.concat (List.map compile_case cases)
      @ [imatch_failure ()]
      @ [ilabel finish_match_label],
-     (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)),
+     (fun clexp -> icopy l clexp (V_id (case_return_id, ctyp))),
      [iclear ctyp case_return_id]
      @ aval_cleanup
 
@@ -583,11 +586,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
-         | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
+         | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> true
          | _ -> false
        in
        let try_label = label "try_" in
-       let exn_cval = (F_id current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
+       let exn_cval = V_id (current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
        let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in
        let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in
        let body_setup, body_call, body_cleanup = compile_aexp ctx body in
@@ -596,7 +599,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          destructure @ [icomment "end destructuring"]
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
-              @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label]
+              @ [ijump (V_unary ("!", V_id (gs, CT_bool))) try_label]
               @ [icomment "end guard"]
             else [])
          @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@@ -607,13 +610,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
      [idecl ctyp try_return_id;
       itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
-      ijump (F_unary ("!", F_id have_exception), CT_bool) handled_exception_label]
+      ijump (V_unary ("!", V_id (have_exception, CT_bool))) handled_exception_label]
      @ List.concat (List.map compile_case cases)
      @ [igoto fallthrough_label;
         ilabel handled_exception_label;
-        icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool false), CT_bool);
+        icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool));
         ilabel fallthrough_label],
-     (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)),
+     (fun clexp -> icopy l clexp (V_id (try_return_id, ctyp))),
      []
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
@@ -655,7 +658,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ [icopy l (CL_id (gs, ctyp)) cval]
      @ cleanup
      @ List.concat (List.map compile_fields (Bindings.bindings fields)),
-     (fun clexp -> icopy l clexp (F_id gs, ctyp)),
+     (fun clexp -> icopy l clexp (V_id (gs, ctyp))),
      [iclear ctyp gs]
 
   | AE_short_circuit (SC_and, aval, aexp) ->
@@ -666,10 +669,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ [ idecl CT_bool gs;
          iif cval
              (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
-             [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)]
+             [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))]
              CT_bool ]
      @ left_cleanup,
-     (fun clexp -> icopy l clexp (F_id gs, CT_bool)),
+     (fun clexp -> icopy l clexp (V_id (gs, CT_bool))),
      []
   | AE_short_circuit (SC_or, aval, aexp) ->
      let left_setup, cval, left_cleanup = compile_aval l ctx aval in
@@ -678,11 +681,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      left_setup
      @ [ idecl CT_bool gs;
          iif cval
-             [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)]
+             [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))]
              (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              CT_bool ]
      @ left_cleanup,
-     (fun clexp -> icopy l clexp (F_id gs, CT_bool)),
+     (fun clexp -> icopy l clexp (V_id (gs, CT_bool))),
      []
 
   (* This is a faster assignment rule for updating fields of a
@@ -696,7 +699,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        @ field_cleanup
      in
      List.concat (List.map compile_fields (Bindings.bindings fields)),
-     (fun clexp -> icopy l clexp unit_fragment),
+     (fun clexp -> icopy l clexp unit_cval),
      []
 
   | AE_assign (id, assign_typ, aexp) ->
@@ -706,7 +709,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | None -> ctyp_of_typ ctx assign_typ
      in
      let setup, call, cleanup = compile_aexp ctx aexp in
-     setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup
+     setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup
 
   | AE_block (aexps, aexp, _) ->
      let block = compile_block ctx aexps in
@@ -720,7 +723,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let body_setup, body_call, body_cleanup = compile_aexp ctx body in
      let gs = ngensym () in
      let unit_gs = ngensym () in
-     let loop_test = (F_unary ("!", F_id gs), CT_bool) in
+     let loop_test = V_unary ("!", V_id (gs, CT_bool)) in
      [idecl CT_bool gs; idecl CT_unit unit_gs]
      @ [ilabel loop_start_label]
      @ [iblock (cond_setup
@@ -732,7 +735,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
                 @ body_cleanup
                 @ [igoto loop_start_label])]
      @ [ilabel loop_end_label],
-     (fun clexp -> icopy l clexp unit_fragment),
+     (fun clexp -> icopy l clexp unit_cval),
      []
 
   | AE_loop (Until, cond, body) ->
@@ -742,7 +745,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let body_setup, body_call, body_cleanup = compile_aexp ctx body in
      let gs = ngensym () in
      let unit_gs = ngensym () in
-     let loop_test = (F_id gs, CT_bool) in
+     let loop_test = V_id (gs, CT_bool) in
      [idecl CT_bool gs; idecl CT_unit unit_gs]
      @ [ilabel loop_start_label]
      @ [iblock (body_setup
@@ -754,7 +757,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
                 @ [ijump loop_test loop_end_label]
                 @ [igoto loop_start_label])]
      @ [ilabel loop_end_label],
-     (fun clexp -> icopy l clexp unit_fragment),
+     (fun clexp -> icopy l clexp unit_cval),
      []
 
   | AE_cast (aexp, typ) -> compile_aexp ctx aexp
@@ -773,7 +776,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          let gs = ngensym () in
          [idecl fn_return_ctyp gs;
           icopy l (CL_id (gs, fn_return_ctyp)) cval;
-          ireturn (F_id gs, fn_return_ctyp)]
+          ireturn (V_id (gs, fn_return_ctyp))]
      in
      return_setup @ creturn,
      (fun clexp -> icomment "unreachable after return"),
@@ -812,7 +815,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | _ -> Util.zencode_string (string_of_id id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
      in
      setup,
-     (fun clexp -> icopy l clexp (F_field (fst cval, field_str), ctyp)),
+     (fun clexp -> icopy l clexp (V_field (cval, field_str))),
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
@@ -848,18 +851,18 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
      @ [iblock ([idecl (CT_fint 64) loop_var;
-                 icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64));
+                 icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64));
                  idecl CT_unit body_gs;
                  iblock ([ilabel loop_start_label]
-                         @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label]
+                         @ [ijump (V_op (V_id (loop_var, CT_fint 64), (if is_inc then ">" else "<"), V_id (to_gs, CT_fint 64))) loop_end_label]
                          @ body_setup
                          @ [body_call (CL_id (body_gs, CT_unit))]
                          @ body_cleanup
                          @ [icopy l (CL_id (loop_var, (CT_fint 64)))
-                                  (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))]
+                                  (V_op (V_id (loop_var, CT_fint 64), (if is_inc then "+" else "-"), V_id (step_gs, CT_fint 64)))]
                          @ [igoto loop_start_label]);
                  ilabel loop_end_label])],
-     (fun clexp -> icopy l clexp unit_fragment),
+     (fun clexp -> icopy l clexp unit_cval),
      []
 
 and compile_block ctx = function
@@ -953,7 +956,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
     | before, I_aux (I_throw cval, (_, l)) :: after ->
        before
        @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
-          icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool true), CT_bool)]
+          icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))]
        @ generate_cleanup (historic @ before)
        @ [igoto end_block_label]
        @ rewrite_exception (historic @ before) after
@@ -966,7 +969,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        if has_effect effects BE_escape then
          before
          @ [funcall;
-            iif (F_id have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
+            iif (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
          @ rewrite_exception (historic @ before) after
        else
          before @ funcall :: rewrite_exception (historic @ before) after
@@ -1004,7 +1007,7 @@ let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp =
   | _ ->
      let apat = anf_pat pat in
      let gs = gensym () in
-     let destructure, cleanup, _ = compile_match ctx apat (F_id (name gs), ctyp) label in
+     let destructure, cleanup, _ = compile_match ctx apat (V_id (name gs, ctyp)) label in
      (gs, (destructure, cleanup))
 
 let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
@@ -1020,7 +1023,7 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
      let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in
      destructure
      @ [idecl (CT_tup ctyps) (name arg_id)]
-     @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (F_id (name id), ctyp)) new_ids,
+     @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (V_id (name id, ctyp))) new_ids,
      List.map (fun (id, _) -> id, ([], [])) new_ids,
      [iclear (CT_tup ctyps) (name arg_id)]
      @ cleanup
@@ -1242,7 +1245,7 @@ and compile_def' n total ctx = function
      let apat = anf_pat ~global:true pat in
      let gs = ngensym () in
      let end_label = label "let_end_" in
-     let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in
+     let destructure, destructure_cleanup, _ = compile_match ctx apat (V_id (gs, ctyp)) end_label in
      let gs_setup, gs_cleanup =
        [idecl ctyp gs], [iclear ctyp gs]
      in
@@ -1307,23 +1310,17 @@ let rec specialize_variants ctx prior =
        unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
 
        (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
-       let casts =
-         let cast_to_suprema (frag, ctyp) =
-           let suprema = ctyp_suprema ctyp in
-           if ctyp_equal ctyp suprema then
-             [], (unpoly frag, ctyp), []
-           else
-             let gs = ngensym () in
-             [idecl suprema gs;
-              icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
-             (F_id gs, suprema),
-             [iclear suprema gs]
-         in
-         List.map cast_to_suprema [cval]
+       let setup, cval, cleanup =
+         let suprema = ctyp_suprema (cval_ctyp cval) in
+         if ctyp_equal ctyp suprema then
+           [], unpoly cval, []
+         else
+           let gs = ngensym () in
+           [idecl suprema gs;
+            icopy l (CL_id (gs, suprema)) (unpoly cval)],
+           V_id (gs, suprema),
+           [iclear suprema gs]
        in
-       let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in
-       let cvals = List.map (fun (_, cval, _) -> cval) casts in
-       let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in
 
        let mk_funcall instr =
          if List.length setup = 0 then
@@ -1332,13 +1329,13 @@ let rec specialize_variants ctx prior =
            iblock (setup @ [instr] @ cleanup)
        in
 
-       mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux))
+       mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, [cval]), aux))
 
     | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
        Reporting.unreachable l __POS__ "Multiple argument constructor found"
 
     (* We have to be careful this is the only place where an F_ctor_kind can appear before calling specialize variants *)
-    | I_aux (I_jump ((F_ctor_kind (_, id, unifiers, pat_ctyp), CT_bool), _), _) as instr when Id.compare id ctor_id = 0 ->
+    | I_aux (I_jump (V_ctor_kind (_, id, unifiers, pat_ctyp), _), _) as instr when Id.compare id ctor_id = 0 ->
        let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
        unifications := Bindings.add mono_id (ctyp_suprema pat_ctyp) !unifications;
        instr
@@ -1354,10 +1351,9 @@ let rec specialize_variants ctx prior =
        let mono_id = append_id field_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
        unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
        I_aux (I_copy (CL_field (clexp, string_of_id mono_id), cval), aux)
-      
     | instr -> instr
   in
-  
+
   function
   | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
      let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
@@ -1406,12 +1402,12 @@ let rec specialize_variants ctx prior =
      let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) cdefs in
      let prior = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) prior in     
      specialize_variants ctx (CDEF_type (CTD_struct (struct_id, new_fields)) :: prior) cdefs
-     
-  | cdef :: cdefs ->
+
+ | cdef :: cdefs ->
      let remove_poly (I_aux (instr, aux)) =
        match instr with
-       | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp ->
-          I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux)
+       | I_copy (clexp, cval) when is_polymorphic (cval_ctyp cval) ->
+          I_aux (I_copy (clexp, unpoly cval), aux)
        | instr -> I_aux (instr, aux)
      in
      let cdef = cdef_map_instr remove_poly cdef in
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index f9829dfd..e0d7167f 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -55,7 +55,7 @@ open Jib_util
 let optimize_unit instrs =
   let unit_cval cval =
     match cval_ctyp cval with
-    | CT_unit -> (F_lit V_unit, CT_unit)
+    | CT_unit -> (V_lit (VL_unit, CT_unit))
     | _ -> cval
   in
   let unit_instr = function
@@ -152,21 +152,18 @@ let unique_per_function_ids cdefs =
   in
   List.mapi unique_cdef cdefs
 
-let rec frag_subst id subst = function
-  | F_id id' -> if Name.compare id id' = 0 then subst else F_id id'
-  | F_ref reg_id -> F_ref reg_id
-  | F_lit vl -> F_lit vl
-  | F_op (frag1, op, frag2) -> F_op (frag_subst id subst frag1, op, frag_subst id subst frag2)
-  | F_unary (op, frag) -> F_unary (op, frag_subst id subst frag)
-  | F_call (op, frags) -> F_call (op, List.map (frag_subst id subst) frags)
-  | F_field (frag, field) -> F_field (frag_subst id subst frag, field)
-  | F_tuple_member (frag, len, n) -> F_tuple_member (frag_subst id subst frag, len, n)
-  | F_raw str -> F_raw str
-  | F_ctor_kind (frag, ctor, unifiers, ctyp) -> F_ctor_kind (frag_subst id subst frag, ctor, unifiers, ctyp)
-  | F_ctor_unwrap (ctor, unifiers, frag) -> F_ctor_unwrap (ctor, unifiers, frag_subst id subst frag)
-  | F_poly frag -> F_poly (frag_subst id subst frag)
-
-let cval_subst id subst (frag, ctyp) = frag_subst id subst frag, ctyp
+let rec cval_subst id subst = function
+  | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp)
+  | V_ref (reg_id, ctyp) -> V_ref (reg_id, ctyp)
+  | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
+  | V_op (cval1, op, cval2) -> V_op (cval_subst id subst cval1, op, cval_subst id subst cval2)
+  | V_unary (op, cval) -> V_unary (op, cval_subst id subst cval)
+  | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals)
+  | V_field (cval, field) -> V_field (cval_subst id subst cval, field)
+  | V_tuple_member (cval, len, n) -> V_tuple_member (cval_subst id subst cval, len, n)
+  | V_ctor_kind (cval, ctor, unifiers, ctyp) -> V_ctor_kind (cval_subst id subst cval, ctor, unifiers, ctyp)
+  | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_subst id subst cval, unifiers, ctyp)
+  | V_poly (cval, ctyp) -> V_poly (cval_subst id subst cval, ctyp)
 
 let rec instrs_subst id subst =
   function
@@ -263,7 +260,7 @@ let inline cdefs should_inline instrs =
        | Some (None, ids, body) ->
           incr inlines;
           let inline_label = label "end_inline_" in
-          let body = List.fold_right2 instrs_subst (List.map name ids) (List.map fst args) body in
+          let body = List.fold_right2 instrs_subst (List.map name ids) args body in
           let body = List.map (map_instr fix_labels) body in
           let body = List.map (map_instr (replace_end inline_label)) body in
           let body = List.map (map_instr (replace_return clexp)) body in
@@ -288,3 +285,10 @@ let inline cdefs should_inline instrs =
       instrs
   in
   go instrs
+
+let rec remove_pointless_goto = function
+  | I_aux (I_goto label, _) :: I_aux (I_label label', aux) :: instrs when label = label' ->
+     I_aux (I_label label', aux) :: remove_pointless_goto instrs
+  | instr :: instrs ->
+     instr :: remove_pointless_goto instrs
+  | [] -> []
diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli
index 78759d08..e9f5cfcf 100644
--- a/src/jib/jib_optimize.mli
+++ b/src/jib/jib_optimize.mli
@@ -64,3 +64,6 @@ val flatten_cdef : cdef -> cdef
 val unique_per_function_ids : cdef list -> cdef list
 
 val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list
+
+(** Remove gotos immediately followed by the label it jumps to *)
+val remove_pointless_goto : instr list -> instr list
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 01240754..810f1ed6 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -56,17 +56,17 @@ let bvint sz x =
 let smt_value vl ctyp =
   let open Value2 in
   match vl, ctyp with
-  | V_bits bs, _ ->
+  | VL_bits (bs, true), _ ->
      begin match Sail2_values.hexstring_of_bits bs with
      | Some s -> Hex (Xstring.implode s)
      | None -> Bin (Xstring.implode (List.map Sail2_values.bitU_char bs))
      end
-  | V_bool b, _ -> Bool_lit b
-  | V_int n, CT_constant m -> bvint (required_width n) (Big_int.to_int n)
-  | V_int n, CT_fint sz -> bvint sz (Big_int.to_int n)
-  | V_bit Sail2_values.B0, CT_bit -> Bin "0"
-  | V_bit Sail2_values.B1, CT_bit -> Bin "1"
-  | V_unit, _ -> Var "unit"
+  | VL_bool b, _ -> Bool_lit b
+  | VL_int n, CT_constant m -> bvint (required_width n) (Big_int.to_int n)
+  | VL_int n, CT_fint sz -> bvint sz (Big_int.to_int n)
+  | VL_bit Sail2_values.B0, CT_bit -> Bin "0"
+  | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
+  | VL_unit, _ -> Var "unit"
 
   | vl, _ -> failwith ("Bad literal " ^ string_of_value vl)
 
@@ -79,30 +79,26 @@ let zencode_ctor ctor_id unifiers =
 
 let rec smt_cval env cval =
   match cval with
-  | F_lit vl, ctyp -> smt_value vl ctyp
-  | frag, _ -> smt_fragment env frag
-
-and smt_fragment env frag =
-  match frag with
-  | F_id (Name (id, _) as ssa_id) ->
+  | V_lit (vl, ctyp) -> smt_value vl ctyp
+  | V_id (Name (id, _) as ssa_id, _) ->
      begin match Type_check.Env.lookup_id id env with
      | Enum _ -> Var (zencode_id id)
      | _ -> Var (zencode_name ssa_id)
      end
-  | F_id ssa_id -> Var (zencode_name ssa_id)
-  | F_op (frag1, "!=", frag2) ->
-     Fn ("not", [Fn ("=", [smt_fragment env frag1; smt_fragment env frag2])])
-  | F_unary ("!", frag) ->
-     Fn ("not", [smt_cval env (frag, CT_bool)])
-  | F_ctor_kind (union, ctor_id, unifiers, _) ->
-     Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_fragment env union)])
-  | F_ctor_unwrap (ctor_id, unifiers, union) ->
-     Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_fragment env union])
-  | F_field (union, field) ->
-     Fn ("un" ^ field, [smt_fragment env union])
-  | F_tuple_member (frag, len, n) ->
-     Fn (Printf.sprintf "tup_%d_%d" len n, [smt_fragment env frag])
-  | frag -> failwith ("Unrecognised fragment " ^ string_of_fragment ~zencode:false frag)
+  | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
+  | V_op (frag1, "!=", frag2) ->
+     Fn ("not", [Fn ("=", [smt_cval env frag1; smt_cval env frag2])])
+  | V_unary ("!", cval) ->
+     Fn ("not", [smt_cval env cval])
+  | V_ctor_kind (union, ctor_id, unifiers, _) ->
+     Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval env union)])
+  | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
+     Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval env union])
+  | V_field (union, field) ->
+     Fn (field, [smt_cval env union])
+  | V_tuple_member (frag, len, n) ->
+     Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval env frag])
+  | cval -> failwith ("Unrecognised cval " ^ string_of_cval ~zencode:false cval)
 
 let builtin_zeros env cval = function
   | CT_fbits (n, _) -> bvzero n
@@ -140,8 +136,8 @@ let int_size = function
    exactly esz bits. *)
 let bvzeint env esz cval =
   let sz = int_size (cval_ctyp cval) in
-  match fst cval with
-  | F_lit (V_int n) ->
+  match cval with
+  | V_lit (VL_int n, _) ->
      bvint esz (Big_int.to_int n)
   | _ ->
      let smt = smt_cval env cval in
@@ -239,7 +235,14 @@ let builtin_unsigned env v ret_ctyp =
      let smt = smt_cval env v in
      Fn ("concat", [bvzero (m - n); smt])
 
-  | _ -> failwith "Cannot compile unsigned"
+  | CT_fbits (n, _), CT_lint ->
+     if n >= !lint_size then
+       failwith "Overflow detected"
+     else
+       let smt = smt_cval env v in
+       Fn ("concat", [bvzero (!lint_size - n); smt])
+
+  | ctyp, _ -> failwith (Printf.sprintf "Cannot compile unsigned : %s -> %s" (string_of_ctyp ctyp) (string_of_ctyp ret_ctyp))
 
 let builtin_eq_int env v1 v2 =
   match cval_ctyp v1, cval_ctyp v2 with
@@ -256,6 +259,18 @@ let builtin_add_bits env v1 v2 ret_ctyp =
 
   | _ -> failwith "Cannot compile add_bits"
 
+let builtin_replicate_bits env v1 v2 ret_ctyp =
+  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
+  | CT_fbits (n, _), CT_constant c, CT_fbits (m, _) ->
+     assert (n * Big_int.to_int c = m);
+     let smt = smt_cval env v1 in
+     Fn ("concat", List.init (Big_int.to_int c) (fun _ -> smt))
+
+  | _ -> failwith "Cannot compile replicate_bits"
+
+let builtin_lt env v1 v2 =
+  Fn ("bvult", [smt_cval env v1; smt_cval env v2])
+
 let smt_primop env name args ret_ctyp =
   match name, args, ret_ctyp with
   | "eq_bits", [v1; v2], _ ->
@@ -266,8 +281,13 @@ let smt_primop env name args ret_ctyp =
      let smt1 = smt_cval env v1 in
      let smt2 = smt_cval env v2 in
      Fn ("=", [smt1; smt2])
+  | "eq_anything", [v1; v2], _ ->
+     let smt1 = smt_cval env v1 in
+     let smt2 = smt_cval env v2 in
+     Fn ("=", [smt1; smt2])
 
   | "not", [v], _ -> Fn ("not", [smt_cval env v])
+  | "lt", [v1; v2], _ -> builtin_lt env v1 v2
 
   | "zeros", [v1], _ -> builtin_zeros env v1 ret_ctyp
   | "zero_extend", [v1; v2], _ -> builtin_zero_extend env v1 v2 ret_ctyp
@@ -281,9 +301,10 @@ let smt_primop env name args ret_ctyp =
   | "vector_access", [v1; v2], ret_ctyp -> builtin_vector_access env v1 v2 ret_ctyp
   | "vector_subrange", [v1; v2; v3], ret_ctyp -> builtin_vector_subrange env v1 v2 v3 ret_ctyp
   | "sail_unsigned", [v], ret_ctyp -> builtin_unsigned env v ret_ctyp
+  | "replicate_bits", [v1; v2], ret_ctyp -> builtin_replicate_bits env v1 v2 ret_ctyp
   | "eq_int", [v1; v2], _ -> builtin_eq_int env v1 v2
 
-  | _ -> failwith ("Bad primop " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map snd args) ^ " -> " ^ string_of_ctyp ret_ctyp)
+  | _ -> failwith ("Bad primop " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
 
 let rec smt_conversion from_ctyp to_ctyp x =
   match from_ctyp, to_ctyp with
@@ -441,22 +462,22 @@ let hex_char =
   | 'F' | 'f' -> [B1; B1; B1; B1]
   | _ -> failwith "Invalid hex character"
 
-let literal_to_fragment (L_aux (l_aux, _) as lit) =
+let literal_to_cval (L_aux (l_aux, _) as lit) =
   match l_aux with
-  | L_num n -> Some (F_lit (V_int n), CT_constant n)
+  | L_num n -> Some (V_lit (VL_int n, CT_constant n))
   | L_hex str when String.length str <= 16 ->
      let content = Util.string_to_list str |> List.map hex_char |> List.concat in
-     Some (F_lit (V_bits content), CT_fbits (String.length str * 4, true))
-  | L_unit -> Some (F_lit V_unit, CT_unit)
-  | L_true -> Some (F_lit (V_bool true), CT_bool)
-  | L_false -> Some (F_lit (V_bool false), CT_bool)
+     Some (V_lit (VL_bits (content, true), CT_fbits (String.length str * 4, true)))
+  | L_unit -> Some (V_lit (VL_unit, CT_unit))
+  | L_true -> Some (V_lit (VL_bool true, CT_bool))
+  | L_false -> Some (V_lit (VL_bool false, CT_bool))
   | _ -> None
 
 let c_literals ctx =
   let rec c_literal env l = function
     | AV_lit (lit, typ) as v ->
-       begin match literal_to_fragment lit with
-       | Some (frag, ctyp) -> AV_C_fragment (frag, typ, ctyp)
+       begin match literal_to_cval lit with
+       | Some cval -> AV_cval (cval, typ)
        | None -> v
        end
     | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
@@ -533,6 +554,7 @@ let rec rmw_write = function
   | CL_rmw (_, write, ctyp) -> write, ctyp
   | CL_id _ -> assert false
   | CL_tuple (clexp, _) -> rmw_write clexp
+  | CL_field (clexp, _) -> rmw_write clexp
   | clexp ->
      failwith (Pretty_print_sail.to_string (pp_clexp clexp))
 
@@ -556,6 +578,20 @@ let rmw_modify smt = function
      | _ ->
         failwith "Tuple modify does not have tuple type"
      end
+  | CL_field (clexp, field) ->
+     let ctyp = clexp_ctyp clexp in
+     begin match ctyp with
+     | CT_struct (struct_id, fields) ->
+        let set_field (field', _) =
+          if Util.zencode_string field = zencode_id field' then
+            smt
+          else
+            Fn (zencode_id field', [Var (rmw_read clexp)])
+        in
+        Fn (zencode_upper_id struct_id, List.map set_field fields)
+     | _ ->
+        failwith "Struct modify does not have struct type"
+     end
   | _ -> assert false
 
 (* For a basic block (contained in a control-flow node / cfnode), we
@@ -637,6 +673,7 @@ let smt_cdef out_chan env all_cdefs = function
           (* |> optimize_unit *)
           |> inline all_cdefs (fun _ -> true)
           |> flatten_instrs
+          |> remove_pointless_goto
         in
 
         let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index e79c88a1..79c5910e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -191,7 +191,7 @@ type cf_node =
   | CF_guard of cval
   | CF_start of ctyp NameMap.t
 
-let cval_not (f, ctyp) = (F_unary ("!", f), ctyp)
+let cval_not cval = V_unary ("!", cval)
 
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
@@ -494,23 +494,22 @@ let rename_variables graph root children =
     stacks := NameMap.add id (n :: match NameMap.find_opt id !stacks with Some s -> s | None -> []) !stacks
   in
 
-  let rec fold_frag = function
-    | F_id id ->
+  let rec fold_cval = function
+    | V_id (id, ctyp) ->
        let i = top_stack id in
-       F_id (ssa_name i id)
-    | F_ref id ->
+       V_id (ssa_name i id, ctyp)
+    | V_ref (id, ctyp) ->
        let i = top_stack id in
-       F_ref (ssa_name i id)
-    | F_lit vl -> F_lit vl
-    | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2)
-    | F_unary (op, f) -> F_unary (op, fold_frag f)
-    | F_call (id, fs) -> F_call (id, List.map fold_frag fs)
-    | F_field (f, field) -> F_field (fold_frag f, field)
-    | F_tuple_member (f, len, n) -> F_tuple_member (fold_frag f, len, n)
-    | F_raw str -> F_raw str
-    | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (fold_frag f, ctor, unifiers, ctyp)
-    | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, fold_frag f)
-    | F_poly f -> F_poly (fold_frag f)
+       V_ref (ssa_name i id, ctyp)
+    | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
+    | V_op (f1, op, f2) -> V_op (fold_cval f1, op, fold_cval f2)
+    | V_unary (op, f) -> V_unary (op, fold_cval f)
+    | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
+    | V_field (f, field) -> V_field (fold_cval f, field)
+    | V_tuple_member (f, len, n) -> V_tuple_member (fold_cval f, len, n)
+    | V_ctor_kind (f, ctor, unifiers, ctyp) -> V_ctor_kind (fold_cval f, ctor, unifiers, ctyp)
+    | V_ctor_unwrap (ctor, f, unifiers, ctyp) -> V_ctor_unwrap (ctor, fold_cval f, unifiers, ctyp)
+    | V_poly (f, ctyp) -> V_poly (fold_cval f, ctyp)
   in
 
   let rec fold_clexp rmw = function
@@ -532,8 +531,6 @@ let rename_variables graph root children =
     | CL_void -> CL_void
   in
 
-  let fold_cval (f, ctyp) = (fold_frag f, ctyp) in
-
   let ssa_instr (I_aux (aux, annot)) =
     let aux = match aux with
       | I_funcall (clexp, extern, id, args) ->
@@ -685,7 +682,7 @@ let string_of_ssainstr = function
   | Phi (id, ctyp, args) ->
      string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = &phi;(" ^ Util.string_of_list ", " string_of_name args ^ ")"
   | Pi cvals ->
-     "&pi;(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")"
+     "&pi;(" ^ Util.string_of_list ", " (fun v -> String.escaped (string_of_cval ~zencode:false v)) cvals ^ ")"
 
 let string_of_phis = function
   | [] -> ""
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 2eabdc57..343c8cb5 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -154,27 +154,30 @@ let return = Return (-1)
 
 let name id = Name (id, -1)
 
-let rec frag_rename from_id to_id = function
-  | F_id id when Name.compare id from_id = 0 -> F_id to_id
-  | F_id id -> F_id id
-  | F_ref id when Name.compare id from_id = 0 -> F_ref to_id
-  | F_ref id -> F_ref id
-  | F_lit v -> F_lit v
-  | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags)
-  | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2)
-  | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
-  | F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
-  | F_tuple_member (f, len, n) -> F_tuple_member (frag_rename from_id to_id f, len, n)
-  | F_raw raw -> F_raw raw
-  | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (frag_rename from_id to_id f, ctor, unifiers, ctyp)
-  | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, frag_rename from_id to_id f)
-  | F_poly f -> F_poly (frag_rename from_id to_id f)
-
-let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
+let rec cval_rename from_id to_id = function
+  | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp)
+  | V_id (id, ctyp) -> V_id (id, ctyp)
+  | V_ref (id, ctyp) when Name.compare id from_id = 0 -> V_ref (to_id, ctyp)
+  | V_ref (id, ctyp) -> V_ref (id, ctyp)
+  | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
+  | V_call (call, cvals) -> V_call (call, List.map (cval_rename from_id to_id) cvals)
+  | V_op (f1, op, f2) -> V_op (cval_rename from_id to_id f1, op, cval_rename from_id to_id f2)
+  | V_unary (op, f) -> V_unary (op, cval_rename from_id to_id f)
+  | V_field (f, field) -> V_field (cval_rename from_id to_id f, field)
+  | V_tuple_member (f, len, n) -> V_tuple_member (cval_rename from_id to_id f, len, n)
+  | V_ctor_kind (f, ctor, unifiers, ctyp) -> V_ctor_kind (cval_rename from_id to_id f, ctor, unifiers, ctyp)
+  | V_ctor_unwrap (ctor, f, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_rename from_id to_id f, unifiers, ctyp)
+  | V_hd cval -> V_hd (cval_rename from_id to_id cval)
+  | V_tl cval -> V_tl (cval_rename from_id to_id cval)
+  | V_poly (f, ctyp) -> V_poly (cval_rename from_id to_id f, ctyp)
 
 let rec clexp_rename from_id to_id = function
   | CL_id (id, ctyp) when Name.compare id from_id = 0 -> CL_id (to_id, ctyp)
   | CL_id (id, ctyp) -> CL_id (id, ctyp)
+  | CL_rmw (read, write, ctyp) ->
+     CL_rmw ((if Name.compare read from_id = 0 then to_id else read),
+             (if Name.compare write from_id = 0 then to_id else write),
+             ctyp)
   | CL_field (clexp, field) ->
      CL_field (clexp_rename from_id to_id clexp, field)
   | CL_addr clexp ->
@@ -247,17 +250,18 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
 (**************************************************************************)
 
 let string_of_value = function
-  | V_bits [] -> "UINT64_C(0)"
-  | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
-  | V_int i -> Big_int.to_string i ^ "l"
-  | V_bool true -> "true"
-  | V_bool false -> "false"
-  | V_null -> "NULL"
-  | V_unit -> "UNIT"
-  | V_bit Sail2_values.B0 -> "UINT64_C(0)"
-  | V_bit Sail2_values.B1 -> "UINT64_C(1)"
-  | V_bit Sail2_values.BU -> failwith "Undefined bit found in value"
-  | V_string str -> "\"" ^ str ^ "\""
+  | VL_bits ([], _) -> "UINT64_C(0)"
+  | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
+  | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
+  | VL_int i -> Big_int.to_string i ^ "l"
+  | VL_bool true -> "true"
+  | VL_bool false -> "false"
+  | VL_null -> "NULL"
+  | VL_unit -> "UNIT"
+  | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
+  | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
+  | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
+  | VL_string str -> "\"" ^ str ^ "\""
 
 let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
   let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in
@@ -273,40 +277,43 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
   | Current_exception n ->
      "current_exception" ^ ssa_num n
 
-let rec string_of_fragment ?zencode:(zencode=true) = function
-  | F_id id -> string_of_name ~zencode:zencode id
-  | F_ref id -> "&" ^ string_of_name ~zencode:zencode id
-  | F_lit v -> string_of_value v
-  | F_call (str, frags) ->
-     Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags)
-  | F_field (f, field) ->
-     Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field
-  | F_tuple_member (f, _, n) ->
-     Printf.sprintf "%s.ztup%d" (string_of_fragment' ~zencode:zencode f) n
-  | F_op (f1, op, f2) ->
-     Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2)
-  | F_unary (op, f) ->
-     op ^ string_of_fragment' ~zencode:zencode f
-  | F_raw raw -> raw
-  | F_ctor_kind (f, ctor, [], _) ->
-     string_of_fragment' ~zencode:zencode f ^ ".kind"
+let rec string_of_cval ?zencode:(zencode=true) = function
+  | V_id (id, _) -> string_of_name ~zencode:zencode id
+  | V_ref (id, _) -> "&" ^ string_of_name ~zencode:zencode id
+  | V_lit (vl, _) -> string_of_value vl
+  | V_call (str, cvals) ->
+     Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_cval ~zencode:zencode) cvals)
+  | V_field (f, field) ->
+     Printf.sprintf "%s.%s" (string_of_cval' ~zencode:zencode f) field
+  | V_tuple_member (f, _, n) ->
+     Printf.sprintf "%s.ztup%d" (string_of_cval' ~zencode:zencode f) n
+  | V_op (f1, op, f2) ->
+     Printf.sprintf "%s %s %s" (string_of_cval' ~zencode:zencode f1) op (string_of_cval' ~zencode:zencode f2)
+  | V_unary (op, f) ->
+     op ^ string_of_cval' ~zencode:zencode f
+  | V_hd f ->
+     Printf.sprintf "(%s).hd" ("*" ^ string_of_cval' ~zencode:zencode f)
+  | V_tl f ->
+     Printf.sprintf "(%s).tl" ("*" ^ string_of_cval' ~zencode:zencode f)
+  | V_ctor_kind (f, ctor, [], _) ->
+     string_of_cval' ~zencode:zencode f ^ ".kind"
      ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor)
-  | F_ctor_kind (f, ctor, unifiers, _) ->
-     string_of_fragment' ~zencode:zencode f ^ ".kind"
+  | V_ctor_kind (f, ctor, unifiers, _) ->
+     string_of_cval' ~zencode:zencode f ^ ".kind"
      ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
-  | F_ctor_unwrap (ctor, [], f) ->
+  | V_ctor_unwrap (ctor, f, [], _) ->
      Printf.sprintf "%s.%s"
-       (string_of_fragment' ~zencode:zencode f)
+       (string_of_cval' ~zencode:zencode f)
        (Util.zencode_string (string_of_id ctor))
-  | F_ctor_unwrap (ctor, unifiers, f) ->
+  | V_ctor_unwrap (ctor, f, unifiers, _) ->
      Printf.sprintf "%s.%s"
-       (string_of_fragment' ~zencode:zencode f)
+       (string_of_cval' ~zencode:zencode f)
        (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
-  | F_poly f -> string_of_fragment ~zencode:zencode f
-and string_of_fragment' ?zencode:(zencode=true) f =
+  | V_poly (f, _) -> string_of_cval ~zencode:zencode f
+and string_of_cval' ?zencode:(zencode=true) f =
   match f with
-  | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")"
-  | _ -> string_of_fragment ~zencode:zencode f
+  | V_op _ | V_unary _ -> "(" ^ string_of_cval ~zencode:zencode f ^ ")"
+  | _ -> string_of_cval ~zencode:zencode f
 
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
@@ -519,12 +526,12 @@ let rec ctyp_ids = function
     | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
 
 let rec unpoly = function
-  | F_poly f -> unpoly f
-  | F_call (call, fs) -> F_call (call, List.map unpoly fs)
-  | F_field (f, field) -> F_field (unpoly f, field)
-  | F_op (f1, op, f2) -> F_op (unpoly f1, op, unpoly f2)
-  | F_unary (op, f) -> F_unary (op, unpoly f)
-  | f -> f
+  | V_poly (cval, _) -> unpoly cval
+  | V_call (call, cvals) -> V_call (call, List.map unpoly cvals)
+  | V_field (cval, field) -> V_field (unpoly cval, field)
+  | V_op (cval1, op, cval2) -> V_op (unpoly cval1, op, unpoly cval2)
+  | V_unary (op, cval) -> V_unary (op, unpoly cval)
+  | cval -> cval
 
 let rec is_polymorphic = function
   | CT_lint | CT_fint _ | CT_constant _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
@@ -546,8 +553,8 @@ let pp_ctyp ctyp =
 let pp_keyword str =
   string ((str |> Util.red |> Util.clear) ^ " ")
 
-let pp_cval (frag, ctyp) =
-  string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp
+let pp_cval cval =
+  string (string_of_cval ~zencode:false cval)
 
 let rec pp_clexp = function
   | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp
@@ -654,17 +661,15 @@ let pp_cdef = function
      ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
      ^^ hardline
 
-let rec fragment_deps = function
-  | F_id id | F_ref id -> NameSet.singleton id
-  | F_lit _ -> NameSet.empty
-  | F_field (frag, _) | F_unary (_, frag) | F_poly frag | F_tuple_member (frag, _, _) -> fragment_deps frag
-  | F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags)
-  | F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2)
-  | F_ctor_kind (frag, _, _, _) -> fragment_deps frag
-  | F_ctor_unwrap (_, _, frag) -> fragment_deps frag
-  | F_raw _ -> NameSet.empty
-
-let cval_deps = function (frag, _) -> fragment_deps frag
+let rec cval_deps = function
+  | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id
+  | V_lit _ -> NameSet.empty
+  | V_field (cval, _) | V_unary (_, cval) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval
+  | V_call (_, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals)
+  | V_op (cval1, _, cval2) -> NameSet.union (cval_deps cval1) (cval_deps cval2)
+  | V_ctor_kind (cval, _, _, _) -> cval_deps cval
+  | V_ctor_unwrap (_, cval, _, _) -> cval_deps cval
+  | V_hd cval | V_tl cval -> cval_deps cval
 
 let rec clexp_deps = function
   | CL_id (id, _) -> NameSet.empty, NameSet.singleton id
@@ -730,24 +735,47 @@ let rec map_clexp_ctyp f = function
   | CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp)
   | CL_void -> CL_void
 
+let rec map_cval_ctyp f = function
+  | V_id (id, ctyp) -> V_id (id, f ctyp)
+  | V_ref (id, ctyp) -> V_ref (id, f ctyp)
+  | V_lit (vl, ctyp) -> V_lit (vl, f ctyp)
+  | V_ctor_kind (cval, id, unifiers, ctyp) ->
+     V_ctor_kind (map_cval_ctyp f cval, id, List.map f unifiers, f ctyp)
+  | V_ctor_unwrap (id, cval, unifiers, ctyp) ->
+     V_ctor_unwrap (id, map_cval_ctyp f cval, List.map f unifiers, f ctyp)
+  | V_op (cval1, op, cval2) ->
+     V_op (map_cval_ctyp f cval1, op, map_cval_ctyp f cval2)
+  | V_tuple_member (cval, i, j) ->
+     V_tuple_member (map_cval_ctyp f cval, i, j)
+  | V_unary (op, cval) ->
+     V_unary (op, map_cval_ctyp f cval)
+  | V_call (op, cvals) ->
+     V_call (op, List.map (map_cval_ctyp f) cvals)
+  | V_field (cval, field) ->
+     V_field (map_cval_ctyp f cval, field)
+  | V_hd cval -> V_hd (map_cval_ctyp f cval)
+  | V_tl cval -> V_tl (map_cval_ctyp f cval)
+  | V_poly (cval, ctyp) -> V_poly (map_cval_ctyp f cval, f ctyp)
+
+
 let rec map_instr_ctyp f (I_aux (instr, aux)) =
   let instr = match instr with
     | I_decl (ctyp, id) -> I_decl (f ctyp, id)
-    | I_init (ctyp1, id, (frag, ctyp2)) -> I_init (f ctyp1, id, (frag, f ctyp2))
-    | I_if ((frag, ctyp1), then_instrs, else_instrs, ctyp2) ->
-       I_if ((frag, f ctyp1), List.map (map_instr_ctyp f) then_instrs, List.map (map_instr_ctyp f) else_instrs, f ctyp2)
-    | I_jump ((frag, ctyp), label) -> I_jump ((frag, f ctyp), label)
+    | I_init (ctyp, id, cval) -> I_init (f ctyp, id, map_cval_ctyp f cval)
+    | I_if (cval, then_instrs, else_instrs, ctyp) ->
+       I_if (map_cval_ctyp f cval, List.map (map_instr_ctyp f) then_instrs, List.map (map_instr_ctyp f) else_instrs, f ctyp)
+    | I_jump (cval, label) -> I_jump (map_cval_ctyp f cval, label)
     | I_funcall (clexp, extern, id, cvals) ->
-       I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (fun (frag, ctyp) -> frag, f ctyp) cvals)
-    | I_copy (clexp, (frag, ctyp)) -> I_copy (map_clexp_ctyp f clexp, (frag, f ctyp))
+       I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (map_cval_ctyp f) cvals)
+    | I_copy (clexp, cval) -> I_copy (map_clexp_ctyp f clexp, map_cval_ctyp f cval)
     | I_clear (ctyp, id) -> I_clear (f ctyp, id)
-    | I_return (frag, ctyp) -> I_return (frag, f ctyp)
+    | I_return cval -> I_return (map_cval_ctyp f cval)
     | I_block instrs -> I_block (List.map (map_instr_ctyp f) instrs)
     | I_try_block instrs -> I_try_block (List.map (map_instr_ctyp f) instrs)
-    | I_throw (frag, ctyp) -> I_throw (frag, f ctyp)
+    | I_throw cval -> I_throw (map_cval_ctyp f cval)
     | I_undefined ctyp -> I_undefined (f ctyp)
     | I_reset (ctyp, id) -> I_reset (f ctyp, id)
-    | I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2))
+    | I_reinit (ctyp, id, cval) -> I_reinit (f ctyp, id, map_cval_ctyp f cval)
     | I_end id -> I_end id
     | (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr
   in
@@ -854,7 +882,57 @@ let label str =
   incr label_counter;
   str
 
-let cval_ctyp = function (_, ctyp) -> ctyp
+let rec infer_unary v = function
+  | "!" -> CT_bool
+  | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Could not infer unary " ^ op)
+
+and infer_op v1 v2 = function
+  | "==" -> CT_bool
+  | "!=" -> CT_bool
+  | ">=" -> CT_bool
+  | "<=" -> CT_bool
+  | ">" -> CT_bool
+  | "<" -> CT_bool
+  | "+" -> cval_ctyp v1
+  | "-" -> cval_ctyp v1
+  | "|" -> cval_ctyp v1
+  | "&" -> cval_ctyp v1
+  | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot infer binary op: " ^ op)
+
+and infer_call vs = function
+  | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot infer call: " ^ op)
+
+and cval_ctyp = function
+  | V_id (_, ctyp) -> ctyp
+  | V_ref (_, ctyp) -> CT_ref ctyp
+  | V_lit (vl, ctyp) -> ctyp
+  | V_ctor_kind _ -> CT_bool
+  | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> ctyp
+  | V_hd v ->
+     begin match cval_ctyp v with
+     | CT_list ctyp -> ctyp
+     | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Invalid list type " ^ full_string_of_ctyp ctyp)
+     end
+  | V_tl v -> cval_ctyp v
+  | V_op (v1, op, v2) -> infer_op v1 v2 op
+  | V_unary (op, v) -> infer_unary v op
+  | V_poly (_, ctyp) -> ctyp
+  | V_tuple_member (cval, _, n) ->
+     begin match cval_ctyp cval with
+     | CT_tup ctyps ->
+        List.nth ctyps n
+     | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Invalid tuple type " ^ full_string_of_ctyp ctyp)
+     end
+  | V_field (cval, field) ->
+     begin match cval_ctyp cval with
+     | CT_struct (id, ctors) ->
+        begin
+          try snd (List.find (fun (id, ctyp) -> Util.zencode_string (string_of_id id) = field) ctors) with
+          | Not_found -> failwith ("Struct type " ^ string_of_id id ^ " does not have a constructor " ^ field)
+        end
+     | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Inavlid type for V_field " ^ full_string_of_ctyp ctyp)
+     end
+  | V_call (op, vs) -> infer_call vs op
 
 let rec clexp_ctyp = function
   | CL_id (_, ctyp) -> ctyp
diff --git a/src/util.ml b/src/util.ml
index 703bbc1f..5ef9686d 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -158,7 +158,7 @@ let rec assoc_compare_opt cmp k l =
   match l with
     | [] -> None
     | (k',v)::l -> if cmp k k' = 0 then Some v else assoc_compare_opt cmp k l
-                 
+
 let rec compare_list f l1 l2 = 
   match (l1,l2) with
     | ([],[]) -> 0
diff --git a/src/value2.lem b/src/value2.lem
index caf355b7..0e65e91f 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -53,10 +53,10 @@ open import Pervasives
 open import Sail2_values
 
 type vl =
-  | V_bits of list bitU
-  | V_bit of bitU
-  | V_bool of bool
-  | V_unit
-  | V_int of integer
-  | V_string of string
-  | V_null (* Used for unitialized values and null pointers in C compilation *)
+  | VL_bits of list bitU * bool
+  | VL_bit of bitU
+  | VL_bool of bool
+  | VL_unit
+  | VL_int of integer
+  | VL_string of string
+  | VL_null (* Used for unitialized values and null pointers in C compilation *)