Skip to content

Commit 2c9f35b

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
added another eval for sptrees, and updated teh test cases
1 parent 2c4bb65 commit 2c9f35b

10 files changed

+346
-27
lines changed

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_1Script.sml‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@ open policy_arith_to_varTheory;
55
open bdd_utilsLib;
66
open apply_trans_to_IOLib;
77
open sptrees_fwd_proofLib;
8+
open bdd_end_to_endTheory;
9+
10+
open sptrees_fwd_proof_evalLib;
811

912
val _ = new_theory "internet_firewall_1";
1013

@@ -81,8 +84,11 @@ val policy_full_order = “[
8184
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"]”;
8285

8386

87+
(*
88+
val final_thm_res =
89+
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
90+
*)
8491

85-
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
86-
92+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
8793

8894
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_2Script.sml‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort
114114
*)
115115

116116
(* hand crafted possible better order *)
117-
117+
(*
118118
val policy_full_order = “[
119119
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
120120
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389"]) ;
@@ -127,10 +127,10 @@ val policy_order = “[
127127
"is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389";
128128
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258";
129129
"is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"]”;
130-
130+
*)
131131

132132
(*best order*)
133-
(*
133+
134134
val policy_order = ``[
135135
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
136136
"is_dstPort_le_53"; "is_dstPort_ge_53";
@@ -152,12 +152,16 @@ val policy_full_order = ``[
152152
("43g",["is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
153153
("w8" ,["is_dstNAT_le_3389";"is_dstNAT_ge_3389"])
154154
]``;
155-
*)
156155

157156

158-
(***********************************************)
159157

158+
(***********************************************)
159+
(*
160160
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
161+
*)
162+
163+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
164+
161165

162166

163167
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_3Script.sml‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort
149149
*)
150150

151151
(* hand crafted possible better order *)
152-
152+
(*
153153
val policy_full_order = “[
154154
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258";"is_srcNAT_le_43265";"is_srcNAT_ge_43265"]);
155155
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321"]);
@@ -162,10 +162,10 @@ val policy_order = “[
162162
"is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321";
163163
"is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321";
164164
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881";]”;
165+
*)
165166

166167

167168

168-
(*
169169
val policy_order = ``[
170170
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
171171
"is_dstPort_le_53"; "is_dstPort_ge_53";
@@ -195,12 +195,16 @@ val policy_full_order = ``[
195195
("hdur",["is_srcNAT_le_43265";"is_srcNAT_ge_43265"]);
196196
("wg" ,["is_dstNAT_le_50321";"is_dstNAT_ge_50321"])
197197
]``;
198-
*)
199198

200199

201-
(***********************************************)
202200

201+
(***********************************************)
202+
(*
203203
val final_thm_res =
204204
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
205+
*)
206+
207+
208+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
205209

206210
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_4Script.sml‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,8 @@ val policy_full_order = “[
172172
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"]”;
173173
*)
174174

175+
176+
(*
175177
val policy_full_order = “[
176178
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389";"is_dstPort_le_50321";"is_dstPort_ge_50321"]);
177179
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321"]);
@@ -185,9 +187,9 @@ val policy_order = “[
185187
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553";
186188
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553";
187189
]”;
190+
*)
188191

189192

190-
(*
191193
val policy_order = ``[
192194
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
193195
"is_dstPort_le_53"; "is_dstPort_ge_53";
@@ -221,12 +223,15 @@ val policy_full_order = ``[
221223
("7eii",["is_srcPort_le_50553";"is_srcPort_ge_50553"]);
222224
("g5" ,["is_srcNAT_le_50553";"is_srcNAT_ge_50553"])
223225
]``;
224-
*)
225226

226227

227-
(***********************************************)
228228

229+
(***********************************************)
230+
(*
229231
val final_thm_res =
230232
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
231-
233+
*)
234+
235+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
236+
232237
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_5Script.sml‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -199,13 +199,13 @@ val policy_full_order = “[
199199
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258";"is_srcNAT_le_43265";"is_srcNAT_ge_43265";"is_srcNAT_le_50553";"is_srcNAT_ge_50553";"is_srcNAT_le_45848";"is_srcNAT_ge_45848"]);
200200
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321";"is_dstNAT_le_443";"is_dstNAT_ge_443"])
201201
]”;
202-
*)
203202
204-
(*
205203
(* Flat policy order (grouped) *)
206204
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_srcPort_le_50002"; "is_srcPort_ge_50002"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321"; "is_dstPort_le_443"; "is_dstPort_ge_443"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_srcNAT_le_45848"; "is_srcNAT_ge_45848"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"; "is_dstNAT_le_443"; "is_dstNAT_ge_443"]”;
207205
*)
208206

207+
208+
(*
209209
val policy_full_order = “[
210210
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321";"is_dstNAT_le_443";"is_dstNAT_ge_443"]);
211211
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389";"is_dstPort_le_50321";"is_dstPort_ge_50321";"is_dstPort_le_443";"is_dstPort_ge_443"]);
@@ -219,9 +219,9 @@ val policy_order = “[
219219
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_srcPort_le_50002"; "is_srcPort_ge_50002";
220220
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_srcNAT_le_45848"; "is_srcNAT_ge_45848";
221221
]”;
222+
*)
222223

223224

224-
(*
225225
val policy_order = ``[
226226
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
227227
"is_dstPort_le_53"; "is_dstPort_ge_53";
@@ -263,14 +263,16 @@ val policy_full_order = ``[
263263
("xxt",["is_srcNAT_le_45848";"is_srcNAT_ge_45848"]);
264264
("dk" ,["is_dstNAT_le_443";"is_dstNAT_ge_443"])
265265
]``;
266-
*)
267266

268267

269-
(***********************************************)
270268

269+
(***********************************************)
271270

271+
(*
272272
val final_thm_res =
273273
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
274-
274+
*)
275+
276+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
275277

276278
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_6Script.sml‎

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -228,6 +228,8 @@ val policy_full_order = “[
228228
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_srcPort_le_50002"; "is_srcPort_ge_50002"; "is_srcPort_le_51465"; "is_srcPort_ge_51465"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321"; "is_dstPort_le_443"; "is_dstPort_ge_443"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_srcNAT_le_45848"; "is_srcNAT_ge_45848"; "is_srcNAT_le_39975"; "is_srcNAT_ge_39975"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"; "is_dstNAT_le_443"; "is_dstNAT_ge_443"]”;
229229
*)
230230

231+
232+
(*
231233
val policy_full_order = “[
232234
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321";"is_dstNAT_le_443";"is_dstNAT_ge_443"]);
233235
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389";"is_dstPort_le_50321";"is_dstPort_ge_50321";"is_dstPort_le_443";"is_dstPort_ge_443"]);
@@ -241,9 +243,9 @@ val policy_order = “[
241243
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_srcPort_le_50002"; "is_srcPort_ge_50002"; "is_srcPort_le_51465"; "is_srcPort_ge_51465";
242244
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_srcNAT_le_45848"; "is_srcNAT_ge_45848"; "is_srcNAT_le_39975"; "is_srcNAT_ge_39975";
243245
]”;
246+
*)
244247

245248

246-
(*
247249
val policy_order = ``[
248250
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
249251
"is_dstPort_le_53"; "is_dstPort_ge_53";
@@ -289,10 +291,15 @@ val policy_full_order = ``[
289291
("fn",["is_srcPort_le_51465";"is_srcPort_ge_51465"]);
290292
("rqv" ,["is_srcNAT_le_39975";"is_srcNAT_ge_39975"])
291293
]``;
292-
*)
294+
295+
293296
(***********************************************)
294297

298+
(*
295299
val final_thm_res =
296300
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
297-
301+
*)
302+
303+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
304+
298305
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_7Script.sml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -317,9 +317,11 @@ val policy_full_order = ``[
317317
("s8w" ,["is_dstNAT_le_47094";"is_dstNAT_ge_47094"])
318318
]``;
319319

320+
(*
320321
val final_thm_res =
321322
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
322-
323+
*)
324+
325+
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
323326

324-
325327
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,7 @@ open apply_trans_to_IOLib;
195195
val _ = time_stage ("FINAL CORRECTNESS PROOF", start_cpu_final, start_real_final)
196196

197197
in
198-
eval_table_full_opt_auto (*final_thm*)
198+
final_thm
199199
end;
200200

201201
end;

‎hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proof_evalLib.sig‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
signature sptrees_fwd_proof_evalLib =
2+
sig
3+
include Abbrev
4+
5+
6+
val eval_sptrees_convert_arith_policy_to_interval_tables : term * term * term * term * term -> thm
7+
val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
8+
9+
end

0 commit comments

Comments
 (0)