Skip to content

Commit abe4b14

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
edited name of file
1 parent dca0b88 commit abe4b14

File tree

1 file changed

+53
-59
lines changed

1 file changed

+53
-59
lines changed

hol/policy_to_table/bdd_test_casesScript.sml renamed to hol/policy_to_table/bdd_fwd_pipeline_exampleScript.sml

Lines changed: 53 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ open table_bs_propertiesTheory;
4040

4141
val _ = load "bdd_utils";
4242

43-
val _ = new_theory "bdd_test_cases";
43+
val _ = new_theory "bdd_fwd_pipeline_example";
4444

4545
(* a few types abbreviations *)
4646
val _ = type_abbrev("BDD_tbl_type", “:(( (string# num list) var_table_list, (string# num list) action_expr) BDD)”);
@@ -51,17 +51,11 @@ val _ = type_abbrev("struc_tbl_type", “:((( atom_var list # num # (string# num
5151
val _ = type_abbrev("action_rule_type", “:((string# num list) action_expr) rule”);
5252
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
5353

54-
55-
56-
57-
58-
59-
6054

6155

6256
(****************************************************************)
6357
(****************************************************************)
64-
(* POLICY 1 *)
58+
(* forward proof for a policy example *)
6559
(****************************************************************)
6660
(****************************************************************)
6761

@@ -70,7 +64,7 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
7064

7165

7266

73-
val test_pd_type1 = “[("ip", type_record [("priority", type_length 3);
67+
val test_pd_type = “[("ip", type_record [("priority", type_length 3);
7468
("size", type_length 16);
7569
("age", type_length 8);
7670
("type", type_length 4)])]”;
@@ -82,41 +76,41 @@ val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^(BDDUtils.make_b
8276
val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 3 4))”;
8377
val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 8 4))”;
8478

85-
val policy1_me1 = “[("x", ^is_high_priority);
79+
val policy_me = “[("x", ^is_high_priority);
8680
("y", ^is_medium_priority);
8781
("z", ^is_small_packet);
8882
("w", ^is_young_packet);
8983
("q", ^is_control_type);
9084
("r", ^is_data_type)]”;
9185

92-
val policy1_full_order = “[("a",["x";"y"]);
86+
val policy_full_order = “[("a",["x";"y"]);
9387
("b",["z"]);
9488
("c",["w"]);
9589
("d",["q";"r"])]”;
9690

97-
val policy1_order = “["x";"y";"z";"w";"q";"r"]”;
91+
val policy_order = “["x";"y";"z";"w";"q";"r"]”;
9892

9993
(* Rule 1: High priority small control packets - expedited forwarding *)
100-
val arith_policy1_rule1 = “(arith_and (arith_a ^is_high_priority)
94+
val arith_policy_rule1 = “(arith_and (arith_a ^is_high_priority)
10195
(arith_and (arith_a ^is_small_packet) (arith_a ^is_control_type)),
10296
action ("fwd_priority",[1; 255])):((string# num list) action_expr) arith_rule”;
10397

10498
(* Rule 2: High priority data packets *)
105-
val arith_policy1_rule2 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_data_type),
99+
val arith_policy_rule2 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_data_type),
106100
action ("fwd",[1])):((string# num list) action_expr) arith_rule”;
107101

108102
(* Rule 3: Medium priority young packets *)
109-
val arith_policy1_rule3 = “(arith_and (arith_a ^is_medium_priority) (arith_a ^is_young_packet),
103+
val arith_policy_rule3 = “(arith_and (arith_a ^is_medium_priority) (arith_a ^is_young_packet),
110104
action ("fwd",[2])):((string# num list) action_expr) arith_rule”;
111105

112106
(* Rule 7: Default forward rule *)
113-
val arith_policy1_rule7 = “(arith_a a_True,
107+
val arith_policy_rule7 = “(arith_a a_True,
114108
action ("fwd",[5])):((string# num list) action_expr) arith_rule”;
115109

116-
val arith_policy1 = “[^arith_policy1_rule1;
117-
^arith_policy1_rule2;
118-
^arith_policy1_rule3;
119-
^arith_policy1_rule7]:((string# num list) action_expr) arith_policy”;
110+
val arith_policy = “[^arith_policy_rule1;
111+
^arith_policy_rule2;
112+
^arith_policy_rule3;
113+
^arith_policy_rule7]:((string# num list) action_expr) arith_policy”;
120114

121115

122116
(********************************)
@@ -128,54 +122,54 @@ val arith_policy1 = “[^arith_policy1_rule1;
128122
(***********************)
129123

130124
(*convert arith policy to var policy*)
131-
val arith_policy1_eval = EVAL “convert_arith_to_var_policy ^arith_policy1 ^policy1_me1”;
132-
val var_policy1 = optionSyntax.dest_some (rhs (concl arith_policy1_eval));
125+
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
126+
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
133127

134128

135129
(* first establish distinction of domain and range of me*)
136-
val policy1_me1_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy1_me1)”;
137-
val policy1_me1_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy1_me1)”;
130+
val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
131+
val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
138132

139-
val all_distinct_conj = CONJ policy1_me1_fst_distinct policy1_me1_snd_distinct;
133+
val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
140134

141135

142136
(* Theorem of correctness for conversion from arith policy to var policy *)
143-
val arith_policy1_var_policy1_thm = REWRITE_RULE[all_distinct_conj, arith_policy1_eval]
144-
(ISPECL[arith_policy1, var_policy1, policy1_me1] policy_airth_to_var_sem_conversion_correct);
137+
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
138+
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
145139

146140

147141
(***********************)
148142
(* STAGE 2 *)
149143
(***********************)
150144

151145
(* create BDD of var policy *)
152-
val eval_policy1_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy1))]) [] ^policy1_order 1”;
153-
val eval_policy1_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy1_full_opt));
146+
val eval_policy_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
147+
val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
154148

155149

156150
(* automatically generate a var table from the var policy's BDD via sml*)
157-
val test_groupings1 = rhs(concl(EVAL policy1_full_order));
158-
val test_action_table1_auto = BDDUtils.bdd_to_tables_iterative eval_policy1_full_opt_rhs test_groupings1;
151+
val test_groupings = rhs(concl(EVAL policy_full_order));
152+
val gen_var_table_auto = BDDUtils.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
159153

160154

161155
(* now create a BDD for the table*)
162-
val eval_table1_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^test_action_table1_auto))]) [] ^policy1_order 1”;
163-
val eval_table1_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table1_full_opt_auto));
156+
val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
157+
val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
164158

165159

166160
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
167-
val get_i_policy1 = BDDUtils.pairBDDs (eval_policy1_full_opt_rhs, eval_table1_full_opt_auto_rhs);
168-
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy1 ^eval_policy1_full_opt_rhs
169-
^eval_table1_full_opt_auto_rhs”;
161+
val get_i_policy = BDDUtils.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
162+
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
163+
^eval_table_full_opt_auto_rhs”;
170164
*)
171165

172166

173167
(* Theorem of correctness for conversion from var policy to var table *)
174168

175169
(* we can do it in two methods, this is: *)
176170
(* method 1 *)
177-
val policy1_thm_init = computeLib.RESTR_EVAL_CONV [“sem_tables”,“sem_policy”, “mv_dom_vars”] “correct_var_policy_var_tables_exec ^var_policy1 ^test_action_table1_auto ^policy1_order ^get_i_policy1 ”;
178-
val policy1_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy1_thm_init;
171+
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 ”;
172+
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy_thm_init;
179173

180174

181175

@@ -184,58 +178,58 @@ val policy1_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] po
184178
(***********************)
185179

186180
(* covert var table to interval table *)
187-
val only_var_table1 = fst (dest_pair test_action_table1_auto);
188-
val convert_to_interval1 = EVAL “convert_var_to_sinterval_tables ^only_var_table1 ^policy1_me1 ^test_pd_type1”;
189-
val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval1));
181+
val only_var_table = fst (dest_pair gen_var_table_auto);
182+
val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
183+
val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
190184

191185

192186
(* Theorem of correctness for conversion from var table to inteval table *)
193-
val final_table1_thm =
194-
REWRITE_RULE [convert_to_interval1] (ISPECL[only_var_table1, only_interval_table1, “0:num”, policy1_me1, test_pd_type1 ] correct_tables_from_var_to_sinterval_thm);
187+
val var_table_sinterval_tbl_thm =
188+
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);
195189

196190

197191

198192
(* to glue the theorems we need to take care of the conditions/ assumptions *)
199193

200194
(* condition1 *)
201-
val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type1 ^policy1_me1”;
202-
val cond1_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy1_me1_fst_distinct] (ISPECL[policy1_me1, test_pd_type1 ] lval_in_me_distinct_imp_cond1);
195+
val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
196+
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);
203197

204198

205199
(* condition2 *)
206-
val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy1_order ^policy1_me1”;
207-
val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type1 ^policy1_me1”;
200+
val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
201+
val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
208202

209-
val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy1_me1_fst_distinct,
203+
val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
210204
in_order_then_in_me_thm, ops_in_me_length_format_thm]
211-
(ISPECL[policy1_me1, test_pd_type1, policy1_order ]
205+
(ISPECL[policy_me, test_pd_type, policy_order ]
212206
wf_format_imp_cond2);
213207

214208
(* condition3 *)
215-
val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy1_me1_fst_distinct,
209+
val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
216210
in_order_then_in_me_thm, ops_in_me_length_format_thm]
217-
(ISPECL[policy1_me1, test_pd_type1]
211+
(ISPECL[policy_me, test_pd_type]
218212
wf_format_imp_cond3);
219213

220214

221215
val final_thm = prove(
222216
“! packet_input .
223-
wf_packet ^test_pd_type1 packet_input ⇒
224-
sem_arith_policy ^arith_policy1 packet_input =
217+
wf_packet ^test_pd_type packet_input ⇒
218+
sem_arith_policy ^arith_policy packet_input =
225219
sem_sinterval_tables (^only_interval_table1,0) packet_input”
226220
,
227221

228222
rpt strip_tac >>
229223

230-
assume_tac arith_policy1_var_policy1_thm >>
231-
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy1_me1 packet_input)’])) >>
224+
assume_tac arith_policy_var_policy_thm >>
225+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
232226

233-
assume_tac policy1_thm >>
234-
first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy1_me1 packet_input)’])) >>
227+
assume_tac var_policy_var_table_thm >>
228+
first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
235229

236230

237-
assume_tac final_table1_thm >>
238-
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy1_me1 packet_input)’])) >>
231+
assume_tac var_table_sinterval_tbl_thm >>
232+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
239233

240234
fs[cond1_thm, cond2_thm, cond3_thm]
241235
);

0 commit comments

Comments
 (0)