Simplification of checksum computation in V1Model, export of to-bool …

…cast

hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml

@@ -170,6 +170,57 @@ val _ = translate header_set_invalid_def;
 val _ = translate p4_append_input_list_def;
 val _ = translate p4_get_output_list_def;
 
+(* Common extern functions: *)
+
+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 add_with_carry'_def;
+val _ = translate add_ones_complement'_def;
+val _ = translate compute_checksum16_inner_def;
+val _ = translate all_lists_length_16_def;
+val _ = translate compute_checksum16_def;
+Theorem compute_checksum16_side:
+!v1. compute_checksum16_side v1
+Proof
+simp[Once $ definition "compute_checksum16_side_def"] \\
+Induct >- (
+ simp[Once $ theorem "compute_checksum16_inner_side_def", all_lists_length_16_def]
+) \\
+rpt strip_tac \\
+gs[all_lists_length_16_def, Once $ theorem "compute_checksum16_inner_side_def"] \\
+Cases_on ‘v1’ >- (
+ gs[theorem "compute_checksum16_inner_side_def",
+    compute_checksum16_inner_def, Once $ definition "add_ones_complement'_side_def",
+    Once $ definition "add_with_carry'_side_def"] \\
+ rpt strip_tac \\ (
+  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_inner_side_def",
+     Once $ definition "add_ones_complement'_side_def",
+     Once $ definition "add_with_carry'_side_def"] \\
+rpt strip_tac >- (
+ gs[]
+) >- (
+ gs[compute_checksum16_inner_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_inner_side_def"]
+QED
+val _ = update_precondition compute_checksum16_side;
+
 val _ = ml_prog_update (close_module NONE);
 
 val _ = export_theory ();

hol/cake_export/p4_exec_sem_e_cakeProgScript.sml

@@ -176,6 +176,7 @@ Definition copyin'_def:
   all_arg_update_for_newscope' xlist dlist elist (ss_curr++gsl)
 End
 
+
 (**************)
 (* ARITHMETIC *)
 
@@ -230,7 +231,6 @@ Definition bitv_neq_def:
  bitv_neq a b = ~bitv_eq a b
 End
 
-
 Definition unop_exec'_def:
  (unop_exec' unop_neg (v_bool b) = SOME (v_bool ~b))
  /\
@@ -897,6 +897,8 @@ val _ = translate listTheory.DROP_def;
 val _ = translate bitstringTheory.fixwidth_def;
 val _ = translate bool_cast_def;
 val _ = translate bitv_cast_def;
+val _ = translate oHD_def;
+val _ = translate to_bool_cast_exec_def;
 val _ = translate cast_exec_def;
 val _ = translate e_exec_cast_def;
 

hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml

@@ -189,14 +189,15 @@ val _ = translate v1model_ascope_update_v_map_def;
 val _ = translate verify_gen_def;
 val _ = translate v1model_verify_def;
 
-(* TODO: verify_checksum, update_checksum *)
+val _ = translate v1model_verify_checksum_def;
+
+val _ = translate v1model_update_checksum_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;

hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml

@@ -166,62 +166,14 @@ 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_inner_def;
-val _ = translate all_lists_length_16_def;
-val _ = translate compute_checksum16_def;
-Theorem compute_checksum16_side:
-!v1. compute_checksum16_side v1
-Proof
-simp[Once $ definition "compute_checksum16_side_def"] \\
-Induct >- (
- simp[Once $ theorem "compute_checksum16_inner_side_def", all_lists_length_16_def]
-) \\
-rpt strip_tac \\
-gs[all_lists_length_16_def, Once $ theorem "compute_checksum16_inner_side_def"] \\
-Cases_on ‘v1’ >- (
- gs[theorem "compute_checksum16_inner_side_def",
-    compute_checksum16_inner_def, Once $ definition "add_ones_complement'_side_def",
-    Once $ definition "add_with_carry'_side_def"] \\
- rpt strip_tac \\ (
-  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_inner_side_def",
-     Once $ definition "add_ones_complement'_side_def",
-     Once $ definition "add_with_carry'_side_def"] \\
-rpt strip_tac >- (
- gs[]
-) >- (
- gs[compute_checksum16_inner_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_inner_side_def"]
-QED
-val _ = update_precondition compute_checksum16_side;
 val _ = translate ALOOKUP_compute_checksum16_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;

hol/p4_coreLib.sig

@@ -10,4 +10,9 @@ val core_ext_map : term
 
 val core_init_v_map : term
 
+val dest_compute_checksum16_inner : term -> term
+val is_compute_checksum16_inner : term -> bool
+val mk_compute_checksum16_inner : term -> term
+val compute_checksum16_inner_tm : term
+
 end

hol/p4_coreLib.sml

@@ -27,4 +27,7 @@ val core_ext_map =
 
 val core_init_v_map = ``[("parseError", v_bit (fixwidth 32 (n2v 0), 32) )]:(string, v) alist``;
 
+val (compute_checksum16_inner_tm, mk_compute_checksum16_inner, dest_compute_checksum16_inner, is_compute_checksum16_inner) =
+  syntax_fns1 "p4_core" "compute_checksum16_inner";
+
 end

hol/p4_coreScript.sml

@@ -412,7 +412,7 @@ Termination
 WF_REL_TAC `measure ( \ t. case t of | (INL x_v_l) => v1_size x_v_l | (INR (x,v)) => v_size v)`
 End
 
-
+(*
 Definition v2w16s'_def:
  (v2w16s' [] = []) /\
  (v2w16s' v =
@@ -463,7 +463,107 @@ Definition get_checksum_incr'_def:
     | _ => NONE)
  )
 End
+*)
+
+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
+
+(* 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_inner_def:
+ (compute_checksum16_inner ([]:(bool list) list) = (fixwidth 16 $ n2v 0)) /\
+ (compute_checksum16_inner ((h::t):(bool list) list) =
+  add_ones_complement' (h, compute_checksum16_inner (t:(bool list) 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 compute_checksum16_def:
+ compute_checksum16 ipv4_checksum =
+  if all_lists_length_16 ipv4_checksum
+  then
+   SOME $ MAP $~ $ compute_checksum16_inner ipv4_checksum
+  else NONE
+End
 
+(*
 Definition add_ones_complement_def:
  add_ones_complement (x, y) = 
   let
@@ -484,10 +584,12 @@ Definition sub_ones_complement_def:
     else word_1comp result
 End
 
+
 Definition compute_checksum16_def:
  compute_checksum16 (w16_list:word16 list) = 
   word_1comp (FOLDR (CURRY add_ones_complement) (0w:word16) w16_list)
 End
+*)
 
 Definition get_bitlist_def:
  get_bitlist scope_list ext_data_name =

hol/p4_exec_semScript.sml

@@ -45,6 +45,14 @@ Definition is_var_def:
  (is_var _ = F)
 End
 
+Definition to_bool_cast_exec_def:
+ to_bool_cast_exec bitv =
+  case oHD $ REVERSE $ FST bitv of
+  | SOME bit => SOME $ v_bool bit
+  | NONE => NONE
+End
+
+
 Definition unop_exec_def:
  (unop_exec unop_neg (v_bool b) = SOME (v_bool ~b))
  /\
@@ -68,7 +76,7 @@ Definition cast_exec_def:
  /\
  (cast_exec (cast_unsigned n) (v_bool b) = SOME (v_bit $ bool_cast n b))
  /\
- (cast_exec (cast_bool) (v_bit bitv) = SOME (v_bool $ to_bool_cast bitv))
+ (cast_exec cast_bool (v_bit bitv) = to_bool_cast_exec bitv)
  /\
  (cast_exec _ _ = NONE)
 End

hol/p4_exec_sem_e_soundnessScript.sml

@@ -552,6 +552,16 @@ Cases_on `is_v e` >| [
 ]
 QED
 
+Theorem oHD_SOME:
+!l h.
+oHD l = SOME h ==>
+HD l = h
+Proof
+Induct >> (
+ fs[listTheory.oHD_thm]
+)
+QED
+
 Theorem e_cast_exec_sound_red:
 !type e c.
 e_exec_sound type e ==>
@@ -580,8 +590,13 @@ Cases_on `is_v e` >| [
   irule ((valOf o find_clause_e_red) "e_cast_bitv") >>
   fs [clause_name_def],
 
+  Cases_on `x` >> (
+   fs[to_bool_cast_exec_def, AllCaseEqs()]
+  ) >>
   irule ((valOf o find_clause_e_red) "e_cast_to_bool") >>
-  fs [clause_name_def]
+  Cases_on `p` >> Cases_on `q` >> (
+   fs [clause_name_def, to_bool_cast_def, oHD_SOME]
+  )
  ],
 
  Cases_on `e_exec ctx g_scope_list scopes_stack e` >> (

hol/p4_v1modelLib.sig

@@ -42,9 +42,4 @@ val is_v1model_register_write_inner : term -> bool
 val mk_v1model_register_write_inner : term * term * term -> term
 val v1model_register_write_inner_tm : term
 
-val dest_v1model_update_checksum_inner : term -> term
-val is_v1model_update_checksum_inner : term -> bool
-val mk_v1model_update_checksum_inner : term -> term
-val v1model_update_checksum_inner_tm : term
-
 end

hol/p4_v1modelLib.sml

@@ -105,7 +105,4 @@ val (v1model_register_read_inner_tm,  mk_v1model_register_read_inner, dest_v1mod
 val (v1model_register_write_inner_tm,  mk_v1model_register_write_inner, dest_v1model_register_write_inner, is_v1model_register_write_inner) =
   syntax_fns3 "p4_v1model" "v1model_register_write_inner";
 
-val (v1model_update_checksum_inner_tm,  mk_v1model_update_checksum_inner, dest_v1model_update_checksum_inner, is_v1model_update_checksum_inner) =
-  syntax_fns1 "p4_v1model" "v1model_update_checksum_inner";
-
 end