Skip to content

Commit a5899f0

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
reverted fed_proof to og status
1 parent 29ee31d commit a5899f0

File tree

1 file changed

+179
-45
lines changed

1 file changed

+179
-45
lines changed

‎hol/policy_to_table/fwd_proofLib.sml‎

Lines changed: 179 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -59,84 +59,218 @@ open bdd_utilsLib;
5959

6060
fun convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
6161

62-
let
62+
let
6363

64-
val start_cpu_total = Timer.startCPUTimer ();
65-
val start_real_total = Timer.startRealTimer ();
64+
val start_cpu_total = Timer.startCPUTimer ();
65+
val start_real_total = Timer.startRealTimer ();
66+
6667

67-
(***********************)
68-
(* STAGE 1 *)
69-
(***********************)
68+
(***********************)
69+
(* STAGE 1 *)
70+
(***********************)
7071

71-
(*convert arith policy to var policy*)
72-
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
73-
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
72+
val start_cpu_stage1 = Timer.startCPUTimer ();
73+
val start_real_stage1 = Timer.startRealTimer ();
7474

7575

76-
(* first establish distinction of domain and range of me*)
77-
val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
78-
val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
76+
(*convert arith policy to var policy*)
77+
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
78+
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
7979

80-
val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
80+
81+
(* first establish distinction of domain and range of me*)
82+
val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
83+
val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
8184

85+
val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
8286

83-
(* Theorem of correctness for conversion from arith policy to var policy *)
84-
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
85-
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
87+
88+
(* Theorem of correctness for conversion from arith policy to var policy *)
89+
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
90+
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
8691

87-
val _ = time_stage ("Stage 1", start_cpu_total, start_real_total)
8892

89-
(***********************)
90-
(* STAGE 2 *)
91-
(***********************)
93+
val _ = time_stage ("Stage 1", start_cpu_stage1, start_real_stage1)
9294

9395

96+
(***********************)
97+
(* STAGE 2 *)
98+
(***********************)
99+
100+
94101
val start_cpu_stage2 = Timer.startCPUTimer ();
95102
val start_real_stage2 = Timer.startRealTimer ();
96103

104+
105+
(* create BDD of var policy *)
106+
val eval_policy_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
107+
val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
108+
109+
val _ = time_stage ("Stage 2 from var policy to BDD", start_cpu_stage2, start_real_stage2);
110+
val start_cpu_stage2_vbdd = Timer.startCPUTimer ();
111+
val start_real_stage2_vbdd = Timer.startRealTimer ();
112+
113+
(* automatically generate a var table from the var policy's BDD via sml*)
114+
val test_groupings = rhs(concl(EVAL policy_full_order));
115+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
116+
117+
118+
val _ = time_stage ("Stage 2 from var BDD to table", start_cpu_stage2_vbdd, start_real_stage2_vbdd);
119+
val start_cpu_stage2_tbl = Timer.startCPUTimer ();
120+
val start_real_stage2_tbl = Timer.startRealTimer ();
121+
122+
(* now create a BDD for the table*)
123+
124+
val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
125+
val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
126+
127+
val _ = time_stage ("Stage 2 from table to table BDD", start_cpu_stage2_tbl, start_real_stage2_tbl);
128+
val start_cpu_stage2_tbdd = Timer.startCPUTimer ();
129+
val start_real_stage2_tbdd = Timer.startRealTimer ();
130+
131+
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
132+
val get_i_policy = bdd_utilsLib.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
133+
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
134+
^eval_table_full_opt_auto_rhs”;
135+
*)
136+
137+
138+
139+
(* Theorem of correctness for conversion from var policy to var table *)
140+
(*)
141+
val policy_thm_init = computeLib.RESTR_EVAL_CONV [“sem_tables”,“sem_policy”, “mv_dom_vars”] “correct_var_policy_var_tables_exec ^var_policy ^gen_var_table_auto ^policy_order ^get_i_policy ”;
142+
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy_thm_init;
143+
*)
144+
97145
(*
98-
val policy_main_hol4_def = Define`
99-
policy_main_hol4 =
100-
case sp_mk_BDD_policy ^var_policy ^policy_order of
101-
NONE => NONE
102-
| SOME (r, sp_edges, sp_labels) =>
103-
SOME (r,
104-
((toSortedAList sp_edges):edges),
105-
((toSortedAList sp_labels): (((string#num list) action_expr) policy, (string#num list) action_expr) labelings))
106-
`;
107146
147+
val isIsomorph_exec_thm = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
148+
^eval_table_full_opt_auto_rhs”;
149+
val assumption1 = EVAL “ALOOKUP ^get_i_policy 0 = SOME 0”;
150+
val assumption2 = EVAL “node_in_BDD 0 ^eval_policy_full_opt_rhs”;
151+
val assumption3 = EVAL “node_in_BDD 0 ^eval_table_full_opt_auto_rhs”;
152+
val assumption4 = EVAL “prop_in_BDD 0 ^eval_policy_full_opt_rhs = SOME ^var_policy”;
153+
val assumption5 = EVAL “prop_in_BDD 0 ^eval_table_full_opt_auto_rhs = SOME ^gen_var_table_auto”;
154+
val assumption6 = EVAL “fv_in_vars_exec table_structure ^gen_var_table_auto ^policy_order”;
155+
val assumption7 = EVAL “fv_in_vars_exec policy_structure ^var_policy ^policy_order”;
156+
val assumption8 = EVAL “ALL_DISTINCT ^var_policy”;
157+
val assumption9 = EVAL “^var_policy ≠ []”;
108158
109-
val eval_policy_full_opt = EVAL “policy_main_hol4”; *)
110159
111-
val eval_policy_full_opt = EVAL “
112-
sp_mk_BDDPred_opt policy_structure (0n,LN,insert 0 (non_termn (NONE, ^var_policy)) LN) [] ^policy_order 1n”;
160+
val var_policy_var_table_thm = prove (“ ∀mv.
161+
mv_dom_vars mv ^policy_order ⇒
162+
sem_policy ^var_policy mv = sem_tables ^gen_var_table_auto mv ”,
163+
assume_tac (INST_TYPE [“:'a” |-> “:(string#num list)”] correct_var_policy_var_tables_exec_thm1) >>
164+
first_x_assum (strip_assume_tac o (SPECL [var_policy, gen_var_table_auto, policy_order, get_i_policy])) >>
165+
166+
fs[correct_var_policy_var_tables_exec_def, eval_policy_full_opt, eval_table_full_opt_auto] >>
167+
fs[assumption1, assumption2, assumption3, assumption4, assumption5, assumption6,
168+
assumption7, assumption8, assumption9, isIsomorph_exec_thm]
169+
);
170+
*)
171+
172+
173+
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 ^gen_var_table_auto ^policy_order ^get_i_policy”;
174+
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;
175+
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] var_eq_thm_extract_red;
176+
177+
178+
179+
val _ = time_stage ("Stage 2 proof", start_cpu_stage2_tbdd, start_real_stage2_tbdd);
180+
181+
val _ = time_stage ("Stage 2 total", start_cpu_stage2, start_real_stage2);
182+
183+
184+
185+
(***********************)
186+
(* STAGE 3 *)
187+
(***********************)
188+
189+
val start_cpu_stage3 = Timer.startCPUTimer ();
190+
val start_real_stage3 = Timer.startRealTimer ();
191+
192+
193+
(* covert var table to interval table *)
194+
val only_var_table = fst (dest_pair gen_var_table_auto);
195+
val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
196+
val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
113197

114198

115-
val eval_policy_full_opt_rhs1 = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
199+
(* Theorem of correctness for conversion from var table to inteval table *)
200+
val var_table_sinterval_tbl_thm =
201+
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);
116202

117-
val _ = time_stage ("Stage 2 from var policy to BDD", start_cpu_stage2, start_real_stage2);
203+
val _ = time_stage ("Stage 3", start_cpu_stage3, start_real_stage3);
118204

119205

120-
val start_cpu_stage2b = Timer.startCPUTimer ();
121-
val start_real_stage2b = Timer.startRealTimer ();
122206

123-
val conv_policy_from_sp_to_bdd =
124-
EVAL ``let (r, sp_edges, sp_labels) = ^eval_policy_full_opt_rhs1
125-
in SOME (r,
126-
(toSortedAList sp_edges),
127-
(toSortedAList sp_labels))``;
128207

208+
(***********************)
209+
(* FINAL PROOF *)
210+
(***********************)
211+
212+
val start_cpu_final = Timer.startCPUTimer ();
213+
val start_real_final = Timer.startRealTimer ();
214+
129215

130-
val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl conv_policy_from_sp_to_bdd));
131216

132-
val _ = time_stage ("Stage toStrted List", start_cpu_stage2b, start_real_stage2b);
217+
(* to glue the theorems we need to take care of the conditions/ assumptions *)
218+
219+
(* condition1 *)
220+
val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
221+
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);
222+
223+
224+
(* condition2 *)
225+
val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
226+
val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
227+
228+
val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
229+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
230+
(ISPECL[policy_me, test_pd_type, policy_order ]
231+
wf_format_imp_cond2);
232+
233+
(* condition3 *)
234+
val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
235+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
236+
(ISPECL[policy_me, test_pd_type]
237+
wf_format_imp_cond3);
238+
239+
240+
val final_thm = prove(
241+
“! packet_input .
242+
wf_packet ^test_pd_type packet_input ⇒
243+
sem_arith_policy ^arith_policy packet_input =
244+
sem_sinterval_tables (^only_interval_table1,0) packet_input”
245+
,
246+
247+
rpt strip_tac >>
248+
249+
assume_tac arith_policy_var_policy_thm >>
250+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
251+
252+
assume_tac var_policy_var_table_thm >>
253+
first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
254+
255+
256+
assume_tac var_table_sinterval_tbl_thm >>
257+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
258+
259+
fs[cond1_thm, cond2_thm, cond3_thm]
260+
);
261+
262+
263+
val _ = time_stage ("Final glue proof", start_cpu_final, start_real_final);
264+
265+
val _ = time_stage ("Total time of everything", start_cpu_total, start_real_total);
266+
133267

134268

135269
in
136-
eval_policy_full_opt
270+
final_thm
137271
end;
138272

139273
end;
140274

141275

142-
276+

0 commit comments

Comments
 (0)