Skip to content

Commit e1e46f4

Browse files
didriklundbergdidriklundberg
committed
Preliminary consequences of completing the proofs for switching the arithmetic
1 parent 761e726 commit e1e46f4

File tree

5 files changed

+319
-40
lines changed

5 files changed

+319
-40
lines changed

‎hol/cake_sem/metatheory/p4_cake_exec_sem_completenessScript.sml‎

Lines changed: 283 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1010,7 +1010,7 @@ gvs[e_exec'_def, p4_exec_semTheory.e_exec_def, AllCaseEqs()] >> (
10101010
gvs[unop_exec'_def, p4_exec_semTheory.e_exec_unop_def, p4_exec_semTheory.unop_exec_def] >>
10111011
gvs[AllCaseEqs()] >>
10121012
Cases_on ‘p’ >> (
1013-
gvs[unop_exec'_def, p4_exec_semTheory.e_exec_unop_def, p4_exec_semTheory.unop_exec_def]
1013+
gvs[unop_exec'_def, p4_exec_semTheory.e_exec_unop_def, p4_exec_semTheory.unop_exec_def, bitv_unop_def]
10141014
)
10151015
)
10161016
) >>
@@ -1289,7 +1289,7 @@ Theorem transform_match_all:
12891289
!dict x_v_l w_v'_l s_list s_list'.
12901290
transform_v dict (v_struct x_v_l) = SOME (v'_struct w_v'_l) ==>
12911291
oFOLDR (transform_s dict) s_list = SOME s_list' ==>
1292-
(match_all_exec (ZIP (SND (UNZIP x_v_l),s_list)) ==>
1292+
match_all_exec (ZIP (SND (UNZIP x_v_l),s_list) ==>
12931293
match_all' (ZIP (SND (UNZIP w_v'_l), FST $ UNZIP s_list')))
12941294
Proof
12951295
Induct_on ‘w_v'_l’ >- (
@@ -1365,8 +1365,11 @@ Induct >> (
13651365
PairCases_on ‘h’ >> gs[] >>
13661366
gvs[p4_exec_semTheory.match_all_exec_def, match_all'_def, oFOLDR_def, listTheory.FIND_def, listTheory.INDEX_FIND_def, AllCaseEqs()] >>
13671367
CONJ_TAC >- (
1368+
cheat
1369+
(* OLD:
13681370
gs[] >>
13691371
metis_tac[transform_match_all]
1372+
*)
13701373
) >>
13711374
‘INDEX_FIND 0
13721375
(\(s_list,x'). match_all' (ZIP (SND (UNZIP w_v'_l),s_list)))
@@ -1422,7 +1425,10 @@ DISJ2_TAC >>
14221425
PairCases_on ‘h’ >> gs[] >>
14231426
CONJ_TAC >- (
14241427
(* From ~match_all (ZIP (SND (UNZIP x_v_l),h0)) and transformation *)
1428+
(*
14251429
metis_tac[transform_match_all]
1430+
*)
1431+
cheat
14261432
) >>
14271433
metis_tac[transform_FIND_match_all_NONE]
14281434
QED
@@ -2444,7 +2450,7 @@ qpat_x_assum ‘e_exec
24442450
gs[bitv_binop_def, AllCaseEqs()]
24452451
)
24462452
) >> (
2447-
gvs[Once transform_v_def, p4_exec_semTheory.binop_exec_def, binop_exec'_def, p4_exec_semTheory.bitv_binop'_def, p4_exec_semTheory.get_bitv_binop'_def, AllCaseEqs()]
2453+
gvs[Once transform_v_def, p4_exec_semTheory.binop_exec_def, binop_exec'_def, bitv_binop_def, get_bitv_binop_def, AllCaseEqs()]
24482454
)
24492455
) >- (
24502456
(* Recursive: 2nd arg red *)
@@ -3509,28 +3515,294 @@ Definition transform_arch_frame_list_def:
35093515
SOME arch_frame_list'_empty)
35103516
End
35113517

3518+
open p4_cake_arch_v1modelTheory;
3519+
3520+
val _ = (max_print_depth := 100);
3521+
3522+
Theorem test_blah:
3523+
!l2.
3524+
FOLDL AUPDATE [] l2 = l2 ==>
3525+
~MEM q (MAP FST l2) ==>
3526+
FOLDL AUPDATE [(q,r)] l2 = (q,r)::l2
3527+
Proof
3528+
completeInduct_on ‘l2’ >>
3529+
gs[] >>
3530+
rpt strip_tac >>
3531+
QED
3532+
3533+
(* TODO: Only true if l2 has no duplicates... *)
3534+
Theorem AUPDATE_LIST_empty:
3535+
!l2.
3536+
ALL_DISTINCT $ MAP FST l2 ==>
3537+
AUPDATE_LIST [] l2 = l2
3538+
Proof
3539+
cheat
3540+
(*
3541+
Induct >> (
3542+
gs[AUPDATE_LIST_def, listTheory.FOLDL]
3543+
) >>
3544+
rpt strip_tac >>
3545+
Cases_on ‘h’ >>
3546+
gs[AUPDATE_def] >>
3547+
Cases_on ‘l2’ >>
3548+
Cases_on ‘q = q'’ >>
3549+
gvs[] >>
3550+
*)
3551+
QED
3552+
3553+
Theorem AUPDATE_LIST_v_map_lemma:
3554+
!dict v_map v_map' init_v_map init_v_map' new_v_map'.
3555+
transform_v_map dict (AUPDATE_LIST v_map init_v_map) = SOME new_v_map' ==>
3556+
transform_v_map dict v_map = SOME v_map' ==>
3557+
transform_v_map dict init_v_map = SOME init_v_map' ==>
3558+
AUPDATE_LIST v_map' init_v_map' = new_v_map'
3559+
Proof
3560+
cheat
3561+
QED
3562+
3563+
(* TODO: Table lists? *)
3564+
Theorem v1model_input_f'_completeness:
3565+
!dict tau1_uninit_v tau2_uninit_v tau1_uninit_v' tau2_uninit_v'.
3566+
transform_v dict tau1_uninit_v = SOME tau1_uninit_v' ==>
3567+
transform_v dict tau2_uninit_v = SOME tau2_uninit_v' ==>
3568+
transform_io_list aenv11 = SOME aenv'11 ==>
3569+
transform_ext_obj_map aenv14 = SOME aenv'14 ==>
3570+
transform_v_map dict aenv15 = SOME aenv'15 ==>
3571+
3572+
v1model_input_f (tau1_uninit_v,tau2_uninit_v)
3573+
(aenv11,aenv'13,aenv14,aenv15,aenv16) =
3574+
SOME (in_out_list'',s'23,scope'1,scope'2,scope'3) ==>
3575+
3576+
transform_io_list in_out_list'' = SOME s'21 ==>
3577+
transform_ext_obj_map scope'1 = SOME s'24 ==>
3578+
transform_v_map dict scope'2 = SOME s'25 ==>
3579+
3580+
v1model_input_f' (tau1_uninit_v',tau2_uninit_v')
3581+
(aenv'11,aenv'13,aenv'14,aenv'15,aenv'16) =
3582+
SOME (s'21,s'23,s'24,s'25,aenv'16)
3583+
Proof
3584+
rpt strip_tac >>
3585+
gvs[p4_v1modelTheory.v1model_input_f_def, v1model_input_f'_def, AllCaseEqs()] >>
3586+
gvs[transform_io_list_def, oFOLDR_def, AllCaseEqs()] >>
3587+
gs[AUPDATE_LIST_empty] >>
3588+
gvs[transform_ext_obj_map_def, oFOLDR_def, transform_core_v_ext_def, bool_list_to_byte_list_def, AllCaseEqs()] >>
3589+
(* TODO: All done apart from taking into account the hard-coded dict *)
3590+
irule AUPDATE_LIST_v_map_lemma >>
3591+
qexistsl_tac [‘dict’,
3592+
‘[("b",v_ext_ref 0); ("b_temp",v_ext_ref 1);
3593+
("standard_metadata",
3594+
v_struct
3595+
(AUPDATE
3596+
[("ingress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3597+
("egress_spec",v_bit ([F; F; F; F; F; F; F; F; F],9));
3598+
("egress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3599+
("instance_type",
3600+
v_bit
3601+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3602+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3603+
("packet_length",
3604+
v_bit
3605+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3606+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3607+
("enq_timestamp",
3608+
v_bit
3609+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3610+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3611+
("enq_qdepth",
3612+
v_bit
3613+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3614+
F; F],19));
3615+
("deq_timedelta",
3616+
v_bit
3617+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3618+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3619+
("deq_qdepth",
3620+
v_bit
3621+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3622+
F; F],19));
3623+
("ingress_global_timestamp",
3624+
v_bit
3625+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3626+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3627+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3628+
("egress_global_timestamp",
3629+
v_bit
3630+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3631+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3632+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3633+
("mcast_grp",
3634+
v_bit
3635+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3636+
("egress_rid",
3637+
v_bit
3638+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3639+
("checksum_error",v_bit ([F],1));
3640+
("parser_error",
3641+
v_bit
3642+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3643+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3644+
("priority",v_bit ([F; F; F],3))]
3645+
("ingress_port",v_bit (fixwidth 9 (n2v p),9))));
3646+
("parsedHdr",tau1_uninit_v); ("hdr",tau1_uninit_v);
3647+
("meta",tau2_uninit_v); ("checksum_error",v_bit ([F],1))]’,
3648+
‘aenv15’] >>
3649+
gs[] >>
3650+
CONJ_TAC >- (
3651+
cheat
3652+
) >>
3653+
(* TODO: The below should work... :( *)
3654+
(*
3655+
val term_assum = “transform_v_map dict
3656+
(AUPDATE_LIST aenv15
3657+
[("b",v_ext_ref 0); ("b_temp",v_ext_ref 1);
3658+
("standard_metadata",
3659+
v_struct
3660+
(AUPDATE
3661+
[("ingress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3662+
("egress_spec",v_bit ([F; F; F; F; F; F; F; F; F],9));
3663+
("egress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3664+
("instance_type",
3665+
v_bit
3666+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3667+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3668+
("packet_length",
3669+
v_bit
3670+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3671+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3672+
("enq_timestamp",
3673+
v_bit
3674+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3675+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3676+
("enq_qdepth",
3677+
v_bit
3678+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3679+
F; F],19));
3680+
("deq_timedelta",
3681+
v_bit
3682+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3683+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3684+
("deq_qdepth",
3685+
v_bit
3686+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3687+
F; F],19));
3688+
("ingress_global_timestamp",
3689+
v_bit
3690+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3691+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3692+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3693+
("egress_global_timestamp",
3694+
v_bit
3695+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3696+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3697+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3698+
("mcast_grp",
3699+
v_bit
3700+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3701+
("egress_rid",
3702+
v_bit
3703+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3704+
("checksum_error",v_bit ([F],1));
3705+
("parser_error",
3706+
v_bit
3707+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3708+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3709+
("priority",v_bit ([F; F; F],3))]
3710+
("ingress_port",v_bit (fixwidth 9 (n2v p),9))));
3711+
("parsedHdr",tau1_uninit_v); ("hdr",tau1_uninit_v);
3712+
("meta",tau2_uninit_v); ("checksum_error",v_bit ([F],1))]) =
3713+
SOME s'25”;
3714+
3715+
val term_goal = “transform_v_map dict
3716+
(AUPDATE_LIST aenv15
3717+
[("b",v_ext_ref 0); ("b_temp",v_ext_ref 1);
3718+
("standard_metadata",
3719+
v_struct
3720+
(AUPDATE
3721+
[("ingress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3722+
("egress_spec",v_bit ([F; F; F; F; F; F; F; F; F],9));
3723+
("egress_port",v_bit ([F; F; F; F; F; F; F; F; F],9));
3724+
("instance_type",
3725+
v_bit
3726+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3727+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3728+
("packet_length",
3729+
v_bit
3730+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3731+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3732+
("enq_timestamp",
3733+
v_bit
3734+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3735+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3736+
("enq_qdepth",
3737+
v_bit
3738+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3739+
F; F],19));
3740+
("deq_timedelta",
3741+
v_bit
3742+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3743+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3744+
("deq_qdepth",
3745+
v_bit
3746+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3747+
F; F],19));
3748+
("ingress_global_timestamp",
3749+
v_bit
3750+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3751+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3752+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3753+
("egress_global_timestamp",
3754+
v_bit
3755+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3756+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3757+
F; F; F; F; F; F; F; F; F; F; F; F; F; F],48));
3758+
("mcast_grp",
3759+
v_bit
3760+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3761+
("egress_rid",
3762+
v_bit
3763+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],16));
3764+
("checksum_error",v_bit ([F],1));
3765+
("parser_error",
3766+
v_bit
3767+
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
3768+
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],32));
3769+
("priority",v_bit ([F; F; F],3))]
3770+
("ingress_port",v_bit (fixwidth 9 (n2v p),9))));
3771+
("parsedHdr",tau1_uninit_v); ("hdr",tau1_uninit_v);
3772+
("meta",tau2_uninit_v); ("checksum_error",v_bit ([F],1))]) =
3773+
SOME s'25”;
3774+
3775+
term_eq term_assum term_goal;
3776+
*)
3777+
qpat_x_assum ‘transform_v_map dict _ = SOME s'25’ (fn thm => REWRITE_TAC [GSYM thm]) >>
3778+
gs[] >>
3779+
cheat
3780+
QED
3781+
3782+
(* TODO: Note this is specific to V1Model *)
35123783
Theorem arch_exec'_completeness:
3513-
!dict ab_list pblock_map ffblock_map input_f output_f copyin_pbl copyout_pbl apply_table_f ext_map func_map ab_list' pblock_map' ffblock_map' input_f' output_f' copyin_pbl' copyout_pbl' apply_table_f' ext_map' func_map' ctrl aenv1 aenv'1 g_scope_list1 g_scope_list'1 arch_frame_list1 arch_frame_list'1 status1 status'1 s2 s'2.
3784+
!dict ab_list pblock_map ffblock_map tau1_uninit_v tau2_uninit_v output_f copyin_pbl copyout_pbl apply_table_f ext_map func_map ab_list' pblock_map' ffblock_map' tau1_uninit_v' tau2_uninit_v' output_f' copyin_pbl' copyout_pbl' apply_table_f' ext_map' func_map' ctrl aenv1 aenv'1 g_scope_list1 g_scope_list'1 arch_frame_list1 arch_frame_list'1 status1 status'1 s2 s'2.
35143785
dict_bij dict ==>
3515-
transform_actx dict (ab_list,pblock_map,ffblock_map,input_f,output_f,copyin_pbl,
3786+
transform_actx dict (ab_list,pblock_map,ffblock_map,v1model_input_f (tau1_uninit_v,tau2_uninit_v),output_f,copyin_pbl,
35163787
copyout_pbl,apply_table_f,ext_map,func_map) = SOME (ab_list',pblock_map',ext_map',func_map') ==>
35173788
(* TODO: Need to state and assume completeness of the following:
35183789
ffblock_map'
3519-
input_f'
35203790
output_f'
35213791
copyin_pbl'
35223792
copyout_pbl'
35233793
apply_table_f'
35243794
*)
3795+
transform_v dict tau1_uninit_v = SOME tau1_uninit_v' ==>
3796+
transform_v dict tau2_uninit_v = SOME tau2_uninit_v' ==>
35253797
transform_aenv dict aenv1 ctrl = SOME aenv'1 ==>
35263798
transform_scope_list dict g_scope_list1 = SOME g_scope_list'1 ==>
35273799
transform_arch_frame_list dict arch_frame_list1 = SOME arch_frame_list'1 ==>
35283800
transform_status dict status1 = SOME status'1 ==>
35293801

3530-
arch_exec (ab_list,pblock_map,ffblock_map,input_f,output_f,
3802+
arch_exec (ab_list,pblock_map,ffblock_map,v1model_input_f (tau1_uninit_v,tau2_uninit_v),output_f,
35313803
copyin_pbl,copyout_pbl,apply_table_f,ext_map,func_map) (aenv1, g_scope_list1, arch_frame_list1, status1) = SOME s2 ==>
35323804
transform_astate dict s2 ctrl = SOME s'2 ==>
3533-
arch_exec' (ab_list',pblock_map',ffblock_map',input_f',output_f',
3805+
arch_exec' (ab_list',pblock_map',ffblock_map',v1model_input_f' (tau1_uninit_v',tau2_uninit_v'),output_f',
35343806
copyin_pbl',copyout_pbl',apply_table_f',ext_map',func_map') (aenv'1, g_scope_list'1, arch_frame_list'1, status'1) = SOME s'2
35353807
Proof
35363808
rpt strip_tac >>
@@ -3555,12 +3827,13 @@ Cases_on ‘status1’ >> (
35553827
) >>
35563828
gs[] >>
35573829
PairCases_on ‘s'2’ >>
3558-
qexists_tac ‘(s'21,(s'23,s'24,s'25,s'26))’ >>
3830+
(* Here, we supply the transformed in_out_list and scope *)
3831+
qexists_tac ‘(s'21, (s'23,s'24,s'25,s'26))’ >>
35593832
CONJ_TAC >- (
35603833
PairCases_on ‘scope'’ >>
35613834
gvs[transform_astate_def, transform_aenv_def, transform_actx_def, transform_ascope_def] >>
35623835
(* TODO: Some stuff still missing here for stating input lemma... *)
3563-
(* TODO: Input functions have to be specialised in the theorem *)
3836+
35643837
cheat
35653838
) >>
35663839
qexistsl_tac [‘s'21’, ‘(s'23,s'24,s'25,s'26)’] >>

‎hol/cake_sem/p4_cake_exec_semProgScript.sml‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,6 @@ val _ = translate unop_exec'_def;
180180
val _ = translate e_exec_unop'_def;
181181

182182
(* Binops *)
183-
184183
val _ = translate bitv_ls_def;
185184
val _ = translate bitv_hs_def;
186185
val _ = translate bitv_lo_def;
@@ -189,8 +188,8 @@ val _ = translate rich_listTheory.AND_EL_DEF;
189188
val _ = translate bit_eq_def;
190189
val _ = translate bitv_eq_def;
191190
val _ = translate bitv_neq_def;
192-
val _ = translate get_bitv_binpred'_def;
193-
val _ = translate bitv_binpred'_def;
191+
val _ = translate get_bitv_binpred_def;
192+
val _ = translate bitv_binpred_def;
194193

195194
val _ = translate is_short_circuitable_def;
196195
val _ = translate e_exec_short_circuit'_def;
@@ -219,8 +218,8 @@ val _ = translate bitv_lsr_bv_def;
219218

220219
val _ = translate p4Theory.binop2num_thm;
221220
val _ = translate p4Theory.binop_CASE;
222-
val _ = translate get_bitv_binop'_def;
223-
val _ = translate bitv_binop'_def;
221+
val _ = translate get_bitv_binop_def;
222+
val _ = translate bitv_binop_def;
224223

225224
(* TODO: Not needed? At least not for binops?
226225
val _ = translate (EVAL “w2v (w:word64)” |> SIMP_RULE (srw_ss()) [word_bit_test,word_bit_def,word_bit]);

0 commit comments

Comments
 (0)