@@ -59,142 +59,129 @@ open apply_trans_to_IOLib;
5959
6060 fun sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
6161
62- let
62+ let
6363
6464
6565
66- (* **********************)
67- (* STAGE 1 *)
68- (* **********************)
69-
70- (* convert arith policy to var policy*)
71- val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
72- val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
73-
74-
75- (* first establish distinction of domain and range of me*)
76- val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
77- val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
78-
79- val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
80-
81-
82- (* Theorem of correctness for conversion from arith policy to var policy *)
83- val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
84- (ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
85-
86-
87- (* **********************)
88- (* STAGE 2 *)
89- (* **********************)
90-
91-
92-
93- val (final_policy_bdd, tbl, final_table_bdd) =
94- apply_trans_to_IOLib.sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order);
95-
66+ (* **********************)
67+ (* STAGE 1 *)
68+ (* **********************)
9669
70+ (* convert arith policy to var policy*)
71+ val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
72+ val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
9773
98- val get_i_policy = bdd_utilsLib.pairBDDs (final_policy_bdd, final_table_bdd);
9974
75+ (* first establish distinction of domain and range of me*)
76+ val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
77+ val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
10078
79+ val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
10180
10281
103- val eval_policy_full_opt = mk_thm ( [], “mk_BDDPred_opt policy_structure (0 ,[],[(0 , non_termn (NONE , ^var_policy))]) [] ^policy_order 1 = SOME ^final_policy_bdd”);
82+ (* Theorem of correctness for conversion from arith policy to var policy *)
83+ val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
84+ (ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
10485
105- val eval_table_full_opt_auto = mk_thm ( [], “mk_BDDPred_opt table_structure (0 ,[],[(0 , non_termn (NONE , ^tbl))]) [] ^policy_order 1 = SOME ^final_table_bdd ”);
10686
87+ (* **********************)
88+ (* STAGE 2 *)
89+ (* **********************)
10790
10891
109- val var_eq_thm_extract = REWRITE_CONV [correct_var_policy_var_tables_exec_def, eval_policy_full_opt , eval_table_full_opt_auto] “correct_var_policy_var_tables_exec ^var_policy ^tbl ^policy_order ^get_i_policy”;
11092
111- val var_eq_thm_extract_red = computeLib.RESTR_EVAL_RULE [“correct_var_policy_var_tables_exec”, “sem_tables”,“sem_policy”, “mv_dom_vars”] var_eq_thm_extract;
93+ val (final_policy_bdd, tbl, final_table_bdd) =
94+ apply_trans_to_IOLib.sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order);
11295
113- val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] var_eq_thm_extract_red;
11496
11597
98+ val get_i_policy = bdd_utilsLib.pairBDDs (final_policy_bdd, final_table_bdd);
11699
117100
118101
119- (* **********************)
120- (* STAGE 3 *)
121- (* **********************)
122102
103+ val eval_policy_full_opt = mk_thm ( [], “mk_BDDPred_opt policy_structure (0 ,[],[(0 , non_termn (NONE , ^var_policy))]) [] ^policy_order 1 = SOME ^final_policy_bdd”);
104+ val eval_table_full_opt_auto = mk_thm ( [], “mk_BDDPred_opt table_structure (0 ,[],[(0 , non_termn (NONE , ^tbl))]) [] ^policy_order 1 = SOME ^final_table_bdd ”);
123105
124106
125- (* covert var table to interval table *)
126- val only_var_table = fst (dest_pair tbl);
127- val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
128- val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
129107
108+ val var_eq_thm_extract = REWRITE_CONV [correct_var_policy_var_tables_exec_def, eval_policy_full_opt , eval_table_full_opt_auto] “correct_var_policy_var_tables_exec ^var_policy ^tbl ^policy_order ^get_i_policy”;
109+ val var_eq_thm_extract_red = computeLib.RESTR_EVAL_RULE [“correct_var_policy_var_tables_exec”, “sem_tables”,“sem_policy”, “mv_dom_vars”] var_eq_thm_extract;
110+ val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] var_eq_thm_extract_red;
130111
131- (* Theorem of correctness for conversion from var table to inteval table *)
132- val var_table_sinterval_tbl_thm =
133- REWRITE_RULE [convert_to_interval] (ISPECL[only_var_table, only_interval_table1, “0 :num”, policy_me, test_pd_type ] correct_tables_from_var_to_sinterval_thm);
134112
113+ (* **********************)
114+ (* STAGE 3 *)
115+ (* **********************)
135116
117+ (* covert var table to interval table *)
118+ val only_var_table = fst (dest_pair tbl);
119+ val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
120+ val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
136121
137122
123+ (* Theorem of correctness for conversion from var table to inteval table *)
124+ val var_table_sinterval_tbl_thm =
125+ REWRITE_RULE [convert_to_interval] (ISPECL[only_var_table, only_interval_table1, “0 :num”, policy_me, test_pd_type ] correct_tables_from_var_to_sinterval_thm);
138126
139127
140- (* **********************)
141- (* FINAL PROOF *)
142- (* **********************)
143128
144- val start_cpu_final = Timer.startCPUTimer ();
145- val start_real_final = Timer.startRealTimer ();
146129
147130
148131
149- (* to glue the theorems we need to take care of the conditions/ assumptions *)
132+ (* **********************)
133+ (* FINAL PROOF *)
134+ (* **********************)
150135
151- (* condition1 *)
152- val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
153- val cond1_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct] (ISPECL[policy_me, test_pd_type ] lval_in_me_distinct_imp_cond1);
136+ val start_cpu_final = Timer.startCPUTimer ();
137+ val start_real_final = Timer.startRealTimer ();
154138
155139
156- (* condition2 *)
157- val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
158- val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
159140
160- val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
161- in_order_then_in_me_thm, ops_in_me_length_format_thm]
162- (ISPECL[policy_me, test_pd_type, policy_order ]
163- wf_format_imp_cond2);
141+ (* to glue the theorems we need to take care of the conditions/ assumptions *)
164142
165- (* condition3 *)
166- val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
167- in_order_then_in_me_thm, ops_in_me_length_format_thm]
168- (ISPECL[policy_me, test_pd_type]
169- wf_format_imp_cond3);
143+ (* condition1 *)
144+ val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
145+ val cond1_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct] (ISPECL[policy_me, test_pd_type ] lval_in_me_distinct_imp_cond1);
170146
171147
172- val final_thm = prove(
173- “! packet_input .
174- wf_packet ^test_pd_type packet_input ⇒
175- sem_arith_policy ^arith_policy packet_input =
176- sem_sinterval_tables (^only_interval_table1,0 ) packet_input”
177- ,
148+ (* condition2 *)
149+ val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
150+ val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
178151
179- rpt strip_tac >>
152+ val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
153+ in_order_then_in_me_thm, ops_in_me_length_format_thm]
154+ (ISPECL[policy_me, test_pd_type, policy_order ]
155+ wf_format_imp_cond2);
180156
181- assume_tac arith_policy_var_policy_thm >>
182- first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
157+ (* condition3 *)
158+ val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
159+ in_order_then_in_me_thm, ops_in_me_length_format_thm]
160+ (ISPECL[policy_me, test_pd_type]
161+ wf_format_imp_cond3);
183162
184- assume_tac var_policy_var_table_thm >>
185- first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
186163
164+ val final_thm = prove(
165+ “! packet_input .
166+ wf_packet ^test_pd_type packet_input ⇒
167+ sem_arith_policy ^arith_policy packet_input =
168+ sem_sinterval_tables (^only_interval_table1,0 ) packet_input”
169+ ,
187170
188- assume_tac var_table_sinterval_tbl_thm >>
189- first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
171+ rpt strip_tac >>
190172
191- fs[cond1_thm, cond2_thm, cond3_thm]
192- );
173+ assume_tac arith_policy_var_policy_thm >>
174+ first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
193175
176+ assume_tac var_policy_var_table_thm >>
177+ first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
194178
195179
180+ assume_tac var_table_sinterval_tbl_thm >>
181+ first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
196182
197-
183+ fs[cond1_thm, cond2_thm, cond3_thm]
184+ );
198185
199186
200187 in
0 commit comments