diff --git a/hol/cake_export/Holmakefile b/hol/cake_export/Holmakefile
index 7390789..702a507 100644
--- a/hol/cake_export/Holmakefile
+++ b/hol/cake_export/Holmakefile
@@ -1,7 +1,7 @@
 # includes
 # ----------------------------------
 
-CAKEMLDIR = #Your CakeML installation here
+CAKEMLDIR = ../../../../../installed-git-repos/cakeml
 
 DEPENDENCIES   = .. \
  $(CAKEMLDIR)/misc \
diff --git a/hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml b/hol/cake_export/p4_conditional_cakeProgScript.sml
similarity index 98%
rename from hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml
rename to hol/cake_export/p4_conditional_cakeProgScript.sml
index 61160cc..baf1c20 100644
--- a/hol/cake_export/p4_exec_sem_wrapper_cakeProgScript.sml
+++ b/hol/cake_export/p4_conditional_cakeProgScript.sml
@@ -1,6 +1,6 @@
 open HolKernel boolLib Parse bossLib;
 
-val _ = new_theory "p4_exec_sem_wrapper_cakeProg";
+val _ = new_theory "p4_conditional_cakeProg";
 
 open p4Syntax;
 open bitstringSyntax numSyntax;
@@ -18,7 +18,7 @@ open p4_exec_sem_v1model_cakeProgTheory;
 open fromSexpTheory;
 
 intLib.deprecate_int();
-val _ = (max_print_depth := 100);
+val _ = (max_print_depth := 1000);
 
 val _ = translation_extends "p4_exec_sem_v1model_cakeProg";
 
@@ -282,6 +282,6 @@ val prog =
     ^(get_ml_prog_state() |> get_prog)”
   |> EVAL |> concl |> rhs;
 
-val _ = astToSexprLib.write_ast_to_file "test3.sexp" prog;
+val _ = astToSexprLib.write_ast_to_file "conditional_test.sexp" prog;
     
 val _ = export_theory ();
diff --git a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
index fb3467a..2fb05dc 100644
--- a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
+++ b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
@@ -200,6 +200,7 @@ Definition v1model_packet_in_extract'_def:
   (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: Move to p4_exec_sem_arch_cakeProg, since it's not architecture-specific *)
 (* 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 =
diff --git a/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml
new file mode 100644
index 0000000..d32d416
--- /dev/null
+++ b/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml
@@ -0,0 +1,370 @@
+open HolKernel boolLib Parse bossLib;
+
+val _ = new_theory "p4_exec_sem_vss_cakeProg";
+
+open p4Syntax;
+open bitstringSyntax numSyntax;
+open p4Theory;
+open p4_auxTheory;
+open p4_exec_semTheory;
+open p4_coreTheory p4_vssTheory;
+
+(* 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);
+
+(* VSS architecture functions *)
+
+Definition vss_reduce_nonout'_def:
+ (vss_reduce_nonout' ([], elist, v_map) =
+  SOME []
+ ) /\
+ (vss_reduce_nonout' (d::dlist, e::elist, v_map) =
+  if is_d_out d
+  then oCONS (e, vss_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, vss_reduce_nonout' (dlist, elist, v_map))
+       else oCONS (e_v (init_out_v_cake v), vss_reduce_nonout' (dlist, elist, v_map))       
+      | _ => NONE)
+    | _ => NONE)) /\
+ (vss_reduce_nonout' (_, _, v_map) = NONE)
+End
+
+Definition vss_copyin_pbl'_def:
+ vss_copyin_pbl' (xlist, dlist, elist, (counter, ext_obj_map, v_map, ctrl):vss_ascope) =
+  case vss_reduce_nonout' (dlist, elist, v_map) of
+  | SOME elist' =>
+   copyin' xlist dlist elist' [v_map_to_scope v_map] [ [] ]
+  | NONE => NONE
+End
+
+(* TODO: Generic. Upstream to regular arch scripts? *)
+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 vss_copyout_pbl'_def:
+ vss_copyout_pbl' (g_scope_list, (counter, ext_obj_map, v_map, ctrl):vss_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):vss_ascope)
+    | NONE => NONE)
+  | _ => NONE
+End
+
+Definition vss_packet_in_extract_gen_def:
+ (vss_packet_in_extract_gen ascope_lookup (ascope_update:num #
+    (num # (core_v_ext + vss_v_ext)) list #
+    (string # p4$v) list #
+    (string # (((e list -> bool) # num) # string # e list) list) list ->
+    num ->
+    core_v_ext + vss_v_ext ->
+    num #
+    (num # (core_v_ext + vss_v_ext)) list #
+    (string # p4$v) list #
+    (string # (((e list -> bool) # num) # string # e list) list) list) ascope_update_v_map (ascope:vss_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, vss_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, vss_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, vss_v_ext) sum)) "parseError" (v_bit (fixwidth 32 (n2v 1), 32)), scope_list, status_trans "reject")
+        | NONE => NONE)
+       | _ => NONE)
+    | NONE => NONE)
+  | _ => NONE
+ )
+End
+
+(* TODO: Why do we need to fix the packet_in_extract stuff? *)
+Definition vss_packet_in_extract'_def:
+ vss_packet_in_extract':((num #
+  (num # (core_v_ext + vss_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 + vss_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) = vss_packet_in_extract_gen vss_ascope_lookup vss_ascope_update vss_ascope_update_v_map
+End
+
+Definition Checksum16_construct'_def:
+ (Checksum16_construct' ((counter, ext_obj_map, v_map, ctrl):vss_ascope, g_scope_list:g_scope_list, scope_list) =
+  let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (vss_v_ext_ipv4_checksum ([]:(bool list) list))) in
+  (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)
+ )
+End
+
+Definition Checksum16_clear'_def:
+ (Checksum16_clear' ((counter, ext_obj_map, v_map, ctrl):vss_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) =>
+   SOME ((counter, AUPDATE ext_obj_map (i, INR (vss_v_ext_ipv4_checksum ([]:(bool list) list))), v_map, ctrl), scope_list, status_returnv v_bot)
+  | _ => NONE
+ )
+End
+
+Definition Checksum16_update'_def:
+ (Checksum16_update' ((counter, ext_obj_map, v_map, ctrl):vss_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 ALOOKUP ext_obj_map i of
+    | SOME (INR (vss_v_ext_ipv4_checksum ipv4_checksum)) =>
+     (case get_checksum_incr'' scope_list (lval_varname (varn_name "data")) of
+      | SOME checksum_incr =>
+       SOME ((counter, AUPDATE ext_obj_map (i, INR (vss_v_ext_ipv4_checksum (ipv4_checksum ++ checksum_incr))), v_map, ctrl), scope_list, status_returnv v_bot)
+      | NONE => NONE)
+    | _ => NONE)
+  | _ => NONE
+ )
+End
+
+(* TODO: Upstream this and the below two? *)
+Definition compute_checksum16'_def:
+ (compute_checksum16' ([]:(bool list) list) = (fixwidth 16 $ n2v 0)) /\
+ (compute_checksum16' ((h::t):(bool list) list) =
+  add_ones_complement' (h, compute_checksum16' (t:(bool list) list))
+ )
+End
+(* TODO: Better name *)
+Definition ALOOKUP'_inner_def:
+ ALOOKUP'_inner ipv4_checksum =
+    if all_lists_length_16 ipv4_checksum
+    then
+     SOME $ MAP $~ $ compute_checksum16' ipv4_checksum
+    else NONE
+End
+(* TODO: Better name *)
+Definition ALOOKUP'_def:
+ ALOOKUP' alist el =
+  case ALOOKUP alist el of
+   | SOME (INR (vss_v_ext_ipv4_checksum ipv4_checksum)) =>
+    ALOOKUP'_inner ipv4_checksum
+   | _ => NONE
+End
+
+Definition Checksum16_get'_def:
+ (Checksum16_get' ((counter, ext_obj_map, v_map, ctrl):vss_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 ALOOKUP' ext_obj_map i of
+    | SOME ipv4_checksum' =>
+     SOME ((counter, ext_obj_map, v_map, ctrl):vss_ascope, scope_list, status_returnv (v_bit (ipv4_checksum', 16)))
+    | _ => NONE)
+  | _ => NONE
+ )
+End
+
+(* TODO: Move to p4_exec_sem_arch_cakeProg, since it's not architecture-specific *)
+(* 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
+
+fun mk_v_bitii' (num, width) =
+ let
+  val width_tm = numSyntax.term_of_int width
+ in
+  mk_v_bit $ pairSyntax.mk_pair (bitstringSyntax.mk_fixwidth (width_tm, bitstringSyntax.mk_n2v $ numSyntax.term_of_int num), width_tm)
+ end
+;
+
+(*
+(* TODO: Hack, some type mismatch when using regular syntax functions *)
+val (v_header_tm, mk_v_header, dest_v_header, is_v_header) =
+  syntax_fns2 "p4" "v_header";
+fun mk_v_header_list vbit x_v_l =
+  mk_v_header (vbit, (listSyntax.mk_list ((map (fn (a, b) => mk_pair (a, b)) x_v_l), ``:(string # p4$v) ``)));
+val (v_struct_tm, mk_v_struct, dest_v_struct, is_v_struct) =
+  syntax_fns1 "p4" "v_struct";
+fun mk_v_struct_list x_v_l =
+  mk_v_struct (listSyntax.mk_list ((map (fn (a, b) => mk_pair (a, b)) x_v_l), ``:(string # p4$v)``));
+
+val ipv4_header_uninit =
+ mk_v_header_list F 
+                  [(``"version"``, mk_v_bitii' (0, 4)),
+                   (``"ihl"``, mk_v_bitii' (0, 4)),
+                   (``"diffserv"``, mk_v_bitii' (0, 8)),
+                   (``"totalLen"``, mk_v_bitii' (0, 16)),
+                   (``"identification"``, mk_v_bitii' (0, 16)),
+                   (``"flags"``, mk_v_bitii' (0, 3)),
+                   (``"fragOffset"``, mk_v_bitii' (0, 13)),
+                   (``"ttl"``, mk_v_bitii' (0, 8)),
+                   (``"protocol"``, mk_v_bitii' (0, 8)),
+                   (``"hdrChecksum"``, mk_v_bitii' (0, 16)),
+                   (``"srcAddr"``, mk_v_bitii' (0, 32)),
+                   (``"dstAddr"``, mk_v_bitii' (0, 32))];
+val ethernet_header_uninit =
+ mk_v_header_list F
+                  [(``"dstAddr"``, mk_v_bitii' (0, 48)),
+                   (``"srcAddr"``, mk_v_bitii' (0, 48)),
+                   (``"etherType"``, mk_v_bitii' (0, 16))];
+val vss_parsed_packet_struct_uninit =
+ mk_v_struct_list [(``"ethernet"``, ethernet_header_uninit), (``"ip"``, ipv4_header_uninit)];
+*)
+
+
+val _ = translation_extends "p4_exec_sem_arch_cakeProg";
+
+val _ = ml_prog_update (open_module "p4_exec_sem_vss_cake");
+
+val _ = translate arch_multi_exec'_def;
+
+val _ = translate vss_parser_runtime_def;
+
+val _ = translate vss_input_f_def;
+
+val _ = translate vss_lookup_obj_def;
+val _ = translate vss_output_f_def;
+
+val _ = translate v_map_to_scope_def;
+val _ = translate oCONS_def;
+val _ = translate vss_reduce_nonout'_def;
+val _ = translate vss_copyin_pbl'_def;
+
+val _ = translate scope_to_vmap_def;
+val _ = translate copyout_pbl_gen'_def;
+val _ = translate vss_copyout_pbl'_def;
+
+val _ = translate FOLDL_MATCH_def;
+val _ = translate ctrl_check_ttl_def;
+val _ = translate vss_apply_table_f_def;
+
+val _ = translate header_is_valid_def;
+
+val _ = translate header_set_valid_def;
+
+val _ = translate header_set_invalid_def;
+
+val _ = translate vss_ascope_update_v_map_def;
+val _ = translate verify_gen_def;
+val _ = translate vss_verify;
+
+val _ = translate Checksum16_construct'_def;
+
+val _ = translate Checksum16_clear'_def;
+
+val _ = translate oTAKE_DROP_def;
+val _ = translate v2w16s'''_def;
+val _ = translate header_entries2v_def;
+val _ = translate v2w16s''_def;
+val _ = translate get_checksum_incr''_def;
+val _ = translate Checksum16_update'_def;
+
+val _ = translate add_with_carry'_def;
+val _ = translate add_ones_complement'_def;
+val _ = translate compute_checksum16'_def;
+val _ = translate all_lists_length_16_def;
+val _ = translate ALOOKUP'_inner_def;
+(* TODO: Clean up proof *)
+Theorem alookup'_inner_side:
+!v1. alookup'_inner_side v1
+Proof
+simp[Once $ definition "alookup'_inner_side_def"] \\
+Induct >- (
+ simp[Once $ theorem "compute_checksum16'_side_def", all_lists_length_16_def]
+) \\
+rpt strip_tac \\
+gs[all_lists_length_16_def] \\
+gs[Once $ theorem "compute_checksum16'_side_def"] \\
+Cases_on ‘v1’ >- (
+ simp[theorem "compute_checksum16'_side_def"] \\
+ gs[compute_checksum16'_def, Once $ definition "add_ones_complement'_side_def",
+    Once $ definition "add_with_carry'_side_def"] \\
+ rpt strip_tac >- (
+  gs[]
+ ) >- (
+  gs[bitstringTheory.fixwidth_def, AllCaseEqs(), bitstringTheory.zero_extend_def, listTheory.PAD_LEFT]
+ ) >- (
+  gs[]
+ ) \\
+ gs[bitstringTheory.fixwidth_def, AllCaseEqs(), bitstringTheory.zero_extend_def, listTheory.PAD_LEFT]
+) \\
+qpat_x_assum ‘!x2 x1. _’ (fn thm => ASSUME_TAC $ Q.SPECL [‘h'’, ‘t’] thm) \\
+simp[Once $ theorem "compute_checksum16'_side_def", all_lists_length_16_def] \\
+simp[Once $ definition "add_ones_complement'_side_def", Once $ definition "add_with_carry'_side_def"] \\
+rpt strip_tac >- (
+ gs[]
+) >- (
+ gs[compute_checksum16'_def, add_ones_complement'_def, add_with_carry'_def, AllCaseEqs(), bitstringTheory.fixwidth_def, AllCaseEqs(), bitstringTheory.zero_extend_def, listTheory.PAD_LEFT]
+) >- (
+ gs[]
+) >- (
+ gs[bitstringTheory.fixwidth_def, AllCaseEqs(), bitstringTheory.zero_extend_def, listTheory.PAD_LEFT]
+) \\
+simp[Once $ theorem "compute_checksum16'_side_def", all_lists_length_16_def]
+QED
+val _ = update_precondition alookup'_inner_side;
+val _ = translate ALOOKUP'_def;
+val _ = translate Checksum16_get'_def;
+
+val _ = translate vss_ascope_update_def;
+val _ = translate vss_ascope_lookup_def;
+val _ = translate update_ascope_gen_def;
+val _ = translate oTAKE_DROP_def;
+val _ = translate set_bit_def;
+val _ = translate set_bool_def;
+val _ = translate size_in_bits_def;
+val _ = translate set_fields_def;
+val _ = translate set_header_def;
+
+val _ = translate lookup_ascope_gen_def;
+val _ = translate lookup_lval_header_def;
+val _ = translate packet_in_extract_gen_def;
+val _ = translate vss_packet_in_extract_gen_def;
+val _ = translate vss_packet_in_extract'_def;
+
+val _ = translate flatten_v_l_def;
+val _ = translate packet_out_emit_gen_def;
+val _ = translate vss_packet_out_emit;
+
+val _ = translate vss_pre_deparser_def;
+
+val _ = ml_prog_update (close_module NONE);
+
+val _ = export_theory ();
diff --git a/hol/cake_export/p4_vss_example_cakeProgScript.sml b/hol/cake_export/p4_vss_example_cakeProgScript.sml
new file mode 100644
index 0000000..ca6bcb8
--- /dev/null
+++ b/hol/cake_export/p4_vss_example_cakeProgScript.sml
@@ -0,0 +1,492 @@
+open HolKernel boolLib Parse bossLib;
+
+val _ = new_theory "p4_vss_example_cakeProg";
+
+open p4Syntax;
+open bitstringSyntax numSyntax;
+open p4Theory;
+open p4_auxTheory;
+open p4_exec_semTheory;
+open p4_coreTheory p4_vssTheory;
+
+(* CakeML: *)
+open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory mlmapTheory basisFunctionsLib
+     astPP comparisonTheory;
+
+open p4_exec_sem_vss_cakeProgTheory;
+
+open fromSexpTheory;
+
+intLib.deprecate_int();
+val _ = (max_print_depth := 100);
+
+val _ = translation_extends "p4_exec_sem_vss_cakeProg";
+
+(***************)
+(* VSS example *)
+
+val vss_actx =
+   “([arch_block_inp;
+      arch_block_pbl "parser"
+        [e_var (varn_name "b"); e_var (varn_name "parsedHeaders")];
+      arch_block_ffbl "parser_runtime";
+      arch_block_pbl "pipe"
+        [e_var (varn_name "headers"); e_var (varn_name "parseError");
+         e_var (varn_name "inCtrl"); e_var (varn_name "outCtrl")];
+      arch_block_ffbl "pre_deparser";
+      arch_block_pbl "deparser"
+        [e_var (varn_name "outputHeaders"); e_var (varn_name "b")];
+      arch_block_out],
+     [("parser",pbl_type_parser,[("b",d_none); ("p",d_out)],
+       [("parser",
+         stmt_seq
+           (stmt_ass lval_null
+              (e_call (funn_inst "Checksum16") [e_var (varn_name "ck")]))
+           (stmt_trans (e_v (v_str "start"))),[])],
+       [(varn_name "ck",tau_ext,NONE)],
+       [("start",
+         stmt_block []
+           (stmt_seq
+              (stmt_ass lval_null
+                 (e_call (funn_ext "packet_in" "extract")
+                    [e_var (varn_name "b");
+                     e_acc (e_var (varn_name "p")) "ethernet"]))
+              (stmt_trans
+                 (e_select
+                    (e_struct
+                       [("",
+                         e_acc (e_acc (e_var (varn_name "p")) "ethernet")
+                           "etherType")])
+                    [([s_sing (v_bit (fixwidth 16 $ n2v 2048,16))],"parse_ipv4")] "reject"))));
+        ("parse_ipv4",
+         stmt_block []
+           (stmt_seq
+              (stmt_ass lval_null
+                 (e_call (funn_ext "packet_in" "extract")
+                    [e_var (varn_name "b");
+                     e_acc (e_var (varn_name "p")) "ip"]))
+              (stmt_seq
+                 (stmt_ass lval_null
+                    (e_call (funn_ext "" "verify")
+                       [e_binop
+                          (e_acc (e_acc (e_var (varn_name "p")) "ip")
+                             "version") binop_eq (e_v (v_bit (fixwidth 4 $ n2v 4,4)));
+                        e_v (v_bit (fixwidth 32 $ n2v 8,32))]))
+                 (stmt_seq
+                    (stmt_ass lval_null
+                       (e_call (funn_ext "" "verify")
+                          [e_binop
+                             (e_acc (e_acc (e_var (varn_name "p")) "ip")
+                                "ihl") binop_eq (e_v (v_bit (fixwidth 4 $ n2v 5,4)));
+                           e_v (v_bit (fixwidth 32 $ n2v 7,32))]))
+                    (stmt_seq
+                       (stmt_ass lval_null
+                          (e_call (funn_ext "Checksum16" "clear")
+                             [e_var (varn_name "ck")]))
+                       (stmt_seq
+                          (stmt_ass lval_null
+                             (e_call (funn_ext "Checksum16" "update")
+                                [e_var (varn_name "ck");
+                                 e_acc (e_var (varn_name "p")) "ip"]))
+                          (stmt_seq
+                             (stmt_ass lval_null
+                                (e_call (funn_ext "" "verify")
+                                   [e_binop
+                                      (e_call (funn_ext "Checksum16" "get")
+                                         [e_var (varn_name "ck")]) binop_eq
+                                      (e_v (v_bit (fixwidth 16 $ n2v 0,16)));
+                                    e_v (v_bit (fixwidth 32 $ n2v 9,32))]))
+                             (stmt_trans (e_v (v_str "accept"))))))))))],[]);
+      ("pipe",pbl_type_control,
+       [("headers",d_inout); ("parseError",d_in); ("inCtrl",d_in);
+        ("outCtrl",d_out)],
+       [("pipe",
+         stmt_block []
+           (stmt_seq
+              (stmt_cond
+                 (e_binop (e_var (varn_name "parseError")) binop_neq
+                    (e_v (v_bit (fixwidth 32 $ n2v 0,32))))
+                 (stmt_seq
+                    (stmt_ass lval_null (e_call (funn_name "Drop_action") []))
+                    (stmt_ret (e_v v_bot))) stmt_empty)
+              (stmt_seq
+                 (stmt_seq
+                    (stmt_app "ipv4_match"
+                       [e_acc (e_acc (e_var (varn_name "headers")) "ip")
+                          "dstAddr"])
+                    (stmt_cond
+                       (e_binop
+                          (e_acc (e_var (varn_name "outCtrl")) "outputPort")
+                          binop_eq (e_var (varn_name "DROP_PORT")))
+                       (stmt_ret (e_v v_bot)) stmt_empty))
+                 (stmt_seq
+                    (stmt_seq
+                       (stmt_app "check_ttl"
+                          [e_acc (e_acc (e_var (varn_name "headers")) "ip")
+                             "ttl"])
+                       (stmt_cond
+                          (e_binop
+                             (e_acc (e_var (varn_name "outCtrl"))
+                                "outputPort") binop_eq
+                             (e_var (varn_name "CPU_OUT_PORT")))
+                          (stmt_ret (e_v v_bot)) stmt_empty))
+                    (stmt_seq
+                       (stmt_seq
+                          (stmt_app "dmac" [e_var (varn_name "nextHop")])
+                          (stmt_cond
+                             (e_binop
+                                (e_acc (e_var (varn_name "outCtrl"))
+                                   "outputPort") binop_eq
+                                (e_var (varn_name "CPU_OUT_PORT")))
+                             (stmt_ret (e_v v_bot)) stmt_empty))
+                       (stmt_app "smac"
+                          [e_acc (e_var (varn_name "outCtrl")) "outputPort"]))))),
+         []);
+        ("Drop_action",
+         stmt_seq
+           (stmt_ass
+              (lval_field (lval_varname (varn_name "outCtrl")) "outputPort")
+              (e_var (varn_name "DROP_PORT"))) (stmt_ret (e_v v_bot)),[]);
+        ("Set_nhop",
+         stmt_seq
+           (stmt_ass (lval_varname (varn_name "nextHop"))
+              (e_var (varn_name "ipv4_dest")))
+           (stmt_seq
+              (stmt_ass
+                 (lval_field
+                    (lval_field (lval_varname (varn_name "headers")) "ip")
+                    "ttl")
+                 (e_binop
+                    (e_acc (e_acc (e_var (varn_name "headers")) "ip") "ttl")
+                    binop_sub (e_v (v_bit (fixwidth 8 $ n2v 1,8)))))
+              (stmt_seq
+                 (stmt_ass
+                    (lval_field (lval_varname (varn_name "outCtrl"))
+                       "outputPort") (e_var (varn_name "port")))
+                 (stmt_ret (e_v v_bot)))),
+         [("ipv4_dest",d_none); ("port",d_none)]);
+        ("Send_to_cpu",
+         stmt_seq
+           (stmt_ass
+              (lval_field (lval_varname (varn_name "outCtrl")) "outputPort")
+              (e_var (varn_name "CPU_OUT_PORT"))) (stmt_ret (e_v v_bot)),[]);
+        ("Set_dmac",
+         stmt_seq
+           (stmt_ass
+              (lval_field
+                 (lval_field (lval_varname (varn_name "headers")) "ethernet")
+                 "dstAddr") (e_var (varn_name "dmac")))
+           (stmt_ret (e_v v_bot)),[("dmac",d_none)]);
+        ("Set_smac",
+         stmt_seq
+           (stmt_ass
+              (lval_field
+                 (lval_field (lval_varname (varn_name "headers")) "ethernet")
+                 "srcAddr") (e_var (varn_name "smac")))
+           (stmt_ret (e_v v_bot)),[("smac",d_none)])],
+       [(varn_name "nextHop",tau_bit 32,NONE)],[],
+       [("ipv4_match",[mk_lpm],"Drop_action",[]);
+        ("check_ttl",[mk_exact],"NoAction",[]);
+        ("dmac",[mk_exact],"Drop_action",[]);
+        ("smac",[mk_exact],"Drop_action",[])]);
+      ("deparser",pbl_type_control,[("p",d_inout); ("b",d_none)],
+       [("deparser",
+         stmt_block []
+           (stmt_seq
+              (stmt_ass lval_null
+                 (e_call (funn_inst "Checksum16") [e_var (varn_name "ck")]))
+              (stmt_seq
+                 (stmt_ass lval_null
+                    (e_call (funn_ext "packet_out" "emit")
+                       [e_var (varn_name "b");
+                        e_acc (e_var (varn_name "p")) "ethernet"]))
+                 (stmt_seq
+                    (stmt_cond
+                       (e_call (funn_ext "header" "isValid")
+                          [e_acc (e_var (varn_name "p")) "ip"])
+                       (stmt_seq
+                          (stmt_ass lval_null
+                             (e_call (funn_ext "Checksum16" "clear")
+                                [e_var (varn_name "ck")]))
+                          (stmt_seq
+                             (stmt_ass
+                                (lval_field
+                                   (lval_field (lval_varname (varn_name "p"))
+                                      "ip") "hdrChecksum")
+                                (e_v (v_bit (fixwidth 16 $ n2v 0,16))))
+                             (stmt_seq
+                                (stmt_ass lval_null
+                                   (e_call (funn_ext "Checksum16" "update")
+                                      [e_var (varn_name "ck");
+                                       e_acc (e_var (varn_name "p")) "ip"]))
+                                (stmt_ass
+                                   (lval_field
+                                      (lval_field
+                                         (lval_varname (varn_name "p")) "ip")
+                                      "hdrChecksum")
+                                   (e_call (funn_ext "Checksum16" "get")
+                                      [e_var (varn_name "ck")])))))
+                       stmt_empty)
+                    (stmt_ass lval_null
+                       (e_call (funn_ext "packet_out" "emit")
+                          [e_var (varn_name "b");
+                           e_acc (e_var (varn_name "p")) "ip"]))))),[])],
+       [(varn_name "ck",tau_ext,NONE)],[],[])],
+     [("parser_runtime",ffblock_ff vss_parser_runtime);
+      ("pre_deparser",ffblock_ff vss_pre_deparser)],
+     vss_input_f
+       (v_struct
+          [("ethernet",
+            v_header F
+              [("dstAddr",
+                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; F;
+                    F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F],48));
+               ("srcAddr",
+                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; F;
+                    F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F],48));
+               ("etherType",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16))]);
+           ("ip",
+            v_header F
+              [("version",v_bit ([F; F; F; F],4));
+               ("ihl",v_bit ([F; F; F; F],4));
+               ("diffserv",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("totalLen",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16));
+               ("identification",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16));
+               ("flags",v_bit ([F; F; F],3));
+               ("fragOffset",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F],13));
+               ("ttl",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("protocol",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("hdrChecksum",
+                v_bit
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16));
+               ("srcAddr",
+                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));
+               ("dstAddr",
+                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))])]),
+     vss_output_f,vss_copyin_pbl',vss_copyout_pbl',vss_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,[("verify",[("condition",d_in); ("err",d_in)],vss_verify)]);
+      ("packet_in",NONE,
+       [("extract",[("this",d_in); ("headerLvalue",d_out)],
+         vss_packet_in_extract')(* ;
+        ("lookahead",[("this",d_in); ("dummy_T",d_in)],
+         vss_packet_in_lookahead);
+        ("advance",[("this",d_in); ("bits",d_in)],vss_packet_in_advance) *)]);
+      ("packet_out",NONE,
+       [("emit",[("this",d_in); ("data",d_in)],vss_packet_out_emit)]);
+      ("Checksum16",SOME ([("this",d_out)],Checksum16_construct'),
+       [("clear",[("this",d_in)],Checksum16_clear');
+        ("update",[("this",d_in); ("data",d_in)],Checksum16_update');
+        ("get",[("this",d_in)],Checksum16_get')])],
+     [("NoAction",stmt_ret (e_v v_bot),[])]):vss_ascope actx”
+
+(* TODO: Apart from the table and extern configurations, this seems close to a generic P4 initial state *)
+val vss_astate = “((0,
+       [],[],0,[],[("parseError",v_bit (REPLICATE 32 F,32))],
+       [("ipv4_match",
+         [(($= [e_v (v_bit (REPLICATE 32 F,32))],0),"Set_nhop",
+           [e_v (v_bit (fixwidth 32 $ n2v 1,32)); e_v (v_bit (REPLICATE 4 F,4))])]);
+        ("dmac",
+         [(($= [e_v (v_bit (fixwidth 32 $ n2v 1,32))],0),"Set_dmac",
+           [e_v (v_bit (fixwidth 48 $ n2v 1,48))])]);
+        ("smac",
+         [(($= [e_v (v_bit (REPLICATE 4 F,4))],0),"Set_smac",
+           [e_v (v_bit (REPLICATE 48 F,48))])])]),
+      [[(varn_name "REAL_PORT_COUNT",v_bit (fixwidth 4 $ n2v 8,4),NONE);
+        (varn_name "RECIRCULATE_IN_PORT",v_bit (fixwidth 4 $ n2v 13,4),NONE);
+        (varn_name "CPU_IN_PORT",v_bit (fixwidth 4 $ n2v 14,4),NONE);
+        (varn_name "DROP_PORT",v_bit (fixwidth 4 $ n2v 15,4),NONE);
+        (varn_name "CPU_OUT_PORT",v_bit (fixwidth 4 $ n2v 14,4),NONE);
+        (varn_name "RECIRCULATE_OUT_PORT",v_bit (fixwidth 4 $ n2v 13,4),NONE);
+        (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):vss_ascope astate”;
+
+val n_max = “180:num”;
+
+
+(*************************)
+(* Generic wrapper parts *)
+
+Definition vss_exec_def:
+ vss_exec input =
+  case
+   arch_multi_exec' ^vss_actx
+    (p4_append_input_list [input] ^vss_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 vss_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))
+ ;
+
+(* From VSS TTL example, with symbolic bits made concrete with arbitrary values *)
+val input = “([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; 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; 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; F; F; F; F; T; F; F; F; F; F; F; F; F; F;
+          F; F; F; T; F; F; F; T; F; T; F; F; F; F; F; F; F; F; F; F; F; F;
+          F; F; F; F; F; F; F; T; F; T; F; F;
+          F; F; F; F; F; F; F; T; F; T; F; F; F;
+          F; F; F; F; F; F; F; T; F; T; F; F; F;
+          F; F; F; F; F; F; F; F; F; F; F; F; F; T; F; F;
+          F; F; F; F; F; F; F; T; F; T; F; F; F;
+          F; F; F; F; F; F; F; T; F; T; F;
+          F; F; F; F; F; F; F; T; F; T;
+          F; F; F; F; F; F; F; T; F;
+          F; F; F; F; F; F; F; T; 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; 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; F;
+          F; F],1:num)”;
+val bl_input_tm = fst $ dest_pair input
+
+
+EVAL “arch_multi_exec ^vss_actx (p4_append_input_list [^input] ^vss_astate) 140”
+
+EVAL “vss_exec ^input”
+
+val bl_input = String.implode $ deparse_bool_list $ fst $ listSyntax.dest_list bl_input_tm
+
+Definition vss_exec_old_def:
+ vss_exec_old input =
+  case
+   arch_multi_exec ^vss_actx
+    (p4_append_input_list [input] ^vss_astate) ^n_max of
+  | SOME res => SOME $ p4_get_output_list res
+  | NONE => NONE
+End
+
+EVAL “vss_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 vss_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 "vss_example.sexp" prog;
+    
+val _ = export_theory ();
diff --git a/hol/p4_auxScript.sml b/hol/p4_auxScript.sml
index aca456c..a75fac1 100644
--- a/hol/p4_auxScript.sml
+++ b/hol/p4_auxScript.sml
@@ -35,6 +35,37 @@ Definition oLASTN_def:
   | 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
+
+Theorem oTAKE_DROP_SOME:
+!n l take rest.
+oTAKE_DROP n l = SOME (take,rest) ==>
+oTAKE n l = SOME take /\ oDROP n l = SOME rest
+Proof
+Induct_on ‘l’ >- (
+ rpt strip_tac >> (
+  Cases_on ‘n’ >> (
+   gs[oTAKE_def, oDROP_def, oTAKE_DROP_def]
+  )
+ )
+) >>
+rpt strip_tac >> (
+ Cases_on ‘n’ >> (
+  gs[oTAKE_def, oDROP_def, oTAKE_DROP_def, AllCaseEqs()]
+ )
+) >>
+res_tac >>
+gvs[]
+QED
+
 Theorem oTAKE_imp_TAKE:
 !i l l'.
 oTAKE i l = SOME l' ==>
@@ -116,6 +147,32 @@ subgoal ‘oDROP (LENGTH l1) (l1 ++ l2) = SOME (DROP (LENGTH l1) (l1 ++ l2))’
 fs[rich_listTheory.DROP_LENGTH_APPEND]
 QED
 
+Theorem oDROP_LENGTH:
+!n l l' take rest.
+oDROP n l = SOME l' ==>
+LENGTH l >= n /\
+LENGTH l' = LENGTH l - n
+Proof
+Induct_on ‘l’ >- (
+ rpt strip_tac >> (
+  Cases_on ‘n’ >> (
+   gs[oDROP_def]
+  )
+ )
+) >>
+rpt strip_tac >- (
+ Cases_on ‘n’ >> (
+  gs[oDROP_def]
+ ) >>
+ res_tac >>
+ FULL_SIMP_TAC arith_ss []
+) >>
+Cases_on ‘n’ >> (
+ gs[oDROP_def]
+) >>
+gvs[]
+QED
+
 Theorem oTAKE_APPEND:
 !l1 l2.
 oTAKE (LENGTH l1) (l1 ++ l2) = SOME l1
diff --git a/hol/p4_coreScript.sml b/hol/p4_coreScript.sml
index 6702c5e..b277fdf 100644
--- a/hol/p4_coreScript.sml
+++ b/hol/p4_coreScript.sml
@@ -171,16 +171,6 @@ Definition set_bit_def:
   | 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 =
@@ -401,20 +391,20 @@ End
 (************)
 
 Definition header_entries2v_def:
- (header_entries2v [] = SOME []) /\
- (header_entries2v (h::t) =
-  case header_entry2v h of
+ (header_entries2v (INL []) = SOME []) /\
+ (header_entries2v (INL (h::t)) =
+  case header_entries2v (INR h) of
   | SOME bl =>
-  (case header_entries2v t of
+  (case header_entries2v (INL t) of
    | SOME bl2 => SOME (bl++bl2)
    | NONE => NONE)
   | NONE => NONE
  ) /\
- (header_entry2v (x:x, v) =
+ (header_entries2v (INR (x:x, v)) =
   case v of
   | (v_bit (bl, n)) => SOME bl
-  | (v_struct x_v_l) => header_entries2v x_v_l
-  | (v_header validity x_v_l) => header_entries2v x_v_l
+  | (v_struct x_v_l) => header_entries2v (INL x_v_l)
+  | (v_header validity x_v_l) => header_entries2v (INL x_v_l)
   | _ => NONE
  )
 Termination
@@ -442,11 +432,11 @@ Definition get_checksum_incr_def:
     | SOME (v_bit (bl, n)) =>
      if n MOD 16 = 0 then SOME (v2w16s' bl) else NONE
     | SOME (v_header vbit f_list) =>
-     (case header_entries2v f_list of
+     (case header_entries2v (INL f_list) of
       | SOME bl => v2w16s bl
       | NONE => NONE)
     | SOME (v_struct f_list) =>
-     (case header_entries2v f_list of
+     (case header_entries2v (INL f_list) of
       | SOME bl => v2w16s bl
       | NONE => NONE)
     | _ => NONE)
@@ -460,12 +450,12 @@ Definition get_checksum_incr'_def:
     | SOME (v_bit (bl, n)) =>
      if n MOD 16 = 0 then SOME bl else NONE
     | SOME (v_header vbit f_list) =>
-     (case header_entries2v f_list of
+     (case header_entries2v (INL f_list) of
       | SOME bl =>
        if (LENGTH bl) MOD 16 = 0 then SOME bl else NONE
       | NONE => NONE)
     | SOME (v_struct f_list) =>
-     (case header_entries2v f_list of
+     (case header_entries2v (INL f_list) of
       | SOME bl =>
        if (LENGTH bl) MOD 16 = 0 then SOME bl else NONE
       | NONE => NONE)
@@ -503,11 +493,11 @@ Definition get_bitlist_def:
   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
+    (case header_entries2v (INL f_list) of
      | SOME bl => SOME bl
      | NONE => NONE)
    | SOME (v_struct f_list) =>
-    (case header_entries2v f_list of
+    (case header_entries2v (INL f_list) of
      | SOME bl => SOME bl
      | NONE => NONE)
    | _ => NONE
diff --git a/hol/p4_ebpfScript.sml b/hol/p4_ebpfScript.sml
index d6b34c0..f79f2fe 100644
--- a/hol/p4_ebpfScript.sml
+++ b/hol/p4_ebpfScript.sml
@@ -201,15 +201,6 @@ Definition v_map_to_scope_def:
 End
 *)
 
-Definition scope_to_vmap_def:
- (scope_to_vmap [] = SOME []) /\
- (scope_to_vmap ((vn, (v:v, lval_opt:lval option))::t) =
-  case vn of
-   | (varn_name k) => oCONS ((k, v), scope_to_vmap t)
-   | _ => NONE
- )
-End
-
 (* TODO: Since the same thing should be initialised
  *       for all known architectures, maybe it should be made a
  *       architecture-generic (core) function? *)
diff --git a/hol/p4_test_vss_ttlScript.sml b/hol/p4_test_vss_ttlScript.sml
index 47cbb01..b07acc8 100644
--- a/hol/p4_test_vss_ttlScript.sml
+++ b/hol/p4_test_vss_ttlScript.sml
@@ -42,48 +42,22 @@ val input_ok = mk_eth_frame_ok input_ipv4_ok;
 val init_inlist_ok = mk_list ([mk_pair (input_ok, input_port_ok)], ``:in_out``);
 val init_outlist_ok = mk_list ([], ``:in_out``);
 
-val ipv4_header_uninit =
- mk_v_header_list F 
-                  [(``"version"``, mk_v_biti_arb 4),
-                   (``"ihl"``, mk_v_biti_arb 4),
-                   (``"diffserv"``, mk_v_biti_arb 8),
-                   (``"totalLen"``, mk_v_biti_arb 16),
-                   (``"identification"``, mk_v_biti_arb 16),
-                   (``"flags"``, mk_v_biti_arb 3),
-                   (``"fragOffset"``, mk_v_biti_arb 13),
-                   (``"ttl"``, mk_v_biti_arb 8),
-                   (``"protocol"``, mk_v_biti_arb 8),
-                   (``"hdrChecksum"``, mk_v_biti_arb 16),
-                   (``"srcAddr"``, mk_v_biti_arb 32),
-                   (``"dstAddr"``, mk_v_biti_arb 32)];
-
-val ethernet_header_uninit =
- mk_v_header_list F
-                  [(``"dstAddr"``, mk_v_biti_arb 48),
-                   (``"srcAddr"``, mk_v_biti_arb 48),
-                   (``"etherType"``, mk_v_biti_arb 16)];
-
-val parsed_packet_struct_uninit =
- mk_v_struct_list [(``"ethernet"``, ethernet_header_uninit), (``"ip"``, ipv4_header_uninit)];
-
-
-val init_counter = ``3:num``;
-
-val init_ext_obj_map = ``[(0, INL (core_v_ext_packet []));
-                          (1, INL (core_v_ext_packet []));
-                          (2, INL (core_v_ext_packet []))]:(num, (core_v_ext + vss_v_ext)) alist``;
+val init_counter = ``0:num``;
+
+val init_ext_obj_map = ``[]:(num, (core_v_ext + vss_v_ext)) alist``;
 
 (* All variables used in the architectural scope need to be declared *)
-(* NOTE: the output packet is here called "data_crc". VSS spec has both input and output called "b" *)
+(*
 val init_v_map = ``[("inCtrl", v_struct [("inputPort", ^(mk_v_biti_arb 4))]);
                     ("outCtrl", v_struct [("outputPort", ^(mk_v_biti_arb 4))]);
-                    ("b_in", v_ext_ref 0);
-                    ("b_out", v_ext_ref 1);
-                    ("data_crc", v_ext_ref 2);
-                    ("parsedHeaders", (^parsed_packet_struct_uninit));
-                    ("headers", (^parsed_packet_struct_uninit));
-                    ("outputHeaders", (^parsed_packet_struct_uninit));
+                    ("b", v_ext_ref 0);
+                    ("b_temp", v_ext_ref 1);
+                    ("parsedHeaders", (^vss_parsed_packet_struct_uninit));
+                    ("headers", (^vss_parsed_packet_struct_uninit));
+                    ("outputHeaders", (^vss_parsed_packet_struct_uninit));
                     ("parseError", ^(mk_v_bitii (0,32)))]:(string, v) alist``;
+*)
+val init_v_map = ``[("parseError", ^(mk_v_bitii (0,32)))]:(string, v) alist``;
 
 (* Regular ethernet output ports are numbered 0-7 *)
 val init_ctrl = ``[("ipv4_match",
@@ -123,52 +97,52 @@ val init_astate =
 (***************************************)
 
 val ctx = ``p4_vss_actx``;
-val stop_consts_rewr = [``compute_checksum16``];
-Definition vss_updated_checksum16_def:
- vss_updated_checksum16 (w16_list:bool list) = 
-  word_1comp (sub_ones_complement (0xFEFFw, v2w w16_list)):word16
+val stop_consts_rewr = [``compute_checksum16'``];
+Definition vss_updated_checksum16'_def:
+ vss_updated_checksum16' (w16_list:bool list) = 
+  MAP $~ (sub_ones_complement' ([T; T; T; T; T; T; T; F; T; T; T; T; T; T; T; T], w16_list))
 End
-val stop_consts_never = [``vss_updated_checksum16``];
+val stop_consts_never = [``vss_updated_checksum16'``];
 
 val ass1 =
- ``compute_checksum16
-    [v2w [F; T; F; F; F; T; F; T; dscp0; dscp1; dscp2; dscp3;
+ ``compute_checksum16'
+    [[F; T; F; F; F; T; F; T; dscp0; dscp1; dscp2; dscp3;
 	  dscp4; dscp5; ecn0; ecn1];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; T; F; T; F; F];
-     v2w [id0; id1; id2; id3; id4; id5; id6; id7; id8; id9; id10;
+     [F; F; F; F; F; F; F; F; F; F; F; T; F; T; F; F];
+     [id0; id1; id2; id3; id4; id5; id6; id7; id8; id9; id10;
 	  id11; id12; id13; id14; id15];
-     v2w [fl0; fl1; fl2; fo0; fo1; fo2; fo3; fo4; fo5; fo6; fo7;
+     [fl0; fl1; fl2; fo0; fo1; fo2; fo3; fo4; fo5; fo6; fo7;
 	  fo8; fo9; fo10; fo11; fo12];
-     v2w [F; F; F; F; F; F; F; T; pr0; pr1; pr2; pr3; pr4; pr5;
+     [F; F; F; F; F; F; F; T; pr0; pr1; pr2; pr3; pr4; pr5;
 	  pr6; pr7];
-     v2w [hc0; hc1; hc2; hc3; hc4; hc5; hc6; hc7; hc8; hc9; hc10; hc11; hc12;
+     [hc0; hc1; hc2; hc3; hc4; hc5; hc6; hc7; hc8; hc9; hc10; hc11; hc12;
 	  hc13; hc14; hc15];
-     v2w [src0; src1; src2; src3; src4; src5; src6; src7; src8;
+     [src0; src1; src2; src3; src4; src5; src6; src7; src8;
 	  src9; src10; src11; src12; src13; src14; src15];
-     v2w [src16; src17; src18; src19; src20; src21; src22; src23;
+     [src16; src17; src18; src19; src20; src21; src22; src23;
 	  src24; src25; src26; src27; src28; src29; src30; src31];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F]] = (0w:word16)``;
+     [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]] = [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F]``;
 
 (* New result due to updated TTL value: same as if 0x0100 and the previous checksum was no longer added to the sum *)
 val ass2 =
- ``compute_checksum16
-    [v2w [F; T; F; F; F; T; F; T; dscp0; dscp1; dscp2; dscp3;
+ ``compute_checksum16'
+    [[F; T; F; F; F; T; F; T; dscp0; dscp1; dscp2; dscp3;
 	  dscp4; dscp5; ecn0; ecn1];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; T; F; T; F; F];
-     v2w [id0; id1; id2; id3; id4; id5; id6; id7; id8; id9; id10;
+     [F; F; F; F; F; F; F; F; F; F; F; T; F; T; F; F];
+     [id0; id1; id2; id3; id4; id5; id6; id7; id8; id9; id10;
 	  id11; id12; id13; id14; id15];
-     v2w [fl0; fl1; fl2; fo0; fo1; fo2; fo3; fo4; fo5; fo6; fo7;
+     [fl0; fl1; fl2; fo0; fo1; fo2; fo3; fo4; fo5; fo6; fo7;
 	  fo8; fo9; fo10; fo11; fo12];
-     v2w [F; F; F; F; F; F; F; F; pr0; pr1; pr2; pr3; pr4; pr5;
+     [F; F; F; F; F; F; F; F; pr0; pr1; pr2; pr3; pr4; pr5;
 	  pr6; pr7];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F];
-     v2w [src0; src1; src2; src3; src4; src5; src6; src7; src8;
+     [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F];
+     [src0; src1; src2; src3; src4; src5; src6; src7; src8;
 	  src9; src10; src11; src12; src13; src14; src15];
-     v2w [src16; src17; src18; src19; src20; src21; src22; src23;
+     [src16; src17; src18; src19; src20; src21; src22; src23;
 	  src24; src25; src26; src27; src28; src29; src30; src31];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F];
-     v2w [F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F]] = vss_updated_checksum16 [hc0; hc1; hc2; hc3; hc4; hc5; hc6; hc7; hc8; hc9; hc10; hc11; hc12; hc13; hc14; hc15]``;
+     [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]] = vss_updated_checksum16' [hc0; hc1; hc2; hc3; hc4; hc5; hc6; hc7; hc8; hc9; hc10; hc11; hc12; hc13; hc14; hc15]``;
 val ctxt = CONJ (ASSUME ass1) (ASSUME ass2);
 
 (*************************************************)
@@ -178,7 +152,7 @@ val ctxt = CONJ (ASSUME ass1) (ASSUME ass2);
 (* 180 steps for TTL=1 packet to get forwarded to CPU *)
 
 (* Theorem on line below proves data non-interference using proof approach 1 *)
-GEN_ALL $ eval_under_assum vss_arch_ty ctx init_astate stop_consts_rewr stop_consts_never ctxt 180;
+GEN_ALL $ eval_under_assum vss_arch_ty ctx init_astate stop_consts_rewr stop_consts_never ctxt 180 (* 180 *);
 
 
 (************************************************************************************************************)
@@ -207,7 +181,7 @@ val ctx' = ``p4_vss_actx'``;
 
 (* EVAL-uate until packet is output (happens to be step 180) *)
 (* Theorem on line below proves data non-interference using proof approach 2 *)
-GEN_ALL $ EVAL ``arch_multi_exec (^ctx') (^init_astate) 181``;
+GEN_ALL $ EVAL ``arch_multi_exec ^ctx' ^init_astate 181``;
 
 
 (**************************************************)
diff --git a/hol/p4_v1modelScript.sml b/hol/p4_v1modelScript.sml
index 93813ca..58a506f 100644
--- a/hol/p4_v1modelScript.sml
+++ b/hol/p4_v1modelScript.sml
@@ -618,16 +618,6 @@ Definition v_map_to_scope_def:
 End
 *)
 
-(* TODO: Generalise and move to core? Duplicated in all three architectures... *)
-Definition scope_to_vmap_def:
- (scope_to_vmap [] = SOME []) /\
- (scope_to_vmap ((vn, (v:v, lval_opt:lval option))::t) =
-  case vn of
-   | (varn_name k) => oCONS ((k, v), scope_to_vmap t)
-   | _ => NONE
- )
-End
-
 (* TODO: Since the same thing should be initialised
  *       for all known architectures, maybe it should be made a
  *       architecture-generic (core) function? *)
@@ -708,7 +698,6 @@ Definition v1model_is_drop_port_def:
 End
 
 (* TODO: Outsource obtaining the output port to an external function? *)
-(* NOTE: "b" renamed to "b_out" *)
 (* A little clumsy with the double v2n, but that makes things easier *)
 Definition v1model_output_f_def:
  v1model_output_f (in_out_list:in_out_list, (counter, ext_obj_map, v_map, ctrl):v1model_ascope) =
diff --git a/hol/p4_vssLib.sig b/hol/p4_vssLib.sig
index b25f094..3dafebb 100644
--- a/hol/p4_vssLib.sig
+++ b/hol/p4_vssLib.sig
@@ -33,6 +33,9 @@ val vss_func_map : term
 
 val vss_init_counter : term
 val vss_init_ext_obj_map : term
+
+val vss_parsed_packet_struct_uninit : term
+
 val vss_init_v_map : term
 
 end
diff --git a/hol/p4_vssLib.sml b/hol/p4_vssLib.sml
index 6e231e7..4a91d9e 100644
--- a/hol/p4_vssLib.sml
+++ b/hol/p4_vssLib.sml
@@ -26,7 +26,11 @@ val vss_init_global_scope =
     (varn_name "CPU_IN_PORT", (^CPU_IN_PORT_tm, NONE) );
     (varn_name "DROP_PORT", (^DROP_PORT_tm, NONE) );
     (varn_name "CPU_OUT_PORT", (^CPU_OUT_PORT_tm, NONE) );
-    (varn_name "RECIRCULATE_OUT_PORT", (^RECIRCULATE_OUT_PORT_tm, NONE) )
+    (varn_name "RECIRCULATE_OUT_PORT", (^RECIRCULATE_OUT_PORT_tm, NONE) );
+    (varn_name "gen_apply_result",
+     v_struct
+       [("hit",v_bool F); ("miss",v_bool F);
+	("action_run",v_bit (REPLICATE 32 F,32))],NONE)
    ]:scope``;
 
 (*******************************************)
@@ -82,12 +86,15 @@ val vss_func_map = core_func_map;
 (***********************)
 (* Architectural state *)
 
-val vss_init_counter = term_of_int 3;
+val vss_init_counter = term_of_int 0;
 
+val vss_init_ext_obj_map = ``[]:(num, vss_sum_v_ext) alist``;
+(*
 val vss_init_ext_obj_map = ``[(0, INL (core_v_ext_packet []));
 			      (1, INL (core_v_ext_packet []));
 			      (2, INL (core_v_ext_packet []))]:(num, vss_sum_v_ext) alist``;
-(*
+*)
+
 val ipv4_header_uninit =
  mk_v_header_list F 
                   [(``"version"``, mk_v_biti_arb 4),
@@ -102,19 +109,24 @@ val ipv4_header_uninit =
                    (``"hdrChecksum"``, mk_v_biti_arb 16),
                    (``"srcAddr"``, mk_v_biti_arb 32),
                    (``"dstAddr"``, mk_v_biti_arb 32)];
+
 val ethernet_header_uninit =
  mk_v_header_list F
                   [(``"dstAddr"``, mk_v_biti_arb 48),
                    (``"srcAddr"``, mk_v_biti_arb 48),
                    (``"etherType"``, mk_v_biti_arb 16)];
+
 val vss_parsed_packet_struct_uninit =
  mk_v_struct_list [(``"ethernet"``, ethernet_header_uninit), (``"ip"``, ipv4_header_uninit)];
-*)
+
+val vss_init_v_map = ``^core_init_v_map:(string, v) alist``;
+(*
 val vss_init_v_map = ``^core_init_v_map ++
                        [("inCtrl", v_struct [("inputPort", ^(mk_v_biti_arb 4))]);
 			("outCtrl", v_struct [("outputPort", ^(mk_v_biti_arb 4))]);
-			("b_in", v_ext_ref 0);
-			("b_out", v_ext_ref 1);
+			("b", v_ext_ref 0);
+			("b_temp", v_ext_ref 1);
 			("data_crc", v_ext_ref 2)]:(string, v) alist``;
+*)
 
 end
diff --git a/hol/p4_vssScript.sml b/hol/p4_vssScript.sml
index df6d62d..89ce569 100644
--- a/hol/p4_vssScript.sml
+++ b/hol/p4_vssScript.sml
@@ -1,12 +1,12 @@
 open HolKernel boolLib Parse bossLib ottLib;
 
-open p4Theory p4_auxTheory p4_coreTheory;
-
 val _ = new_theory "p4_vss";
 
+open p4Theory p4_auxTheory p4_coreTheory;
+    
 Datatype:
  vss_v_ext =
-   vss_v_ext_ipv4_checksum (word16 list)
+   vss_v_ext_ipv4_checksum ((bool list) list)
 End
 val _ = type_abbrev("vss_sum_v_ext", ``:(core_v_ext, vss_v_ext) sum``);
 
@@ -68,9 +68,9 @@ End
 (*************)
 (* construct *)
 
-Definition Checksum16_construct:
+Definition Checksum16_construct_def:
  (Checksum16_construct ((counter, ext_obj_map, v_map, ctrl):vss_ascope, g_scope_list:g_scope_list, scope_list) =
-  let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (vss_v_ext_ipv4_checksum ([]:word16 list))) in
+  let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (vss_v_ext_ipv4_checksum ([]:(bool list) list))) in
   (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)
@@ -82,11 +82,11 @@ End
 (*********)
 (* clear *)
 
-Definition Checksum16_clear:
+Definition Checksum16_clear_def:
  (Checksum16_clear ((counter, ext_obj_map, v_map, ctrl):vss_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) =>
-   SOME ((counter, AUPDATE ext_obj_map (i, INR (vss_v_ext_ipv4_checksum ([]:word16 list))), v_map, ctrl), scope_list, status_returnv v_bot)
+   SOME ((counter, AUPDATE ext_obj_map (i, INR (vss_v_ext_ipv4_checksum ([]:(bool list) list))), v_map, ctrl), scope_list, status_returnv v_bot)
   | _ => NONE
  )
 End
@@ -95,14 +95,54 @@ End
 (**********)
 (* update *)
 
+Definition v2w16s'''_def:
+ (v2w16s''' [] = SOME []) /\
+ (v2w16s''' v =
+  case oTAKE_DROP 16 v of
+  | SOME (taken, left) =>
+   (case v2w16s''' left of
+    | SOME l =>
+     SOME (taken::l)
+    | NONE => NONE)
+  | _ => NONE
+ )
+Termination
+WF_REL_TAC `measure LENGTH` >>
+rpt strip_tac >>
+imp_res_tac oTAKE_DROP_SOME >>
+imp_res_tac oDROP_LENGTH >>
+gs[]
+End
+   
+Definition v2w16s''_def:
+ (v2w16s'' v = if (LENGTH v) MOD 16 = 0 then (v2w16s''' v) else NONE)
+End
+
+Definition get_checksum_incr''_def:
+ (get_checksum_incr'' scope_list ext_data_name =
+   (case lookup_lval' scope_list ext_data_name of
+    | SOME (v_bit (bl, n)) =>
+     if n MOD 16 = 0 then (v2w16s''' bl) else NONE
+    | SOME (v_header vbit f_list) =>
+     (case header_entries2v (INL f_list) of
+      | SOME bl => v2w16s'' bl
+      | NONE => NONE)
+    | SOME (v_struct f_list) =>
+     (case header_entries2v (INL f_list) of
+      | SOME bl => v2w16s'' bl
+      | NONE => NONE)
+    | _ => NONE)
+ )
+End
+
 (* Note that this assumes the order of fields in the header is correct *)
-Definition Checksum16_update:
+Definition Checksum16_update_def:
  (Checksum16_update ((counter, ext_obj_map, v_map, ctrl):vss_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 ALOOKUP ext_obj_map i of
     | SOME (INR (vss_v_ext_ipv4_checksum ipv4_checksum)) =>
-     (case get_checksum_incr scope_list (lval_varname (varn_name "data")) of
+     (case get_checksum_incr'' scope_list (lval_varname (varn_name "data")) of
       | SOME checksum_incr =>
        SOME ((counter, AUPDATE ext_obj_map (i, INR (vss_v_ext_ipv4_checksum (ipv4_checksum ++ checksum_incr))), v_map, ctrl), scope_list, status_returnv v_bot)
       | NONE => NONE)
@@ -115,13 +155,114 @@ End
 (*******)
 (* get *)
 
-Definition Checksum16_get:
+(* TODO: carry_in hard-coded as false *)
+(* TODO: This is the bitvector version of the function on words *)
+(* TODO: Would be nice if this function could be made total *)
+(*
+Definition add_with_carry'_def:
+ add_with_carry' (x,y) =
+  case (x,y) of
+  | ([],[]) => NONE
+  | ([],_) => NONE
+  | (_,[]) => NONE
+  | _ =>
+   let
+    unsigned_sum = v2n x + v2n y;
+    result = fixwidth 16 $ n2v unsigned_sum;
+    carry_out = (v2n result <> unsigned_sum) and
+    overflow =
+      ((HD x <=> HD y) /\ (HD x <=/=> HD result))
+   in
+    SOME (result,carry_out,overflow)
+End
+
+(* TODO: This is the bitvector version of the function on words *)
+Definition add_ones_complement'_def:
+ add_ones_complement' (x, y) =
+  case add_with_carry' (x, y) of
+  | SOME (result,carry_out,overflow) =>
+   if carry_out
+   then SOME $ fixwidth 16 $ n2v (v2n result + 1)
+   else SOME result
+  | NONE => NONE
+End
+
+Definition sub_ones_complement'_def:
+ sub_ones_complement' (x, y) =
+  case add_with_carry' (x, MAP $~ y) of
+  | SOME (result,carry_out,overflow) =>
+   if carry_out
+   then SOME $ fixwidth 16 $ n2v (v2n result + 1)
+   else SOME $ MAP $~ result
+  | NONE => NONE
+End
+
+Definition compute_checksum16'_def:
+ compute_checksum16' (w16_list:(bool list) list) = 
+  case (FOLDR (\a b_opt. case b_opt of SOME b => (add_ones_complement' (a,b)) | NONE => NONE) (SOME (fixwidth 16 $ n2v 0)) w16_list) of
+  | SOME res => SOME $ MAP $~ res
+  | NONE => NONE
+End
+*)
+
+(* TODO: carry_in hard-coded as false *)
+(* TODO: This is the bitvector version of the function on words *)
+Definition add_with_carry'_def:
+ add_with_carry' (x,y) =
+  let
+   unsigned_sum = v2n x + v2n y;
+   result = fixwidth 16 $ n2v unsigned_sum;
+   carry_out = (v2n result <> unsigned_sum) and
+   overflow =
+     ((HD x <=> HD y) /\ (HD x <=/=> HD result))
+  in
+   (result,carry_out,overflow)
+End
+
+(* TODO: This is the bitvector version of the function on words *)
+Definition add_ones_complement'_def:
+ add_ones_complement' (x, y) =
+  let
+   (result,carry_out,overflow) = add_with_carry' (x, y)
+  in
+   if carry_out
+   then fixwidth 16 $ n2v (v2n result + 1)
+   else result
+End
+
+Definition sub_ones_complement'_def:
+ sub_ones_complement' (x, y) =
+  let
+   (result,carry_out,overflow) = add_with_carry' (x, MAP $~ y)
+  in
+   if carry_out
+   then fixwidth 16 $ n2v (v2n result + 1)
+   else MAP $~ result
+End
+
+Definition compute_checksum16'_def:
+ compute_checksum16' (w16_list:(bool list) list) = 
+  MAP $~  (FOLDR (CURRY add_ones_complement') (fixwidth 16 $ n2v 0) w16_list)
+End
+
+Definition all_lists_length_16_def:
+ (all_lists_length_16 ([]:(bool list) list) = T) /\
+ (all_lists_length_16 (h::t) = 
+   if LENGTH h = 16
+   then all_lists_length_16 t
+   else F)
+End
+
+Definition Checksum16_get_def:
  (Checksum16_get ((counter, ext_obj_map, v_map, ctrl):vss_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 ALOOKUP ext_obj_map i of
     | SOME (INR (vss_v_ext_ipv4_checksum ipv4_checksum)) =>
-     SOME ((counter, ext_obj_map, v_map, ctrl):vss_ascope, scope_list, status_returnv (v_bit (w16 (compute_checksum16 ipv4_checksum))))
+     if all_lists_length_16 ipv4_checksum
+     then
+     SOME ((counter, ext_obj_map, v_map, ctrl):vss_ascope, scope_list, status_returnv (v_bit (compute_checksum16' ipv4_checksum, 16)))
+     else NONE
     | _ => NONE)
   | _ => NONE
  )
@@ -132,52 +273,33 @@ End
 (*                     MODEL-SPECIFIC                     *)
 (**********************************************************)
 
+(*
 Definition get_optional_bits:
  get_optional_bits header = ((v2n (TAKE 4 (DROP 116 header)))*32) - 160
 End
+*)
 
 (* TODO: This should also arbitrate between different ports, taking a list of lists of input *)
-(* NOTE: VSS example starts out at the data link layer (physical layer ignored):
- * https://en.wikipedia.org/wiki/Ethernet_frame#Frame_%E2%80%93_data_link_layer *)
-(* NOTE: VSS example uses only Ethernet II framing:
- * https://en.wikipedia.org/wiki/Ethernet_frame#Ethernet_II *)
-
-(* The first 14 bytes are always the Eth-II header.
- * The last 4 bytes are always the CRC checksum.
- * In between these is the IPv4 payload. The first 16 bytes
- * of this are mandatory fields. Depending on the IHL header
- * field, 0-46 bytes of option field follows. *)
-(* NOTE: "b" renamed to "b_in" *)
-(* TODO: Note that this also resets parseError to 0 *)
 Definition vss_input_f_def:
-  (vss_input_f (io_list:in_out_list, (counter, ext_obj_map, v_map, ctrl):vss_ascope) =
-   case io_list of
-   | [] => NONE
-   | ((bl,p)::t) =>
-    let frame_length = LENGTH bl in
-    let optional_bits = get_optional_bits bl in
-    (case oTAKE (272+optional_bits) bl of
-     | SOME header =>
-      (case oDROP (272+optional_bits) bl of
-       | SOME data_crc =>
-        (case ALOOKUP v_map "b_in" of
-         | SOME (v_ext_ref i) =>
-          let ext_obj_map' = AUPDATE ext_obj_map (i, INL (core_v_ext_packet header)) in
-          (case ALOOKUP v_map "data_crc" of
-           | SOME (v_ext_ref i') =>
-            let ext_obj_map'' = AUPDATE ext_obj_map' (i', INL (core_v_ext_packet data_crc)) in
-             (* TODO: Below is a bit of a hack. We should replace all "AUPDATE" with an assign
-              * function for vss_ascope. *)
-             let v_map' = AUPDATE v_map ("inCtrl", v_struct [("inputPort", v_bit (w4 (n2w p)))]) in
-             let v_map'' = AUPDATE v_map' ("parseError", v_bit (fixwidth 32 (n2v 0), 32)) in
-              SOME (t, (counter, ext_obj_map'', v_map'', ctrl):vss_ascope)
-           | _ => NONE)
-         | _ => NONE)
-       | NONE => NONE)
-     | NONE => NONE)
-   | _ => NONE)
+ (vss_input_f tau_uninit_v (io_list:in_out_list, (counter, ext_obj_map, v_map, ctrl):vss_ascope) =
+  case io_list of
+  | [] => NONE
+  | ((bl,p)::t) =>
+   (* TODO: Currently, no garbage collection in ext_obj_map is done *)
+   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));
+                                    ("parsedHeaders", tau_uninit_v);
+                                    ("inCtrl", v_struct [("inputPort", v_bit (fixwidth 4 (n2v p), 4)  )]);
+                                    (* TODO: What should be the default value here? Is this undefined? *)
+                                    ("outCtrl", v_struct [("outputPort", v_bit (fixwidth 4 (n2v p), 4) )]);
+                                    ("parseError", v_bit (fixwidth 32 (n2v 0), 32))] in
+    SOME (t, (counter', ext_obj_map', v_map', ctrl):vss_ascope))
 End
 
+(* TODO: Make general in p4_core *)
 Definition vss_reduce_nonout_def:
  (vss_reduce_nonout ([], elist, v_map) =
   SOME []
@@ -223,11 +345,22 @@ End
 
 Definition vss_parser_runtime_def:
  vss_parser_runtime ((counter, ext_obj_map, v_map, ctrl):vss_ascope) =
-  (case ALOOKUP v_map "parsedHeaders" of
-   | SOME (v_struct hdrs) =>
-    let v_map' = AUPDATE v_map ("headers", v_struct hdrs) in
-     SOME (counter, ext_obj_map, v_map', ctrl)
-   | _ => NONE)
+  (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 "parsedHeaders" of
+         | SOME (v_struct hdrs) =>
+          let v_map' = AUPDATE v_map ("headers", v_struct hdrs) in
+          let ext_obj_map' = AUPDATE ext_obj_map (i, INL (core_v_ext_packet [])) in
+          let ext_obj_map'' = AUPDATE ext_obj_map' (i', INL (core_v_ext_packet bl)) in
+           SOME (counter, ext_obj_map'', v_map', ctrl)
+         | _ => NONE)
+       | _ => NONE)
+     | _ => NONE)
+   | _ => NONE) 
 End
 
 Definition vss_pre_deparser_def:
@@ -247,15 +380,12 @@ Definition vss_lookup_obj_def:
   | _ => NONE
 End
 
-(* Add new header + data + Ethernet CRC as a tuple with new output port to output list *)
-(* Add data + Ethernet CRC *)
 (* TODO: Outsource obtaining the output port to an external function? *)
-(* NOTE: "b" renamed to "b_out" *)
 Definition vss_output_f_def:
  vss_output_f (in_out_list:in_out_list, (counter, ext_obj_map, v_map, ctrl):vss_ascope) =
-  (case vss_lookup_obj ext_obj_map v_map "b_out" of
+  (case vss_lookup_obj ext_obj_map v_map "b" of
    | SOME (INL (core_v_ext_packet headers)) =>
-    (case vss_lookup_obj ext_obj_map v_map "data_crc" of
+    (case vss_lookup_obj ext_obj_map v_map "b_temp" of
      | SOME (INL (core_v_ext_packet data_crc)) =>
       (case ALOOKUP v_map "outCtrl" of
        | SOME (v_struct [(fldname, v_bit (bl, n))]) =>
@@ -272,7 +402,7 @@ Definition vss_output_f_def:
    | _ => NONE)
 End
 
-Definition ctrl_check_ttl:
+Definition ctrl_check_ttl_def:
  (ctrl_check_ttl e_l =
   case e_l of
   | [e] =>
diff --git a/hol/p4_vss_exampleScript.sml b/hol/p4_vss_exampleScript.sml
index 6d15780..84c68ec 100644
--- a/hol/p4_vss_exampleScript.sml
+++ b/hol/p4_vss_exampleScript.sml
@@ -1,12 +1,12 @@
 open HolKernel boolLib Parse bossLib;
 
+val _ = new_theory "p4_vss_example";
+
 open p4Theory p4_vssTheory;
 open pairSyntax listSyntax p4Syntax;
 
 open p4_vssLib;
 
-val _ = new_theory "p4_vss_example";
-
 (* This file contains the VSS example program. Specifically, it saves a theorem
  * that contains the architectural context of the program. *)
 
@@ -84,7 +84,7 @@ val vss_parser_pbl =
  ``(pbl_type_parser, [("b", d_none); ("p", d_out)], [("parser", (^vss_parser_inits, []))], (^vss_parser_decl_list), (^vss_parser_pmap), []):pblock``;
 
 val vss_parser_ab =
- ``arch_block_pbl "parser" [e_var (varn_name "b_in"); e_var (varn_name "parsedHeaders")]``;
+ ``arch_block_pbl "parser" [e_var (varn_name "b"); e_var (varn_name "parsedHeaders")]``;
 
 
 (************)
@@ -197,7 +197,7 @@ val vss_deparser_body =
 
 val vss_deparser_pbl = ``(pbl_type_control, [("p", d_inout); ("b", d_none)], [("deparser", (^vss_deparser_body, []))], (^vss_deparser_decl_list), [], (^vss_deparser_tblmap)):pblock``;
 
-val vss_deparser_ab = ``arch_block_pbl "deparser" [e_var (varn_name "outputHeaders"); e_var (varn_name "b_out")]``;
+val vss_deparser_ab = ``arch_block_pbl "deparser" [e_var (varn_name "outputHeaders"); e_var (varn_name "b")]``;
 
 
 (**********************)
@@ -222,7 +222,7 @@ val vss_actx =
  ``(^(list_mk_pair [``(^vss_ab_list):ab_list``,
                     ``(^vss_pblock_map):pblock_map``,
                     ``(^vss_ffblock_map):vss_ascope ffblock_map``,
-                    ``(^vss_input_f):vss_ascope input_f``,
+                    ``(^vss_input_f ^vss_parsed_packet_struct_uninit):vss_ascope input_f``,
                     ``(^vss_output_f):vss_ascope output_f``,
                     ``(^vss_copyin_pbl):vss_ascope copyin_pbl``,
                     ``(^vss_copyout_pbl):vss_ascope copyout_pbl``,