diff --git a/hol/cake_export/Holmakefile b/hol/cake_export/Holmakefile
index e2322a6..7390789 100644
--- a/hol/cake_export/Holmakefile
+++ b/hol/cake_export/Holmakefile
@@ -10,7 +10,9 @@ DEPENDENCIES   = .. \
  $(CAKEMLDIR)/basis/pure \
  $(CAKEMLDIR)/basis \
  $(CAKEMLDIR)/translator \
- $(CAKEMLDIR)/characteristic
+ $(CAKEMLDIR)/characteristic \
+ $(CAKEMLDIR)/compiler/parsing \
+ $(CAKEMLDIR)/unverified/sexpr-bootstrap
 
 # configuration
 # ----------------------------------
diff --git a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml
index 61ec6a0..45bcdfc 100644
--- a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml
+++ b/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml
@@ -127,6 +127,17 @@ Definition arch_exec'_def:
 (arch_exec' _ _ = NONE)
 End
 
+Definition arch_multi_exec'_def:
+ (arch_multi_exec' actx (aenv, g_scope_list, arch_frame_list, status) 0 =
+  SOME (aenv, g_scope_list, arch_frame_list, status))
+  /\
+ (arch_multi_exec' actx (aenv, g_scope_list, arch_frame_list, status) (SUC fuel) =
+  case arch_exec' actx (aenv, g_scope_list, arch_frame_list, status) of
+  | SOME (aenv', g_scope_list', arch_frame_list', status') =>
+   arch_multi_exec' actx (aenv', g_scope_list', arch_frame_list', status') fuel
+  | NONE => NONE)
+End
+
 
 val _ = translation_extends "p4_exec_sem_frames_cakeProg";
 
@@ -144,6 +155,8 @@ val _ = translate set_fin_status_def;
 
 val _ = translate arch_exec'_def;
 
+val _ = translate arch_multi_exec'_def;
+
 val _ = ml_prog_update (close_module NONE);
 
 val _ = export_theory ();
diff --git a/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml
index f94449e..9906722 100644
--- a/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml
+++ b/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml
@@ -136,46 +136,6 @@ Termination
  METIS_TAC [v1_size_mem]
 End
 
-Definition slice'_def:
- slice' (v, n) (vec1, len1) (vec2, len2) =
-  let hi = v2n vec1 in
-  let lo = v2n vec2 in
-  if lo <= hi /\ hi < n /\ LENGTH v = n
-  then
-   SOME $ bitv_bitslice (v, n) (v2n vec1) (v2n vec2)
-  else NONE
-End
-
-Definition slice_lval'_def:
- slice_lval' v e1 e2 =
-  case v of
-  | (v_bit (v, bl)) =>
-   (case e1 of
-    | (e_v (v_bit (v1, bl1))) =>
-     (case e2 of
-      | (e_v (v_bit (v2, bl2))) =>
-       (case slice' (v, bl) (v1, bl1) (v2, bl2) of
-        | SOME bitv => SOME $ v_bit bitv
-        | NONE => NONE)
-      | _ => NONE)
-    | _ => NONE)
-  | _ => NONE
-End
-
-Definition lookup_lval'_def:
- (lookup_lval' (ss:scope list) (lval_varname x) = lookup_v ss x) /\
- (lookup_lval' ss (lval_field lval f) =
-  case lookup_lval' ss lval of
-  | SOME v => acc_f v f
-  | NONE => NONE) /\
- (lookup_lval' ss (lval_slice lval e1 e2) =
-  case lookup_lval' ss lval of
-   | SOME (v_bit (v, bl)) => slice_lval' (v_bit (v, bl)) e1 e2
-   | _ => NONE) /\
- (lookup_lval' ss lval_null = NONE ) /\
- (lookup_lval' ss (lval_paren lval) = lookup_lval' ss lval) 
-End
-
 
 Definition one_arg_val_for_newscope'_def:
  one_arg_val_for_newscope' d e ss =
@@ -1030,25 +990,4 @@ val _ = translate e_exec'_def;
 
 val _ = ml_prog_update (close_module NONE);
 
-(*
-(* To print the resulting CakeML program *)
-fun get_current_prog () =
-  let
-    val state = get_ml_prog_state ()
-    val state_thm =
-     state |> ml_progLib.remove_snocs
-           |> ml_progLib.clean_state
-           |> get_thm
-  in
-    state_thm |> concl |> strip_comb |> #2 |> el 2
-  end
-;
-
-val _ = astPP.enable_astPP();
-
-val _ = print_term (get_current_prog ());
-
-val _ = astPP.disable_astPP();
-*)
-
 val _ = export_theory ();
diff --git a/hol/cake_export/p4_exec_sem_stmt_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_stmt_cakeProgScript.sml
index 0c61f50..31b4272 100644
--- a/hol/cake_export/p4_exec_sem_stmt_cakeProgScript.sml
+++ b/hol/cake_export/p4_exec_sem_stmt_cakeProgScript.sml
@@ -46,62 +46,6 @@ Definition declare_list_in_fresh_scope'_def:
   MAP (\(x, (t, lvalop)). (x, (init_v_from_tau_cake t, NONE))) t_scope
 End
 
-(* Puts the bits in bl1 between index hi and lo of bl2. *)
-Definition replace_bits_def:
- replace_bits (bl1, (n1:num)) (bl2,n2) hi lo =
-  if lo <= hi /\ hi < n2 /\ LENGTH bl2 = n2
-  then
-   SOME $ (SEG (n2-(hi+1)) 0 bl2) ++ bl1 ++ (SEG lo (n2-lo) bl2)
-  else NONE
-End
-
-Definition assign_to_slice'_def:
- assign_to_slice' vb vb' ev1 ev2 =
-  (case ev1 of
-   | (e_v (v_bit (bl1, n1))) =>
-    (case ev2 of
-     | (e_v (v_bit (bl2, n2))) =>
-      (case replace_bits vb vb' (v2n bl1) (v2n bl2) of
-       | SOME bitv =>
-        SOME $ v_bit (bitv, SND vb')
-       | NONE => NONE)
-     | _ => NONE)
-   | _ => NONE)
-End
-
-Definition assign'_def:
- (assign' ss v (lval_varname x) =
-  case find_topmost_map ss x of
-  | SOME (i, sc) =>
-   (case lookup_out ss x of
-    | SOME str_opt =>
-      SOME (LUPDATE (AUPDATE sc (x, (v, str_opt))) i ss)
-    | NONE => NONE)
-  | _ => NONE) /\
- (assign' ss v (lval_field lval f) =
-  case lookup_lval' ss lval of
-  | SOME (v_struct f_v_l) =>
-   (case INDEX_OF f (MAP FST f_v_l) of
-    | SOME i => assign' ss (v_struct (LUPDATE (f, v) i f_v_l)) lval
-    | NONE => NONE)
-  | SOME (v_header validity f_v_l) =>
-   (case INDEX_OF f (MAP FST f_v_l) of
-    | SOME i => assign' ss (v_header validity (LUPDATE (f, v) i f_v_l)) lval
-    | NONE => NONE)
-   | _ => NONE) /\    
- (assign' ss v (lval_slice lval ev1 ev2) =
-  case v of
-  | v_bit vb =>
-   (case lookup_lval' ss lval of
-    | SOME (v_bit vb') =>
-     (case assign_to_slice' vb vb' ev1 ev2 of
-      | SOME v_res => assign' ss v_res lval
-      | _ => NONE)
-    | _ => NONE)
-  | _ => NONE) /\
- (assign' ss v lval_null = SOME ss) /\
- (assign' ss v (lval_paren lval) = assign' ss v lval)
-End
 
 Definition stmt_exec_ass'_def:
  (stmt_exec_ass' lval (e_v v) ss = assign' ss v lval) /\
diff --git a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
new file mode 100644
index 0000000..fb3467a
--- /dev/null
+++ b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
@@ -0,0 +1,283 @@
+open HolKernel boolLib Parse bossLib;
+
+val _ = new_theory "p4_exec_sem_v1model_cakeProg";
+
+open p4Syntax;
+open bitstringSyntax numSyntax;
+open p4Theory;
+open p4_auxTheory;
+open p4_exec_semTheory;
+open p4_coreTheory p4_v1modelTheory;
+
+(* CakeML: *)
+open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory mlmapTheory basisFunctionsLib
+     astPP comparisonTheory;
+
+open p4_exec_sem_arch_cakeProgTheory;
+
+intLib.deprecate_int();
+val _ = (max_print_depth := 100);
+
+(* V1Model architecture functions *)
+
+Definition v1model_postparser'_def:
+ v1model_postparser' ((counter, ext_obj_map, v_map, ctrl):v1model_ascope) =
+  (case ALOOKUP v_map "b" of
+   | SOME (v_ext_ref i) =>
+    (case ALOOKUP ext_obj_map i of
+     | SOME (INL (core_v_ext_packet bl)) =>
+      (case ALOOKUP v_map "b_temp" of
+       | SOME (v_ext_ref i') =>
+        (case ALOOKUP v_map "parsedHdr" of
+         | SOME v =>
+          let v_map' = AUPDATE v_map ("hdr", v) in
+           (case ALOOKUP v_map "parseError" of
+            | SOME v' =>
+             (case assign' [v_map_to_scope v_map'] v' (lval_field (lval_varname (varn_name "standard_metadata")) "parser_error") of
+              | SOME [v_map_scope] =>
+               (case scope_to_vmap v_map_scope of
+                | SOME v_map'' =>
+                 let v_map''' = AUPDATE v_map'' ("parseError", v_bit (fixwidth 32 (n2v 0), 32)) in
+                 let (counter', ext_obj_map', v_map'''', ctrl') = (v1model_ascope_update (counter, ext_obj_map, v_map''', ctrl) i' (INL (core_v_ext_packet bl))) in
+   SOME (v1model_ascope_update (counter', ext_obj_map', v_map'''', ctrl') i (INL (core_v_ext_packet [])))
+                | NONE => NONE)
+              | _ => NONE)
+            | NONE => NONE)
+         | _ => NONE)
+       | _ => NONE)
+     | _ => NONE)
+   | _ => NONE)
+End
+
+fun mk_v_bitii' (num, width) =
+ let
+  val width_tm = term_of_int width
+ in
+  mk_v_bit $ mk_pair (mk_fixwidth (width_tm, mk_n2v $ term_of_int num), width_tm)
+ end
+;
+
+val v1model_standard_metadata_zeroed' =
+ listSyntax.mk_list
+  (map pairSyntax.mk_pair
+   [(“"ingress_port"”, mk_v_bitii' (0, 9)),
+    (“"egress_spec"”, mk_v_bitii' (0, 9)),
+    (“"egress_port"”, mk_v_bitii' (0, 9)),
+    (“"instance_type"”, mk_v_bitii' (0, 32)),
+    (“"packet_length"”, mk_v_bitii' (0, 32)),
+    (“"enq_timestamp"”, mk_v_bitii' (0, 32)),
+    (“"enq_qdepth"”, mk_v_bitii' (0, 19)),
+    (“"deq_timedelta"”, mk_v_bitii' (0, 32)),
+    (“"deq_qdepth"”, mk_v_bitii' (0, 19)),
+    (“"ingress_global_timestamp"”, mk_v_bitii' (0, 48)),
+    (“"egress_global_timestamp"”, mk_v_bitii' (0, 48)),
+    (“"mcast_grp"”, mk_v_bitii' (0, 16)),
+    (“"egress_rid"”, mk_v_bitii' (0, 16)),
+    (“"checksum_error"”, mk_v_bitii' (0, 1)),
+    (“"parser_error"”, mk_v_bitii' (0, 32)),
+    (“"priority"”, mk_v_bitii' (0, 3))],
+   “:(string # p4$v)”);
+
+Definition v1model_input_f'_def:
+ (v1model_input_f' (tau1_uninit_v,tau2_uninit_v) (io_list:in_out_list, (counter, ext_obj_map, v_map, ctrl):v1model_ascope) =
+  case io_list of
+  | [] => NONE
+  | ((bl,p)::t) =>
+   (* TODO: Currently, no garbage collection in ext_obj_map is done *)
+   (* let counter' = ^v1model_init_counter in *)
+   let ext_obj_map' = AUPDATE_LIST ext_obj_map [(counter, INL (core_v_ext_packet bl));
+                                                (counter+1, INL (core_v_ext_packet []))] in
+   let counter' = counter + 2 in
+   (* TODO: Currently, no garbage collection in v_map is done *)
+   let v_map' = AUPDATE_LIST v_map [("b", v_ext_ref counter);
+                                    ("b_temp", v_ext_ref (counter+1));
+                                    ("standard_metadata", v_struct (AUPDATE (^v1model_standard_metadata_zeroed') ("ingress_port", (v_bit (fixwidth 9 $ n2v p, 9) ) )));
+                                    ("parsedHdr", tau1_uninit_v);
+                                    ("hdr", tau1_uninit_v);
+                                    ("meta", tau2_uninit_v)] in
+    SOME (t, (counter', ext_obj_map', v_map', ctrl):v1model_ascope))
+End
+
+
+Definition v1model_reduce_nonout'_def:
+ (v1model_reduce_nonout' ([], elist, v_map) =
+  SOME []
+ ) /\
+ (v1model_reduce_nonout' (d::dlist, e::elist, v_map) =
+  if is_d_out d
+  then oCONS (e, v1model_reduce_nonout' (dlist, elist, v_map))
+  else
+   (case e of
+    | (e_var (varn_name x)) =>
+     (case ALOOKUP v_map x of
+      | SOME v =>
+       if is_d_in d
+       then oCONS (e_v v, v1model_reduce_nonout' (dlist, elist, v_map))
+       else oCONS (e_v (init_out_v_cake v), v1model_reduce_nonout' (dlist, elist, v_map))       
+      | _ => NONE)
+    | _ => NONE)) /\
+ (v1model_reduce_nonout' (_, _, v_map) = NONE)
+End
+
+Definition v1model_copyin_pbl'_def:
+ v1model_copyin_pbl' (xlist, dlist, elist, (counter, ext_obj_map, v_map, ctrl):v1model_ascope) =
+  case v1model_reduce_nonout' (dlist, elist, v_map) of
+  | SOME elist' =>
+   (case copyin' xlist dlist elist' [v_map_to_scope v_map] [ [] ] of
+    | SOME scope =>
+     SOME scope
+    | NONE => NONE)
+  | NONE => NONE
+End
+
+Definition copyout_pbl_gen'_def:
+ copyout_pbl_gen' xlist dlist g_scope_list v_map =
+  let v_map_scope = v_map_to_scope v_map in
+   update_return_frame' xlist dlist [v_map_scope] g_scope_list
+End
+
+Definition v1model_copyout_pbl'_def:
+ v1model_copyout_pbl' (g_scope_list, (counter, ext_obj_map, v_map, ctrl):v1model_ascope, dlist, xlist, (status:status)) =
+  case copyout_pbl_gen' xlist dlist g_scope_list v_map of
+  | SOME [v_map_scope] =>
+   (case scope_to_vmap v_map_scope of
+    | SOME v_map' => SOME ((counter, ext_obj_map, v_map', ctrl):v1model_ascope)
+    | NONE => NONE)
+  | _ => NONE
+End
+
+(* TODO: This is the same as the regular version, but with types specialised for V1Model.
+ *       The regular version gives side conditions, for some reason... *)
+Definition v1model_packet_in_extract_gen_def:
+ (v1model_packet_in_extract_gen ascope_lookup (ascope_update:num #
+    (num # (core_v_ext + v1model_v_ext)) list #
+    (string # p4$v) list #
+    (string # (((e list -> bool) # num) # string # e list) list) list ->
+    num ->
+    core_v_ext + v1model_v_ext ->
+    num #
+    (num # (core_v_ext + v1model_v_ext)) list #
+    (string # p4$v) list #
+    (string # (((e list -> bool) # num) # string # e list) list) list) ascope_update_v_map (ascope:v1model_ascope, g_scope_list:g_scope_list, scope_list) =
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
+  | SOME (v_ext_ref i) =>
+   (case lookup_lval_header scope_list (lval_varname (varn_name "headerLvalue")) of
+    | SOME (valid_bit, x_v_l) =>
+     (case lookup_ascope_gen ascope_lookup ascope i of
+      | SOME ((INL (core_v_ext_packet packet_in_bl)):(core_v_ext, v1model_v_ext) sum) =>
+       (case size_in_bits (v_header valid_bit x_v_l) of
+        | SOME size' =>
+         if arithmetic$<= size' (LENGTH packet_in_bl)
+         then
+          (case set_header x_v_l packet_in_bl of
+           | SOME header =>
+            (case assign' scope_list header (lval_varname (varn_name "headerLvalue")) of
+             | SOME scope_list' =>
+              SOME (update_ascope_gen ascope_update ascope i ((INL (core_v_ext_packet (DROP size' packet_in_bl))):(core_v_ext, v1model_v_ext) sum), scope_list', status_returnv v_bot)
+             | NONE => NONE)
+           | NONE => NONE)
+         else
+          (* NOTE: Specific serialisation of errors is assumed here - "PacketTooShort" -> 1 *)
+          SOME (ascope_update_v_map (update_ascope_gen ascope_update ascope i ((INL (core_v_ext_packet [])):(core_v_ext, v1model_v_ext) sum)) "parseError" (v_bit (fixwidth 32 (n2v 1), 32)), scope_list, status_trans "reject")
+        | NONE => NONE)
+       | _ => NONE)
+    | NONE => NONE)
+  | _ => NONE
+ )
+End
+
+Definition v1model_packet_in_extract'_def:
+ v1model_packet_in_extract':((num #
+  (num # (core_v_ext + v1model_v_ext)) list #
+  (string # p4$v) list #
+  (string # (((e list -> bool) # num) # string # e list) list) list) #
+ (varn # p4$v # lval option) list list #
+ (varn # p4$v # lval option) list list ->
+ ((num #
+   (num # (core_v_ext + v1model_v_ext)) list #
+   (string # p4$v) list #
+   (string # (((e list -> bool) # num) # string # e list) list) list) #
+  (varn # p4$v # lval option) list list # status) option) = v1model_packet_in_extract_gen v1model_ascope_lookup v1model_ascope_update v1model_ascope_update_v_map
+End
+
+(* TODO: Note that this does not distinguish failing from finishing *)
+Definition arch_multi_exec'_def:
+ (arch_multi_exec' actx ((aenv, g_scope_list, arch_frame_list, status):'a astate) 0 =
+  SOME (aenv, g_scope_list, arch_frame_list, status))
+  /\
+ (arch_multi_exec' actx (aenv, g_scope_list, arch_frame_list, status) (SUC fuel) =
+  case arch_exec' actx (aenv, g_scope_list, arch_frame_list, status) of
+  | SOME (aenv', g_scope_list', arch_frame_list', status') =>
+   arch_multi_exec' actx (aenv', g_scope_list', arch_frame_list', status') fuel
+  | NONE => SOME (aenv, g_scope_list, arch_frame_list, status))
+End
+
+Definition p4_get_output_list_def:
+ p4_get_output_list (((i, io_list, io_list', ascope), g_scope_list, arch_frame_list, status):'a astate) =
+  io_list'
+End
+
+
+val _ = translation_extends "p4_exec_sem_arch_cakeProg";
+
+val _ = ml_prog_update (open_module "p4_exec_sem_v1model_cake");
+
+val _ = translate arch_multi_exec'_def;
+
+val _ = translate v_map_to_scope_def;
+val _ = translate oCONS_def;
+val _ = translate scope_to_vmap_def;
+val _ = translate v1model_ascope_update_def;
+val _ = translate v1model_postparser'_def;
+
+val _ = translate v1model_input_f'_def;
+
+val _ = translate v1model_is_drop_port_def;
+val _ = translate v1model_lookup_obj_def;
+val _ = translate v1model_output_f_def;
+
+val _ = translate v1model_reduce_nonout'_def;
+val _ = translate v1model_copyin_pbl'_def;
+
+val _ = translate copyout_pbl_gen'_def;
+val _ = translate v1model_copyout_pbl'_def;
+
+val _ = translate FOLDL_MATCH_alt_def;
+val _ = translate FOLDL_MATCH_def;
+val _ = translate listTheory.LIST_TO_SET_DEF;
+val _ = translate boolTheory.IN_DEF;
+val _ = translate v1model_apply_table_f_def;
+
+val _ = translate header_is_valid_def;
+
+val _ = translate header_set_valid_def;
+
+val _ = translate header_set_invalid_def;
+
+val _ = translate v1model_mark_to_drop_def;
+
+val _ = translate v1model_ascope_update_v_map_def;
+val _ = translate verify_gen_def;
+val _ = translate v1model_verify_def;
+
+val _ = translate lookup_lval_header_def;
+val _ = translate lookup_ascope_gen_def;
+val _ = translate size_in_bits_def;
+val _ = translate set_bool_def;
+val _ = translate set_bit_def;
+val _ = translate oTAKE_DROP_def;
+val _ = translate set_fields_def;
+val _ = translate set_header_def;
+val _ = translate update_ascope_gen_def;
+val _ = translate packet_in_extract_gen_def;
+val _ = translate v1model_packet_in_extract_gen_def;
+val _ = translate v1model_ascope_lookup_def;
+val _ = translate v1model_packet_in_extract'_def;
+
+val _ = translate flatten_v_l_def;
+val _ = translate packet_out_emit_gen_def;
+val _ = translate v1model_packet_out_emit_def;
+
+val _ = ml_prog_update (close_module NONE);
+
+val _ = export_theory ();
diff --git a/hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml
new file mode 100644
index 0000000..61160cc
--- /dev/null
+++ b/hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml
@@ -0,0 +1,287 @@
+open HolKernel boolLib Parse bossLib;
+
+val _ = new_theory "p4_exec_sem_wrapper_cakeProg";
+
+open p4Syntax;
+open bitstringSyntax numSyntax;
+open p4Theory;
+open p4_auxTheory;
+open p4_exec_semTheory;
+open p4_coreTheory p4_v1modelTheory;
+
+(* CakeML: *)
+open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory mlmapTheory basisFunctionsLib
+     astPP comparisonTheory;
+
+open p4_exec_sem_v1model_cakeProgTheory;
+
+open fromSexpTheory;
+
+intLib.deprecate_int();
+val _ = (max_print_depth := 100);
+
+val _ = translation_extends "p4_exec_sem_v1model_cakeProg";
+
+(***********************)
+(* Conditional example *)
+
+val symb_exec1_actx = ``([arch_block_inp;
+  arch_block_pbl "p"
+    [e_var (varn_name "b"); e_var (varn_name "parsedHdr");
+     e_var (varn_name "meta"); e_var (varn_name "standard_metadata")];
+  arch_block_ffbl "postparser";
+  arch_block_pbl "vrfy" [e_var (varn_name "hdr"); e_var (varn_name "meta")];
+  arch_block_pbl "ingress"
+    [e_var (varn_name "hdr"); e_var (varn_name "meta");
+     e_var (varn_name "standard_metadata")];
+  arch_block_pbl "egress"
+    [e_var (varn_name "hdr"); e_var (varn_name "meta");
+     e_var (varn_name "standard_metadata")];
+  arch_block_pbl "update" [e_var (varn_name "hdr"); e_var (varn_name "meta")];
+  arch_block_pbl "deparser" [e_var (varn_name "b"); e_var (varn_name "hdr")];
+  arch_block_out],
+ [("p",pbl_type_parser,
+   [("b",d_none); ("h",d_out); ("m",d_inout); ("sm",d_inout)],
+   [("p",stmt_seq stmt_empty (stmt_trans (e_v (v_str "start"))),[])],[],
+   [("start",
+     stmt_seq
+       (stmt_ass lval_null
+          (e_call (funn_ext "packet_in" "extract")
+             [e_var (varn_name "b"); e_acc (e_var (varn_name "h")) "h"]))
+       (stmt_trans (e_v (v_str "accept"))))],[]);
+  ("vrfy",pbl_type_control,[("h",d_inout); ("m",d_inout)],
+   [("vrfy",stmt_seq stmt_empty stmt_empty,[])],[],[],[]);
+  ("update",pbl_type_control,[("h",d_inout); ("m",d_inout)],
+   [("update",stmt_seq stmt_empty stmt_empty,[])],[],[],[]);
+  ("egress",pbl_type_control,[("h",d_inout); ("m",d_inout); ("sm",d_inout)],
+   [("egress",stmt_seq stmt_empty stmt_empty,[])],[],[],[]);
+  ("deparser",pbl_type_control,[("b",d_none); ("h",d_in)],
+   [("deparser",
+     stmt_seq stmt_empty
+       (stmt_ass lval_null
+          (e_call (funn_ext "packet_out" "emit")
+             [e_var (varn_name "b"); e_acc (e_var (varn_name "h")) "h"])),[])],
+   [],[],[]);
+  ("ingress",pbl_type_control,
+   [("h",d_inout); ("m",d_inout); ("standard_meta",d_inout)],
+   [("ingress",
+     stmt_seq stmt_empty
+       (stmt_cond
+          (e_binop
+             (e_acc (e_acc (e_acc (e_var (varn_name "h")) "h") "row") "e")
+             binop_lt (e_v (v_bit ([T; F; F; F; F; F; F; F],8))))
+          (stmt_ass
+             (lval_field (lval_varname (varn_name "standard_meta"))
+                "egress_spec") (e_v (v_bit ([F; F; F; F; F; F; F; F; T],9))))
+          (stmt_ass
+             (lval_field (lval_varname (varn_name "standard_meta"))
+                "egress_spec") (e_v (v_bit ([F; F; F; F; F; F; F; T; F],9))))),
+     [])],[],[],[])],[("postparser",ffblock_ff v1model_postparser')],
+ v1model_input_f'
+   (v_struct
+      [("h",
+        v_header F
+          [("row",
+            v_struct
+              [("e",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("t",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16));
+               ("l",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("r",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("v",v_bit ([F; F; F; F; F; F; F; F],8))])])],
+    v_struct []),v1model_output_f,v1model_copyin_pbl',v1model_copyout_pbl',
+ v1model_apply_table_f,
+ [("header",NONE,
+   [("isValid",[("this",d_in)],header_is_valid);
+    ("setValid",[("this",d_inout)],header_set_valid);
+    ("setInvalid",[("this",d_inout)],header_set_invalid)]);
+  ("",NONE,
+   [("mark_to_drop",[("standard_metadata",d_inout)],v1model_mark_to_drop);
+    ("verify",[("condition",d_in); ("err",d_in)],v1model_verify);
+(*
+    ("verify_checksum",
+     [("condition",d_in); ("data",d_in); ("checksum",d_in); ("algo",d_none)],
+     v1model_verify_checksum);
+
+    ("update_checksum",
+     [("condition",d_in); ("data",d_in); ("checksum",d_inout);
+      ("algo",d_none)],v1model_update_checksum) *) ]);
+  ("packet_in",NONE,
+   [("extract",[("this",d_in); ("headerLvalue",d_out)],
+     v1model_packet_in_extract')]);
+  ("packet_out",NONE,
+   [("emit",[("this",d_in); ("data",d_in)],v1model_packet_out_emit)]) (* ;
+  ("register",
+   SOME
+     ([("this",d_out); ("size",d_none); ("targ1",d_in)],register_construct),
+   [("read",[("this",d_in); ("result",d_out); ("index",d_in)],register_read);
+    ("write",[("this",d_in); ("index",d_in); ("value",d_in)],register_write)])
+*)
+],
+ [("NoAction",
+   stmt_seq
+     (stmt_cond (e_var (varn_name "from_table"))
+        (stmt_ass (lval_varname (varn_name "gen_apply_result"))
+           (e_struct
+              [("hit",e_var (varn_name "hit"));
+               ("miss",e_unop unop_neg (e_var (varn_name "hit")));
+               ("action_run",
+                e_v
+                  (v_bit
+                     ([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
+                       F; F; F; F; F; F; F; F; F; F; F; F; F; F],32)))]))
+        stmt_empty) (stmt_seq stmt_empty (stmt_ret (e_v v_bot))),
+   [("from_table",d_in); ("hit",d_in)])]):v1model_ascope actx``;
+
+(* TODO: Apart from the table and extern configurations, this seems close to a generic P4 initial state *)
+val symb_exec1_astate = “((0,[],[],0,[],[("parseError",v_bit (fixwidth 32 (n2v 0),32))],[]),
+    [[(varn_name "gen_apply_result",
+       v_struct
+         [("hit",v_bool F); ("miss",v_bool F);
+          ("action_run",v_bit (REPLICATE 32 F,32))],NONE)]],
+    arch_frame_list_empty,status_running):v1model_ascope astate”;
+
+(* 44 seems to work also with arch_multi_exec, 45 doesn't work *)
+val n_max = “45:num”;
+
+
+(*************************)
+(* Generic wrapper parts *)
+
+Definition symb_exec1_exec_def:
+ symb_exec1_exec input =
+  case
+   arch_multi_exec' ^symb_exec1_actx
+    (p4_append_input_list [input] ^symb_exec1_astate) ^n_max of
+  | SOME res => SOME $ p4_get_output_list res
+  | NONE => NONE
+End
+
+val _ = translate p4_append_input_list_def;
+val _ = translate p4_get_output_list_def;
+val _ = translate symb_exec1_exec_def;
+
+(*
+
+exception ParseError of string;
+
+fun parse_bool_list l =
+   case l of
+     [] => []
+   | h::t =>
+    if h = #"0"
+    then (F::(parse_bool_list t))
+    else if h = #"1"
+    then (T::(parse_bool_list t))
+    else raise ParseError ("Error: packet (first command-line argument) should be specified using only 0s and 1s to signify bits.\n");
+
+fun deparse_bool_list l =
+   case l of
+     [] => []
+   | h::t =>
+    if Teq h
+    then (#"1"::(deparse_bool_list t))
+    else (#"0"::(deparse_bool_list t))
+ ;
+
+val input = listSyntax.mk_list (parse_bool_list $ String.explode "010010101001001011111111100100101", bool)
+
+
+val input = “([F; F; F; T; F; F; F; T; F; F; F; T; F; F; F; T; F; F; F; T; F; F; F; T; F;
+               F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; T; F; T; T; F; F; F; F],0:num)”;
+val bl_input_tm = fst $ dest_pair input
+
+
+
+
+EVAL “symb_exec1_exec ^input”
+
+val bl_input = String.implode $ deparse_bool_list $ fst $ listSyntax.dest_list bl_input_tm
+
+Definition symb_exec1_exec_old_def:
+ symb_exec1_exec_old input =
+  case
+   arch_multi_exec ^symb_exec1_actx
+    (p4_append_input_list [input] ^symb_exec1_astate) ^n_max of
+  | SOME res => SOME $ p4_get_output_list res
+  | NONE => NONE
+End
+
+EVAL “symb_exec1_exec_old ^input”
+
+*)
+
+
+(* TODO: Change this to Quote cakeml: syntax? *)
+val _ = append_prog o process_topdecs $ 
+ ‘exception ParseError string;’
+;
+
+val _ = append_prog o process_topdecs $ 
+ ‘fun parse_bool_list l =
+   case l of
+     [] => []
+   | h::t =>
+    if h = #"0"
+    then (False::(parse_bool_list t))
+    else if h = #"1"
+    then (True::(parse_bool_list t))
+    else raise ParseError ("Error: packet (first command-line argument) should be specified using only 0s and 1s to signify bits.\n")
+ ;
+’;
+
+val _ = append_prog o process_topdecs $ 
+ ‘fun deparse_bool_list l =
+   case l of
+     [] => []
+   | h::t =>
+    if h
+    then (#"T"::(deparse_bool_list t))
+    else (#"F"::(deparse_bool_list t))
+ ;’;
+
+val _ = append_prog o process_topdecs $ 
+ ‘fun print_output_packets l =
+   case l of
+     [] => ()
+   | (out_bl, out_port)::t =>
+    let
+     val out_packet_string = String.implode (deparse_bool_list out_bl)
+    in
+     print(out_packet_string ^ " at port "); print_int out_port; print "\n"; print_output_packets t
+    end
+ ;’;
+
+val _ = append_prog o process_topdecs $ 
+ ‘fun main () =
+   let
+     val packet_arg::rest = (CommandLine.arguments())
+     val port_arg = List.hd rest
+
+     val bl = parse_bool_list (String.explode packet_arg)
+     val in_port = Option.valOf (Int.fromString port_arg)
+     val in_packet_string = String.implode (deparse_bool_list bl)
+   in
+    (case symb_exec1_exec (bl, in_port) of
+       None => raise ParseError ("Error: execution result is None.\n")
+     | Some output_packets =>
+       (print ("Input packet was: " ^ in_packet_string ^ " at port "); print_int in_port; print "\n";
+       print "Output packet(s) are: "; print_output_packets output_packets))
+   end
+   handle ParseError parse_err_msg => TextIO.print_err parse_err_msg
+   handle _ =>
+     TextIO.print_err ("Usage: " ^ CommandLine.name() ^ " <n>\n");’;
+
+(* TODO: Can this be replaced with something more short-handish? *)
+val prog =
+ “SNOC
+   (Dlet unknown_loc (Pcon NONE [])
+    (App Opapp [Var (Short "main"); Con NONE []]))
+    ^(get_ml_prog_state() |> get_prog)”
+  |> EVAL |> concl |> rhs;
+
+val _ = astToSexprLib.write_ast_to_file "test3.sexp" prog;
+    
+val _ = export_theory ();
diff --git a/hol/p4_auxScript.sml b/hol/p4_auxScript.sml
index 23136c6..aca456c 100644
--- a/hol/p4_auxScript.sml
+++ b/hol/p4_auxScript.sml
@@ -2649,4 +2649,107 @@ Proof
 metis_tac[]
 QED
 
+(***************************************)
+(* For exportable executable semantics *)
+
+
+Definition slice'_def:
+ slice' (v, n) (vec1, len1) (vec2, len2) =
+  let hi = v2n vec1 in
+  let lo = v2n vec2 in
+  if lo <= hi /\ hi < n /\ LENGTH v = n
+  then
+   SOME $ bitv_bitslice (v, n) (v2n vec1) (v2n vec2)
+  else NONE
+End
+
+Definition slice_lval'_def:
+ slice_lval' v e1 e2 =
+  case v of
+  | (v_bit (v, bl)) =>
+   (case e1 of
+    | (e_v (v_bit (v1, bl1))) =>
+     (case e2 of
+      | (e_v (v_bit (v2, bl2))) =>
+       (case slice' (v, bl) (v1, bl1) (v2, bl2) of
+        | SOME bitv => SOME $ v_bit bitv
+        | NONE => NONE)
+      | _ => NONE)
+    | _ => NONE)
+  | _ => NONE
+End
+
+Definition lookup_lval'_def:
+ (lookup_lval' (ss:scope list) (lval_varname x) = lookup_v ss x) /\
+ (lookup_lval' ss (lval_field lval f) =
+  case lookup_lval' ss lval of
+  | SOME v => acc_f v f
+  | NONE => NONE) /\
+ (lookup_lval' ss (lval_slice lval e1 e2) =
+  case lookup_lval' ss lval of
+   | SOME (v_bit (v, bl)) => slice_lval' (v_bit (v, bl)) e1 e2
+   | _ => NONE) /\
+ (lookup_lval' ss lval_null = NONE ) /\
+ (lookup_lval' ss (lval_paren lval) = lookup_lval' ss lval) 
+End
+
+
+(* Puts the bits in bl1 between index hi and lo of bl2. *)
+Definition replace_bits_def:
+ replace_bits (bl1, (n1:num)) (bl2,n2) hi lo =
+  if lo <= hi /\ hi < n2 /\ LENGTH bl2 = n2
+  then
+   SOME $ (SEG (n2-(hi+1)) 0 bl2) ++ bl1 ++ (SEG lo (n2-lo) bl2)
+  else NONE
+End
+
+Definition assign_to_slice'_def:
+ assign_to_slice' vb vb' ev1 ev2 =
+  (case ev1 of
+   | (e_v (v_bit (bl1, n1))) =>
+    (case ev2 of
+     | (e_v (v_bit (bl2, n2))) =>
+      (case replace_bits vb vb' (v2n bl1) (v2n bl2) of
+       | SOME bitv =>
+        SOME $ v_bit (bitv, SND vb')
+       | NONE => NONE)
+     | _ => NONE)
+   | _ => NONE)
+End
+
+Definition assign'_def:
+ (assign' ss v (lval_varname x) =
+  case find_topmost_map ss x of
+  | SOME (i, sc) =>
+   (case lookup_out ss x of
+    | SOME str_opt =>
+      SOME (LUPDATE (AUPDATE sc (x, (v, str_opt))) i ss)
+    | NONE => NONE)
+  | _ => NONE) /\
+ (assign' ss v (lval_field lval f) =
+  case lookup_lval' ss lval of
+  | SOME (v_struct f_v_l) =>
+   (case INDEX_OF f (MAP FST f_v_l) of
+    | SOME i => assign' ss (v_struct (LUPDATE (f, v) i f_v_l)) lval
+    | NONE => NONE)
+  | SOME (v_header validity f_v_l) =>
+   (case INDEX_OF f (MAP FST f_v_l) of
+    | SOME i => assign' ss (v_header validity (LUPDATE (f, v) i f_v_l)) lval
+    | NONE => NONE)
+   | _ => NONE) /\    
+ (assign' ss v (lval_slice lval ev1 ev2) =
+  case v of
+  | v_bit vb =>
+   (case lookup_lval' ss lval of
+    | SOME (v_bit vb') =>
+     (case assign_to_slice' vb vb' ev1 ev2 of
+      | SOME v_res => assign' ss v_res lval
+      | _ => NONE)
+    | _ => NONE)
+  | _ => NONE) /\
+ (assign' ss v lval_null = SOME ss) /\
+ (assign' ss v (lval_paren lval) = assign' ss v lval)
+End
+
+
 val _ = export_theory ();
diff --git a/hol/p4_coreScript.sml b/hol/p4_coreScript.sml
index 0accd15..6702c5e 100644
--- a/hol/p4_coreScript.sml
+++ b/hol/p4_coreScript.sml
@@ -26,11 +26,11 @@ End
 
 Definition verify_gen_def:
  (verify_gen ascope_update_v_map (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "condition")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "condition")) of
   | SOME (v_bool T) =>
    SOME (ascope, scope_list, status_returnv v_bot)
   | SOME (v_bool F) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "err")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "err")) of
     | SOME (v_bit bitv) =>
      SOME (ascope_update_v_map ascope "parseError" (v_bit bitv), scope_list, status_trans "reject")
     | _ => NONE)
@@ -101,7 +101,7 @@ End
 
 Definition header_is_valid_def:
  (header_is_valid (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_header valid_bit x_v_l) =>
    SOME (ascope, scope_list, status_returnv (v_bool valid_bit))
   | _ => NONE
@@ -110,9 +110,9 @@ End
 
 Definition header_set_valid_def:
  (header_set_valid (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_header valid_bit x_v_l) =>
-   (case assign scope_list (v_header T x_v_l) (lval_varname (varn_name "this")) of
+   (case assign' scope_list (v_header T x_v_l) (lval_varname (varn_name "this")) of
     | SOME scope_list' =>
      SOME (ascope, scope_list', status_returnv v_bot)
     | NONE => NONE)
@@ -122,9 +122,9 @@ End
 
 Definition header_set_invalid_def:
  (header_set_invalid (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_header valid_bit x_v_l) =>
-   (case assign scope_list (v_header F x_v_l) (lval_varname (varn_name "this")) of
+   (case assign' scope_list (v_header F x_v_l) (lval_varname (varn_name "this")) of
     | SOME scope_list' =>             
      SOME (ascope, scope_list', status_returnv v_bot)
     | NONE => NONE)
@@ -154,32 +154,54 @@ End
 
 Definition lookup_lval_header_def:
  (lookup_lval_header ss header_lval =
-  case lookup_lval ss header_lval of
+  case lookup_lval' ss header_lval of
    | SOME (v_header valid_bit x_v_l) => SOME (valid_bit, x_v_l)
    | _ => NONE
  )
 End
 
-(* Partial, but does the job where it is used *)
 Definition set_bool_def:
- (set_bool packet_in = v_bool (HD packet_in))
+ (set_bool [] = NONE) /\
+ (set_bool packet_in = SOME (v_bool (HD packet_in), TL packet_in))
 End
 Definition set_bit_def:
- (set_bit n packet_in = v_bit (TAKE n packet_in, n))
+ (set_bit n packet_in =
+  case oTAKE n packet_in of
+  | SOME res => SOME (v_bit (res, n), DROP n packet_in)
+  | NONE => NONE)
+End
+
+Definition oTAKE_DROP_def:
+ (oTAKE_DROP 0 l = SOME ([], l)) /\
+ (oTAKE_DROP (SUC n) [] = NONE) /\
+ (oTAKE_DROP (SUC n) (h::t) =
+  case oTAKE_DROP n t of
+  | SOME (l1, l2) =>
+   SOME (h::l1, l2)
+  | NONE => NONE)
 End
 
 Definition set_fields_def:
  (set_fields []     acc _ = SOME acc) /\
  (set_fields (h::t) acc packet_in =
   case h of
-  | (x:x, (v_bool b)) => set_fields t (acc++[(x, set_bool packet_in)]) (DROP 1 packet_in)
-  | (x, (v_bit (bv, l))) => set_fields t (acc++[(x, set_bit l packet_in)]) (DROP l packet_in)
+  | (x:x, (v_bool b)) =>
+   (case set_bool packet_in of
+    | SOME (res, t') => set_fields t (acc++[(x, res)]) t'
+    | NONE => NONE)
+  | (x, (v_bit (bv, l))) =>
+   (case set_bit l packet_in of
+    | SOME (res, t') => set_fields t (acc++[(x, res)]) t'
+    | NONE => NONE)
   | (x, (v_struct x_v_l)) =>
    (case size_in_bits (v_struct x_v_l) of
     | SOME n =>
-     (case set_fields x_v_l [] (TAKE n packet_in) of
-      | SOME acc' =>
-       set_fields t (acc++[(x, v_struct acc')]) (DROP n packet_in)
+     (case oTAKE_DROP n packet_in of
+      | SOME (res, t') =>
+       (case set_fields x_v_l [] res of
+        | SOME acc' =>
+         set_fields t (acc++[(x, v_struct acc')]) t'
+        | NONE => NONE)
       | NONE => NONE)
     | NONE => NONE)
   | _ => NONE)
@@ -202,8 +224,14 @@ Definition set_struct_def:
 End
 
 Definition set_v_def:
- (set_v (v_bit (bitv, n)) packet_in = SOME (set_bit n packet_in)) /\
- (set_v (v_bool b)        packet_in = SOME (set_bool packet_in)) /\
+ (set_v (v_bit (bitv, n)) packet_in =
+  case set_bit n packet_in of
+  | SOME (res, t') => SOME res
+  | NONE => NONE) /\
+ (set_v (v_bool b)        packet_in =
+  case set_bool packet_in of
+  | SOME (res, t') => SOME res
+  | NONE => NONE) /\
  (set_v (v_struct x_v_l)  packet_in = (set_struct x_v_l packet_in)) /\
  (set_v (v_header validity x_v_l) packet_in = (set_header x_v_l packet_in))
 End
@@ -212,7 +240,7 @@ End
 (* TODO: Extend to cover extraction to header stacks *)
 Definition packet_in_extract_gen_def:
  (packet_in_extract_gen ascope_lookup ascope_update ascope_update_v_map (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_ext_ref i) =>
    (case lookup_lval_header scope_list (lval_varname (varn_name "headerLvalue")) of
     | SOME (valid_bit, x_v_l) =>
@@ -224,7 +252,7 @@ Definition packet_in_extract_gen_def:
          then
           (case set_header x_v_l packet_in_bl of
            | SOME header =>
-            (case assign scope_list header (lval_varname (varn_name "headerLvalue")) of
+            (case assign' scope_list header (lval_varname (varn_name "headerLvalue")) of
              | SOME scope_list' =>
               SOME (update_ascope_gen ascope_update ascope i ((INL (core_v_ext_packet (DROP size packet_in_bl))):(core_v_ext, 'b) sum), scope_list', status_returnv v_bot)
              | NONE => NONE)
@@ -242,9 +270,9 @@ End
 (* See https://p4.org/p4-spec/docs/P4-16-v1.2.4.html#sec-packet-lookahead *)
 Definition packet_in_lookahead_gen_def:
  (packet_in_lookahead_gen ascope_lookup ascope_update_v_map (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_ext_ref i) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "targ1")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "targ1")) of
     | SOME dummy_v =>
      (case lookup_ascope_gen ascope_lookup ascope i of
       | SOME ((INL (core_v_ext_packet packet_in_bl)):(core_v_ext, 'b) sum) =>
@@ -272,7 +300,7 @@ End
 
 Definition lookup_lval_bit32_def:
  (lookup_lval_bit32 ss bit32_lval =
-  case lookup_lval ss bit32_lval of
+  case lookup_lval' ss bit32_lval of
    | SOME (v_bit (bitv, 32)) => SOME (v2n bitv)
    | _ => NONE
  )
@@ -280,7 +308,7 @@ End
 
 Definition packet_in_advance_gen_def:
  (packet_in_advance_gen ascope_lookup ascope_update ascope_update_v_map (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_ext_ref i) =>
    (case lookup_lval_bit32 scope_list (lval_varname (varn_name "bits")) of
     | SOME n_bits =>
@@ -345,11 +373,11 @@ End
 (* Note: Nested headers are not allowed, so this is only checked at top level *)
 Definition packet_out_emit_gen_def:
  (packet_out_emit_gen (ascope_lookup:'a -> num -> (core_v_ext + 'b) option) ascope_update (ascope:'a, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "this")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "this")) of
   | SOME (v_ext_ref i) =>
    (case lookup_ascope_gen ascope_lookup ascope i of
     | SOME (INL (core_v_ext_packet packet_out_bl)) =>
-     (case lookup_lval scope_list (lval_varname (varn_name "data")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "data")) of
       | SOME (v_header F x_v_l) => SOME (ascope, scope_list, status_returnv v_bot)
       | SOME (v_header T x_v_l) =>
        (case flatten_v_l (MAP SND x_v_l) of
@@ -410,7 +438,7 @@ End
 
 Definition get_checksum_incr_def:
  (get_checksum_incr scope_list ext_data_name =
-   (case lookup_lval scope_list ext_data_name of
+   (case lookup_lval' scope_list ext_data_name of
     | SOME (v_bit (bl, n)) =>
      if n MOD 16 = 0 then SOME (v2w16s' bl) else NONE
     | SOME (v_header vbit f_list) =>
@@ -428,7 +456,7 @@ End
 (* Alternative version tailored for symbolic execution *)
 Definition get_checksum_incr'_def:
  (get_checksum_incr' scope_list ext_data_name =
-   (case lookup_lval scope_list ext_data_name of
+   (case lookup_lval' scope_list ext_data_name of
     | SOME (v_bit (bl, n)) =>
      if n MOD 16 = 0 then SOME bl else NONE
     | SOME (v_header vbit f_list) =>
@@ -472,7 +500,7 @@ End
 
 Definition get_bitlist_def:
  get_bitlist scope_list ext_data_name =
-  case lookup_lval scope_list ext_data_name of
+  case lookup_lval' scope_list ext_data_name of
    | SOME (v_bit (bl, n)) => SOME bl
    | SOME (v_header vbit f_list) =>
     (case header_entries2v f_list of
diff --git a/hol/p4_ebpfScript.sml b/hol/p4_ebpfScript.sml
index df9fdde..d6b34c0 100644
--- a/hol/p4_ebpfScript.sml
+++ b/hol/p4_ebpfScript.sml
@@ -191,6 +191,7 @@ Definition ebpf_reduce_nonout_def:
  (ebpf_reduce_nonout (_, _, v_map) = NONE)
 End
 
+(*
 (* TODO: Remove these and keep "v_map" as just a regular scope? *)
 Definition v_map_to_scope_def:
  (v_map_to_scope [] = []) /\
@@ -198,6 +199,7 @@ Definition v_map_to_scope_def:
   ((varn_name k, (v, NONE:lval option))::v_map_to_scope t)
  )
 End
+*)
 
 Definition scope_to_vmap_def:
  (scope_to_vmap [] = SOME []) /\
diff --git a/hol/p4_v1modelScript.sml b/hol/p4_v1modelScript.sml
index 5914897..93813ca 100644
--- a/hol/p4_v1modelScript.sml
+++ b/hol/p4_v1modelScript.sml
@@ -115,9 +115,9 @@ End
 (* NOTE: 511 is the default drop port *)
 Definition v1model_mark_to_drop_def:
  v1model_mark_to_drop (v1model_ascope:v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case assign scope_list (v_bit (fixwidth 9 (n2v 511), 9)) (lval_field (lval_varname (varn_name "standard_metadata")) "egress_spec") of
+  case assign' scope_list (v_bit (fixwidth 9 (n2v 511), 9)) (lval_field (lval_varname (varn_name "standard_metadata")) "egress_spec") of
    | SOME scope_list' =>
-    (case assign scope_list' (v_bit (fixwidth 16 (n2v 0), 16)) (lval_field (lval_varname (varn_name "standard_metadata")) "mcast_grp") of
+    (case assign' scope_list' (v_bit (fixwidth 16 (n2v 0), 16)) (lval_field (lval_varname (varn_name "standard_metadata")) "mcast_grp") of
      | SOME scope_list'' =>
       SOME (v1model_ascope, scope_list'', status_returnv v_bot)
      | NONE => NONE)
@@ -199,24 +199,24 @@ End
 
 Definition v1model_verify_checksum_def:
  (v1model_verify_checksum ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  (case lookup_lval scope_list (lval_varname (varn_name "condition")) of
+  (case lookup_lval' scope_list (lval_varname (varn_name "condition")) of
    | SOME $ v_bool b =>
     if b
     then
-     (case lookup_lval scope_list (lval_varname (varn_name "algo")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "algo")) of
       | SOME $ v_bit (bl, n) =>
        if v2n bl = 6
        then
         (case get_checksum_incr scope_list (lval_varname (varn_name "data")) of
          | SOME checksum_incr =>
-          (case lookup_lval scope_list (lval_varname (varn_name "checksum")) of
+          (case lookup_lval' scope_list (lval_varname (varn_name "checksum")) of
            | SOME $ v_bit (bl', n') =>
             if n' = 16
             then
              (if (v_bit (bl', n')) = (v_bit $ w16 $ compute_checksum16 checksum_incr)
               then SOME ((counter, ext_obj_map, v_map, ctrl), scope_list, status_returnv v_bot)
               else
-               (case assign [v_map_to_scope v_map] (v_bit ([T], 1)) (lval_field (lval_varname (varn_name "standard_metadata")) "checksum_error") of
+               (case assign' [v_map_to_scope v_map] (v_bit ([T], 1)) (lval_field (lval_varname (varn_name "standard_metadata")) "checksum_error") of
                 | SOME [v_map_scope] =>
                  (case scope_to_vmap v_map_scope of
                   | SOME v_map' =>
@@ -244,22 +244,22 @@ End
 
 Definition v1model_update_checksum_def:
  (v1model_update_checksum ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  (case lookup_lval scope_list (lval_varname (varn_name "condition")) of
+  (case lookup_lval' scope_list (lval_varname (varn_name "condition")) of
    | SOME $ v_bool b =>
     if b
     then
-     (case lookup_lval scope_list (lval_varname (varn_name "algo")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "algo")) of
       | SOME $ v_bit (bl, n) =>
        if v2n bl = 6
        then
         (case get_checksum_incr' scope_list (lval_varname (varn_name "data")) of
          | SOME checksum_incr =>
-          (case lookup_lval scope_list (lval_varname (varn_name "checksum")) of
+          (case lookup_lval' scope_list (lval_varname (varn_name "checksum")) of
            | SOME $ v_bit (bl', n') =>
             if n' = 16
             then
              (* TODO: This can be made total, since we just looked up the checksum *)
-             (case assign scope_list (v1model_update_checksum_inner checksum_incr) (lval_varname (varn_name "checksum")) of
+             (case assign' scope_list (v1model_update_checksum_inner checksum_incr) (lval_varname (varn_name "checksum")) of
               | SOME scope_list' =>
                SOME ((counter, ext_obj_map, v_map, ctrl), scope_list', status_returnv v_bot)             | NONE => NONE)
             else NONE
@@ -290,12 +290,12 @@ End
 
 Definition register_construct_def:
  (register_construct ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "size")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "size")) of
   | SOME (v_bit (bl, n)) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "targ1")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "targ1")) of
     | SOME (v_bit (bl', n')) =>
      let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (v1model_v_ext_register (v1model_register_construct_inner bl n'))) in
-     (case assign scope_list (v_ext_ref counter) (lval_varname (varn_name "this")) of
+     (case assign' scope_list (v_ext_ref counter) (lval_varname (varn_name "this")) of
       | SOME scope_list' =>
        SOME ((counter + 1, ext_obj_map', v_map, ctrl), scope_list', status_returnv v_bot)
       | NONE => NONE)
@@ -307,15 +307,15 @@ End
 (* OLD:
 Definition register_read_def:
  (register_read ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "index")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "index")) of
   | SOME (v_bit (bl, n)) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "this")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "this")) of
     | SOME (v_ext_ref i) =>
      (case ALOOKUP ext_obj_map i of
       | SOME (INR (v1model_v_ext_register array)) =>
        (case oEL (v2n bl) array of
         | SOME (bl', n') =>
-         (case assign scope_list (v_bit (bl', n')) (lval_varname (varn_name "result")) of
+         (case assign' scope_list (v_bit (bl', n')) (lval_varname (varn_name "result")) of
           | SOME scope_list' =>
            SOME ((counter, ext_obj_map, v_map, ctrl), scope_list', status_returnv v_bot)
           | NONE => NONE)
@@ -339,17 +339,17 @@ End
 (* Note that register_read always has a result, according to v1model.p4. *)
 Definition register_read_def:
  (register_read ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "index")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "index")) of
   | SOME (v_bit (bl, n)) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "this")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "this")) of
     | SOME (v_ext_ref i) =>
      (case ALOOKUP ext_obj_map i of
       | SOME (INR (v1model_v_ext_register array)) =>
        (* TODO: HACK, looking up the result variable to get the result width. *)
-       (case lookup_lval scope_list (lval_varname (varn_name "result")) of
+       (case lookup_lval' scope_list (lval_varname (varn_name "result")) of
         | SOME (v_bit (bl'', n'')) =>      
          let (bl', n') = v1model_register_read_inner n'' bl array in
-           (case assign scope_list (v_bit (bl', n')) (lval_varname (varn_name "result")) of
+           (case assign' scope_list (v_bit (bl', n')) (lval_varname (varn_name "result")) of
             | SOME scope_list' =>
              SOME ((counter, ext_obj_map, v_map, ctrl), scope_list', status_returnv v_bot)
             | NONE => NONE)
@@ -368,11 +368,11 @@ End
         
 Definition register_write_def:
  (register_write ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "index")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "index")) of
   | SOME (v_bit (bl, n)) =>
-   (case lookup_lval scope_list (lval_varname (varn_name "value")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "value")) of
     | SOME (v_bit (bl', n')) =>
-     (case lookup_lval scope_list (lval_varname (varn_name "this")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "this")) of
       | SOME (v_ext_ref i) =>
        (case ALOOKUP ext_obj_map i of
         | SOME (INR (v1model_v_ext_register array)) =>
@@ -394,7 +394,7 @@ End
 Definition ipsec_crypt_construct_def:
  (ipsec_crypt_construct ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
    let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (v1model_v_ext_ipsec_crypt)) in
-   (case assign scope_list (v_ext_ref counter) (lval_varname (varn_name "this")) of
+   (case assign' scope_list (v_ext_ref counter) (lval_varname (varn_name "this")) of
     | SOME scope_list' =>
      SOME ((counter + 1, ext_obj_map', v_map, ctrl), scope_list', status_returnv v_bot)
     | NONE => NONE)
@@ -420,17 +420,17 @@ End
 
 Definition ipsec_crypt_decrypt_aes_ctr_def:
  (ipsec_crypt_decrypt_aes_ctr ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "ipv4")) of
   | SOME ipv4_header =>
-   (case lookup_lval scope_list (lval_varname (varn_name "esp")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "esp")) of
     | SOME esp_header =>
-     (case lookup_lval scope_list (lval_varname (varn_name "standard_metadata")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "standard_metadata")) of
       | SOME standard_metadata =>
-       (case assign scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
+       (case assign' scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
         | SOME scope_list' =>
-         (case assign scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
+         (case assign' scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
           | SOME scope_list'' =>
-           (case assign scope_list'' (set_validity T $ init_out_v standard_metadata) (lval_varname (varn_name "standard_metadata")) of
+           (case assign' scope_list'' (set_validity T $ init_out_v standard_metadata) (lval_varname (varn_name "standard_metadata")) of
             | SOME scope_list''' =>
              SOME ((counter, ext_obj_map, v_map, ctrl), scope_list''', status_returnv v_bot)
             | _ => NONE)
@@ -444,13 +444,13 @@ End
 
 Definition ipsec_crypt_encrypt_aes_ctr_def:
  (ipsec_crypt_encrypt_aes_ctr ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "ipv4")) of
   | SOME ipv4_header =>
-   (case lookup_lval scope_list (lval_varname (varn_name "esp")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "esp")) of
     | SOME esp_header =>
-     (case assign scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
+     (case assign' scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
       | SOME scope_list' =>
-       (case assign scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
+       (case assign' scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
         | SOME scope_list'' =>
          SOME ((counter, ext_obj_map, v_map, ctrl), scope_list'', status_returnv v_bot)
         | _ => NONE)
@@ -462,13 +462,13 @@ End
 
 Definition ipsec_crypt_encrypt_null_def:
  (ipsec_crypt_encrypt_null ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "ipv4")) of
   | SOME ipv4_header =>
-   (case lookup_lval scope_list (lval_varname (varn_name "esp")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "esp")) of
     | SOME esp_header =>
-     (case assign scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
+     (case assign' scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
       | SOME scope_list' =>
-       (case assign scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
+       (case assign' scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
         | SOME scope_list'' =>
          SOME ((counter, ext_obj_map, v_map, ctrl), scope_list'', status_returnv v_bot)
         | _ => NONE)
@@ -480,17 +480,17 @@ End
 
 Definition ipsec_crypt_decrypt_null_def:
  (ipsec_crypt_decrypt_null ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) =
-  case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of
+  case lookup_lval' scope_list (lval_varname (varn_name "ipv4")) of
   | SOME ipv4_header =>
-   (case lookup_lval scope_list (lval_varname (varn_name "esp")) of
+   (case lookup_lval' scope_list (lval_varname (varn_name "esp")) of
     | SOME esp_header =>
-     (case lookup_lval scope_list (lval_varname (varn_name "standard_metadata")) of
+     (case lookup_lval' scope_list (lval_varname (varn_name "standard_metadata")) of
       | SOME standard_metadata =>
-       (case assign scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
+       (case assign' scope_list (set_validity T $ init_out_v ipv4_header) (lval_varname (varn_name "ipv4")) of
         | SOME scope_list' =>
-         (case assign scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
+         (case assign' scope_list' (set_validity T $ init_out_v esp_header) (lval_varname (varn_name "esp")) of
           | SOME scope_list'' =>
-           (case assign scope_list'' (set_validity T $ init_out_v standard_metadata) (lval_varname (varn_name "standard_metadata")) of
+           (case assign' scope_list'' (set_validity T $ init_out_v standard_metadata) (lval_varname (varn_name "standard_metadata")) of
             | SOME scope_list''' =>
              SOME ((counter, ext_obj_map, v_map, ctrl), scope_list''', status_returnv v_bot)
             | _ => NONE)
@@ -607,6 +607,7 @@ Definition v1model_reduce_nonout_def:
  (v1model_reduce_nonout (_, _, v_map) = NONE)
 End
 
+(*
 (* TODO: Generalise and move to core? Duplicated in all three architectures... *)
 (* TODO: Remove these and keep "v_map" as just a regular scope? *)
 Definition v_map_to_scope_def:
@@ -615,6 +616,7 @@ Definition v_map_to_scope_def:
   ((varn_name k, (v, NONE:lval option))::v_map_to_scope t)
  )
 End
+*)
 
 (* TODO: Generalise and move to core? Duplicated in all three architectures... *)
 Definition scope_to_vmap_def:
@@ -677,7 +679,7 @@ Definition v1model_postparser_def:
           let v_map' = AUPDATE v_map ("hdr", v) in
            (case ALOOKUP v_map "parseError" of
             | SOME v' =>
-             (case assign [v_map_to_scope v_map'] v' (lval_field (lval_varname (varn_name "standard_metadata")) "parser_error") of
+             (case assign' [v_map_to_scope v_map'] v' (lval_field (lval_varname (varn_name "standard_metadata")) "parser_error") of
               | SOME [v_map_scope] =>
                (case scope_to_vmap v_map_scope of
                 | SOME v_map'' =>