From 58031bb2b73b7d3dab5cd4a0743c3ad324fb0da2 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Mon, 30 Dec 2024 18:01:51 +0100 Subject: [PATCH] Simplification of checksum computation in V1Model, export of to-bool cast --- .../p4_exec_sem_arch_cakeProgScript.sml | 51 +++++++++ .../p4_exec_sem_e_cakeProgScript.sml | 4 +- .../p4_exec_sem_v1model_cakeProgScript.sml | 5 +- .../p4_exec_sem_vss_cakeProgScript.sml | 48 -------- hol/p4_coreLib.sig | 5 + hol/p4_coreLib.sml | 3 + hol/p4_coreScript.sml | 104 +++++++++++++++++- hol/p4_exec_semScript.sml | 10 +- hol/p4_exec_sem_e_soundnessScript.sml | 17 ++- hol/p4_v1modelLib.sig | 5 - hol/p4_v1modelLib.sml | 3 - hol/p4_v1modelScript.sml | 46 ++++---- hol/p4_vssScript.sml | 98 ----------------- hol/symb_exec/p4_symb_exec_v1modelLib.sml | 8 +- 14 files changed, 219 insertions(+), 188 deletions(-) diff --git a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml index 14778b51..0a0e03bd 100644 --- a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml +++ b/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 (); diff --git a/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml index 28e7f945..62089fd8 100644 --- a/hol/cake_export/p4_exec_sem_e_cakeProgScript.sml +++ b/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; diff --git a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml index 1ec71703..3d3b0745 100644 --- a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml +++ b/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; diff --git a/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml index 35f2ef40..be40ff8a 100644 --- a/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml +++ b/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; diff --git a/hol/p4_coreLib.sig b/hol/p4_coreLib.sig index dd29df86..c61d748d 100644 --- a/hol/p4_coreLib.sig +++ b/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 diff --git a/hol/p4_coreLib.sml b/hol/p4_coreLib.sml index dbe93517..9b68762d 100644 --- a/hol/p4_coreLib.sml +++ b/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 diff --git a/hol/p4_coreScript.sml b/hol/p4_coreScript.sml index 8943f909..6fff184f 100644 --- a/hol/p4_coreScript.sml +++ b/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 = diff --git a/hol/p4_exec_semScript.sml b/hol/p4_exec_semScript.sml index a7e45e84..5c2498fa 100644 --- a/hol/p4_exec_semScript.sml +++ b/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 diff --git a/hol/p4_exec_sem_e_soundnessScript.sml b/hol/p4_exec_sem_e_soundnessScript.sml index 5b6dc44a..02083e2f 100644 --- a/hol/p4_exec_sem_e_soundnessScript.sml +++ b/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` >> ( diff --git a/hol/p4_v1modelLib.sig b/hol/p4_v1modelLib.sig index 4b82005b..c3e4d62b 100644 --- a/hol/p4_v1modelLib.sig +++ b/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 diff --git a/hol/p4_v1modelLib.sml b/hol/p4_v1modelLib.sml index a39c5ff3..b72b0a4a 100644 --- a/hol/p4_v1modelLib.sml +++ b/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 diff --git a/hol/p4_v1modelScript.sml b/hol/p4_v1modelScript.sml index 03946963..51f979db 100644 --- a/hol/p4_v1modelScript.sml +++ b/hol/p4_v1modelScript.sml @@ -22,11 +22,9 @@ val _ = new_theory "p4_v1model"; val CONTROL_PLANE_API = 0; -(* TODO: v1model uses a checksum in the verify_checksum and update_checksum externs *) Datatype: v1model_v_ext = - v1model_v_ext_ipv4_checksum (word16 list) - | v1model_v_ext_counter + v1model_v_ext_counter | v1model_v_ext_direct_counter | v1model_v_ext_meter | v1model_v_ext_direct_meter @@ -229,22 +227,25 @@ Definition v1model_verify_checksum_def: | SOME $ v_bit (bl, n) => if v2n bl = 6 then - (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 => (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 - | SOME [v_map_scope] => - (case scope_to_vmap v_map_scope of - | SOME v_map' => - SOME ((counter, ext_obj_map, v_map', ctrl), scope_list, status_returnv v_bot) - | NONE => NONE) - | _ => NONE)) + (case compute_checksum16 checksum_incr of + | SOME bl'' => + (if (v_bit (bl', n')) = (v_bit (bl'', 16)) + 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 + | SOME [v_map_scope] => + (case scope_to_vmap v_map_scope of + | SOME v_map' => + SOME ((counter, ext_obj_map, v_map', ctrl), scope_list, status_returnv v_bot) + | NONE => NONE) + | _ => NONE)) + | _ => NONE) else NONE | _ => NONE) | NONE => NONE) @@ -259,11 +260,6 @@ End (*******************) (* update_checksum *) -Definition v1model_update_checksum_inner_def: - v1model_update_checksum_inner bitlist = - v_bit $ w16 $ compute_checksum16 $ v2w16s' bitlist -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 @@ -274,16 +270,18 @@ Definition v1model_update_checksum_def: | SOME $ v_bit (bl, n) => if v2n bl = 6 then - (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 => (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 - | SOME scope_list' => - SOME ((counter, ext_obj_map, v_map, ctrl), scope_list', status_returnv v_bot) | NONE => NONE) + (case compute_checksum16 checksum_incr of + | SOME res => + (case assign' scope_list (v_bit (res, 16)) (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) + | NONE => NONE) else NONE | _ => NONE) | NONE => NONE) diff --git a/hol/p4_vssScript.sml b/hol/p4_vssScript.sml index 0d2c83b6..87cb475e 100644 --- a/hol/p4_vssScript.sml +++ b/hol/p4_vssScript.sml @@ -95,46 +95,6 @@ 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_def: (Checksum16_update ((counter, ext_obj_map, v_map, ctrl):vss_ascope, g_scope_list:g_scope_list, scope_list) = @@ -155,64 +115,6 @@ End (*******) (* get *) -(* 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 ALOOKUP_compute_checksum16_def: ALOOKUP_compute_checksum16 alist el = case ALOOKUP alist el of diff --git a/hol/symb_exec/p4_symb_exec_v1modelLib.sml b/hol/symb_exec/p4_symb_exec_v1modelLib.sml index 6ec30386..22f17af5 100644 --- a/hol/symb_exec/p4_symb_exec_v1modelLib.sml +++ b/hol/symb_exec/p4_symb_exec_v1modelLib.sml @@ -114,19 +114,19 @@ fun approx_v1model_register_read p4_symb_arg_prefix fv_index scope_list ascope = fun approx_v1model_update_checksum p4_symb_arg_prefix fv_index scope_list = let (* TODO: HOL4P4_CONV? *) - val data_bitlist = dest_some $ rhs $ concl $ EVAL “get_checksum_incr' ^scope_list (lval_varname (varn_name "data"))” + val data_bitlist = dest_some $ rhs $ concl $ EVAL “get_checksum_incr'' ^scope_list (lval_varname (varn_name "data"))” - val tm1 = mk_v1model_update_checksum_inner data_bitlist + val tm1 = mk_compute_checksum16_inner data_bitlist val approx_vars = fixedwidth_freevars_fromindex (p4_symb_arg_prefix, fv_index, 16) - val rhs_tm = mk_v_bit $ mk_pair (approx_vars, term_of_int 16) + val rhs_tm = mk_some approx_vars val goal_tm = mk_disj_list [boolSyntax.list_mk_exists (fst $ dest_list approx_vars, mk_eq (tm1, rhs_tm))] val approx_thm = (* “^goal_tm” *) prove(goal_tm, - SIMP_TAC std_ss [disj_list_def, v1model_update_checksum_inner_def, p4Theory.v_11, p4Theory.w16_def, w2v_exists] + SIMP_TAC std_ss [disj_list_def, compute_checksum16_inner_def, p4Theory.v_11, p4Theory.w16_def, w2v_exists] ); in SOME (approx_thm, [fv_index+16])