Skip to content

Commit 29ee31d

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
updated test cases
1 parent 2c9f35b commit 29ee31d

23 files changed

+911
-232
lines changed

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

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,8 @@ val policy_me = “[
330330
("is_srcNAT_le_16215", ^is_srcNAT_le_16215);
331331
("is_srcNAT_ge_16215", ^is_srcNAT_ge_16215);
332332
]”;
333+
(*
334+
333335
334336
(* Grouped policy ordering *)
335337
val policy_full_order = “[
@@ -342,6 +344,79 @@ val policy_full_order = “[
342344
(* Flat policy order (grouped) *)
343345
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_srcPort_le_60513"; "is_srcPort_ge_60513"; "is_srcPort_le_50049"; "is_srcPort_ge_50049"; "is_srcPort_le_52244"; "is_srcPort_ge_52244"; "is_srcPort_le_50627"; "is_srcPort_ge_50627"; "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_dstPort_le_47094"; "is_dstPort_ge_47094"; "is_dstPort_le_58774"; "is_dstPort_ge_58774"; "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_srcNAT_le_45469"; "is_srcNAT_ge_45469"; "is_srcNAT_le_21285"; "is_srcNAT_ge_21285"; "is_srcNAT_le_2211"; "is_srcNAT_ge_2211"; "is_srcNAT_le_16215"; "is_srcNAT_ge_16215"; "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"; "is_dstNAT_le_47094"; "is_dstNAT_ge_47094"; "is_dstNAT_le_58774"; "is_dstNAT_ge_58774"]”;
344346
(***********************************************)
347+
*)
348+
349+
350+
351+
val policy_order = ``[
352+
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
353+
"is_dstPort_le_53"; "is_dstPort_ge_53";
354+
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587";
355+
"is_dstNAT_le_53"; "is_dstNAT_ge_53";
356+
"is_srcPort_le_56258"; "is_srcPort_ge_56258";
357+
"is_dstPort_le_3389"; "is_dstPort_ge_3389";
358+
"is_srcNAT_le_56258"; "is_srcNAT_ge_56258";
359+
"is_dstNAT_le_3389"; "is_dstNAT_ge_3389";
360+
"is_srcPort_le_6881"; "is_srcPort_ge_6881";
361+
"is_dstPort_le_50321"; "is_dstPort_ge_50321";
362+
"is_srcNAT_le_43265"; "is_srcNAT_ge_43265";
363+
"is_dstNAT_le_50321"; "is_dstNAT_ge_50321";
364+
"is_srcPort_le_50553"; "is_srcPort_ge_50553";
365+
"is_srcNAT_le_50553"; "is_srcNAT_ge_50553";
366+
"is_srcPort_le_50002"; "is_srcPort_ge_50002";
367+
"is_dstPort_le_443"; "is_dstPort_ge_443";
368+
"is_srcNAT_le_45848"; "is_srcNAT_ge_45848";
369+
"is_dstNAT_le_443"; "is_dstNAT_ge_443";
370+
"is_srcPort_le_51465"; "is_srcPort_ge_51465";
371+
"is_srcNAT_le_39975"; "is_srcNAT_ge_39975";
372+
"is_srcPort_le_60513"; "is_srcPort_ge_60513";
373+
"is_dstPort_le_47094"; "is_dstPort_ge_47094";
374+
"is_srcNAT_le_45469"; "is_srcNAT_ge_45469";
375+
"is_dstNAT_le_47094"; "is_dstNAT_ge_47094";
376+
"is_srcPort_le_50049"; "is_srcPort_ge_50049";
377+
"is_srcNAT_le_21285"; "is_srcNAT_ge_21285";
378+
"is_srcPort_le_52244"; "is_srcPort_ge_52244";
379+
"is_dstPort_le_58774"; "is_dstPort_ge_58774";
380+
"is_srcNAT_le_2211"; "is_srcNAT_ge_2211";
381+
"is_dstNAT_le_58774"; "is_dstNAT_ge_58774";
382+
"is_srcPort_le_50627"; "is_srcPort_ge_50627";
383+
"is_srcNAT_le_16215"; "is_srcNAT_ge_16215"
384+
]``;
385+
386+
val policy_full_order = ``[
387+
("igfm",["is_srcPort_le_57222";"is_srcPort_ge_57222"]);
388+
("f5x" ,["is_dstPort_le_53";"is_dstPort_ge_53"]);
389+
("s9e",["is_srcNAT_le_54587";"is_srcNAT_ge_54587"]);
390+
("thxd" ,["is_dstNAT_le_53";"is_dstNAT_ge_53"]);
391+
("gm",["is_srcPort_le_56258";"is_srcPort_ge_56258"]);
392+
("9g5" ,["is_dstPort_le_3389";"is_dstPort_ge_3389"]);
393+
("1qf",["is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
394+
("s2qx" ,["is_dstNAT_le_3389";"is_dstNAT_ge_3389"]);
395+
("qou",["is_srcPort_le_6881";"is_srcPort_ge_6881"]);
396+
("pa" ,["is_dstPort_le_50321";"is_dstPort_ge_50321"]);
397+
("wi",["is_srcNAT_le_43265";"is_srcNAT_ge_43265"]);
398+
("4acn" ,["is_dstNAT_le_50321";"is_dstNAT_ge_50321"]);
399+
("ebq",["is_srcPort_le_50553";"is_srcPort_ge_50553"]);
400+
("5g" ,["is_srcNAT_le_50553";"is_srcNAT_ge_50553"]);
401+
("ti",["is_srcPort_le_50002";"is_srcPort_ge_50002"]);
402+
("lc" ,["is_dstPort_le_443";"is_dstPort_ge_443"]);
403+
("fckc",["is_srcNAT_le_45848";"is_srcNAT_ge_45848"]);
404+
("nms7" ,["is_dstNAT_le_443";"is_dstNAT_ge_443"]);
405+
("5nby",["is_srcPort_le_51465";"is_srcPort_ge_51465"]);
406+
("0w" ,["is_srcNAT_le_39975";"is_srcNAT_ge_39975"]);
407+
("kjz",["is_srcPort_le_60513";"is_srcPort_ge_60513"]);
408+
("2fo" ,["is_dstPort_le_47094";"is_dstPort_ge_47094"]);
409+
("f0",["is_srcNAT_le_45469";"is_srcNAT_ge_45469"]);
410+
("pq" ,["is_dstNAT_le_47094";"is_dstNAT_ge_47094"]);
411+
("j06",["is_srcPort_le_50049";"is_srcPort_ge_50049"]);
412+
("w6" ,["is_srcNAT_le_21285";"is_srcNAT_ge_21285"]);
413+
("hjl",["is_srcPort_le_52244";"is_srcPort_ge_52244"]);
414+
("8cb0" ,["is_dstPort_le_58774";"is_dstPort_ge_58774"]);
415+
("4se8",["is_srcNAT_le_2211";"is_srcNAT_ge_2211"]);
416+
("pch" ,["is_dstNAT_le_58774";"is_dstNAT_ge_58774"]);
417+
("8ug",["is_srcPort_le_50627";"is_srcPort_ge_50627"]);
418+
("ut3r" ,["is_srcNAT_le_16215";"is_srcNAT_ge_16215"])
419+
]``;
345420

346421

347422
(*

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

Lines changed: 82 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,8 @@ val policy_me = “[
365365
("is_dstNAT_ge_80", ^is_dstNAT_ge_80);
366366
]”;
367367

368+
369+
(*
368370
(* Grouped policy ordering *)
369371
val policy_full_order = “[
370372
("srcPortGrp",["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_srcPort_le_60513";"is_srcPort_ge_60513";"is_srcPort_le_50049";"is_srcPort_ge_50049";"is_srcPort_le_52244";"is_srcPort_ge_52244";"is_srcPort_le_50627";"is_srcPort_ge_50627";"is_srcPort_le_43676";"is_srcPort_ge_43676"]);
@@ -376,7 +378,86 @@ val policy_full_order = “[
376378
(* Flat policy order (grouped) *)
377379
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_srcPort_le_60513"; "is_srcPort_ge_60513"; "is_srcPort_le_50049"; "is_srcPort_ge_50049"; "is_srcPort_le_52244"; "is_srcPort_ge_52244"; "is_srcPort_le_50627"; "is_srcPort_ge_50627"; "is_srcPort_le_43676"; "is_srcPort_ge_43676"; "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_dstPort_le_47094"; "is_dstPort_ge_47094"; "is_dstPort_le_58774"; "is_dstPort_ge_58774"; "is_dstPort_le_80"; "is_dstPort_ge_80"; "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_srcNAT_le_45469"; "is_srcNAT_ge_45469"; "is_srcNAT_le_21285"; "is_srcNAT_ge_21285"; "is_srcNAT_le_2211"; "is_srcNAT_ge_2211"; "is_srcNAT_le_16215"; "is_srcNAT_ge_16215"; "is_srcNAT_le_45378"; "is_srcNAT_ge_45378"; "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"; "is_dstNAT_le_47094"; "is_dstNAT_ge_47094"; "is_dstNAT_le_58774"; "is_dstNAT_ge_58774"; "is_dstNAT_le_80"; "is_dstNAT_ge_80"]”;
378380
(************************************************)
379-
381+
*)
382+
383+
384+
val policy_order = ``[
385+
"is_srcPort_le_57222"; "is_srcPort_ge_57222";
386+
"is_dstPort_le_53"; "is_dstPort_ge_53";
387+
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587";
388+
"is_dstNAT_le_53"; "is_dstNAT_ge_53";
389+
"is_srcPort_le_56258"; "is_srcPort_ge_56258";
390+
"is_dstPort_le_3389"; "is_dstPort_ge_3389";
391+
"is_srcNAT_le_56258"; "is_srcNAT_ge_56258";
392+
"is_dstNAT_le_3389"; "is_dstNAT_ge_3389";
393+
"is_srcPort_le_6881"; "is_srcPort_ge_6881";
394+
"is_dstPort_le_50321"; "is_dstPort_ge_50321";
395+
"is_srcNAT_le_43265"; "is_srcNAT_ge_43265";
396+
"is_dstNAT_le_50321"; "is_dstNAT_ge_50321";
397+
"is_srcPort_le_50553"; "is_srcPort_ge_50553";
398+
"is_srcNAT_le_50553"; "is_srcNAT_ge_50553";
399+
"is_srcPort_le_50002"; "is_srcPort_ge_50002";
400+
"is_dstPort_le_443"; "is_dstPort_ge_443";
401+
"is_srcNAT_le_45848"; "is_srcNAT_ge_45848";
402+
"is_dstNAT_le_443"; "is_dstNAT_ge_443";
403+
"is_srcPort_le_51465"; "is_srcPort_ge_51465";
404+
"is_srcNAT_le_39975"; "is_srcNAT_ge_39975";
405+
"is_srcPort_le_60513"; "is_srcPort_ge_60513";
406+
"is_dstPort_le_47094"; "is_dstPort_ge_47094";
407+
"is_srcNAT_le_45469"; "is_srcNAT_ge_45469";
408+
"is_dstNAT_le_47094"; "is_dstNAT_ge_47094";
409+
"is_srcPort_le_50049"; "is_srcPort_ge_50049";
410+
"is_srcNAT_le_21285"; "is_srcNAT_ge_21285";
411+
"is_srcPort_le_52244"; "is_srcPort_ge_52244";
412+
"is_dstPort_le_58774"; "is_dstPort_ge_58774";
413+
"is_srcNAT_le_2211"; "is_srcNAT_ge_2211";
414+
"is_dstNAT_le_58774"; "is_dstNAT_ge_58774";
415+
"is_srcPort_le_50627"; "is_srcPort_ge_50627";
416+
"is_srcNAT_le_16215"; "is_srcNAT_ge_16215";
417+
"is_srcPort_le_43676"; "is_srcPort_ge_43676";
418+
"is_dstPort_le_80"; "is_dstPort_ge_80";
419+
"is_srcNAT_le_45378"; "is_srcNAT_ge_45378";
420+
"is_dstNAT_le_80"; "is_dstNAT_ge_80"
421+
]``;
422+
423+
val policy_full_order = ``[
424+
("c3yn",["is_srcPort_le_57222";"is_srcPort_ge_57222"]);
425+
("g1" ,["is_dstPort_le_53";"is_dstPort_ge_53"]);
426+
("7i",["is_srcNAT_le_54587";"is_srcNAT_ge_54587"]);
427+
("x8hr" ,["is_dstNAT_le_53";"is_dstNAT_ge_53"]);
428+
("41",["is_srcPort_le_56258";"is_srcPort_ge_56258"]);
429+
("ca0k" ,["is_dstPort_le_3389";"is_dstPort_ge_3389"]);
430+
("ckm",["is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
431+
("sj" ,["is_dstNAT_le_3389";"is_dstNAT_ge_3389"]);
432+
("hh",["is_srcPort_le_6881";"is_srcPort_ge_6881"]);
433+
("p9a" ,["is_dstPort_le_50321";"is_dstPort_ge_50321"]);
434+
("xwx",["is_srcNAT_le_43265";"is_srcNAT_ge_43265"]);
435+
("eh" ,["is_dstNAT_le_50321";"is_dstNAT_ge_50321"]);
436+
("2p6",["is_srcPort_le_50553";"is_srcPort_ge_50553"]);
437+
("ty4h" ,["is_srcNAT_le_50553";"is_srcNAT_ge_50553"]);
438+
("5520",["is_srcPort_le_50002";"is_srcPort_ge_50002"]);
439+
("8s9" ,["is_dstPort_le_443";"is_dstPort_ge_443"]);
440+
("zey",["is_srcNAT_le_45848";"is_srcNAT_ge_45848"]);
441+
("gu" ,["is_dstNAT_le_443";"is_dstNAT_ge_443"]);
442+
("n0yq",["is_srcPort_le_51465";"is_srcPort_ge_51465"]);
443+
("pd" ,["is_srcNAT_le_39975";"is_srcNAT_ge_39975"]);
444+
("5mlo",["is_srcPort_le_60513";"is_srcPort_ge_60513"]);
445+
("we" ,["is_dstPort_le_47094";"is_dstPort_ge_47094"]);
446+
("q7v",["is_srcNAT_le_45469";"is_srcNAT_ge_45469"]);
447+
("ny4" ,["is_dstNAT_le_47094";"is_dstNAT_ge_47094"]);
448+
("b85g",["is_srcPort_le_50049";"is_srcPort_ge_50049"]);
449+
("6b" ,["is_srcNAT_le_21285";"is_srcNAT_ge_21285"]);
450+
("lgmh",["is_srcPort_le_52244";"is_srcPort_ge_52244"]);
451+
("rijc" ,["is_dstPort_le_58774";"is_dstPort_ge_58774"]);
452+
("x9",["is_srcNAT_le_2211";"is_srcNAT_ge_2211"]);
453+
("m7w" ,["is_dstNAT_le_58774";"is_dstNAT_ge_58774"]);
454+
("zj",["is_srcPort_le_50627";"is_srcPort_ge_50627"]);
455+
("dkx" ,["is_srcNAT_le_16215";"is_srcNAT_ge_16215"]);
456+
("y1d",["is_srcPort_le_43676";"is_srcPort_ge_43676"]);
457+
("w2" ,["is_dstPort_le_80";"is_dstPort_ge_80"]);
458+
("dt",["is_srcNAT_le_45378";"is_srcNAT_ge_45378"]);
459+
("77nf" ,["is_dstNAT_le_80";"is_dstNAT_ge_80"])
460+
]``;
380461

381462
(*
382463
val final_thm_res =

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

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ open policy_arith_to_varTheory;
44

55
open bdd_utilsLib;
66
open sptrees_fwd_proofLib;
7+
open sptrees_fwd_proof_evalLib;
78

89

910
val _ = new_theory "internet_firewall_2";
@@ -99,22 +100,22 @@ val policy_me = “[
99100
("is_dstNAT_ge_3389", ^is_dstNAT_ge_3389);
100101
]”;
101102

102-
(*
103+
(*
103104
(* Grouped policy ordering *)
104105
val policy_full_order = “[
105106
("srcPortGrp",["is_srcPort_le_57222";"is_srcPort_ge_57222";"is_srcPort_le_56258";"is_srcPort_ge_56258"]);
106107
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389"]);
107108
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
108109
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389"])
109-
]”;
110+
]”; *)
110111

111112
(* Flat policy order (grouped) *)
112113

113114
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"]”;
114-
*)
115+
115116

116117
(* hand crafted possible better order *)
117-
(*
118+
(*
118119
val policy_full_order = “[
119120
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
120121
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389"]) ;
@@ -126,8 +127,8 @@ val policy_order = “[
126127
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258";
127128
"is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389";
128129
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258";
129-
"is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"]”;
130-
*)
130+
"is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"]”; *)
131+
131132

132133
(*best order*)
133134

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ open policy_arith_to_varTheory;
44

55
open bdd_utilsLib;
66
open sptrees_fwd_proofLib;
7+
open sptrees_fwd_proof_evalLib;
78

89

910
val _ = new_theory "internet_firewall_3";
@@ -133,7 +134,7 @@ val policy_me = “[
133134
("is_dstNAT_ge_50321", ^is_dstNAT_ge_50321);
134135
]”;
135136

136-
(*
137+
(*
137138
(* Grouped policy ordering *)
138139
val policy_full_order = “[
139140
("srcPortGrp",["is_srcPort_le_57222";"is_srcPort_ge_57222";"is_srcPort_le_56258";"is_srcPort_ge_56258";"is_srcPort_le_6881";"is_srcPort_ge_6881"]);
@@ -145,11 +146,11 @@ val policy_full_order = “[
145146
146147
(* Flat policy order (grouped) *)
147148
148-
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_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_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"]”;
149-
*)
149+
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_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_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"]”; *)
150+
150151

151152
(* hand crafted possible better order *)
152-
(*
153+
(*
153154
val policy_full_order = “[
154155
("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"]);
155156
("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"]);
@@ -161,8 +162,8 @@ val policy_order = “[
161162
"is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265";
162163
"is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321";
163164
"is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321";
164-
"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-
*)
165+
"is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881";]”; *)
166+
166167

167168

168169

@@ -200,11 +201,10 @@ val policy_full_order = ``[
200201

201202
(***********************************************)
202203
(*
203-
val final_thm_res =
204-
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
205-
*)
204+
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)
205+
*)
206206

207+
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);
207208

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);
209-
209+
210210
val _ = export_theory ();

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ open policy_arith_to_varTheory;
44

55
open bdd_utilsLib;
66
open sptrees_fwd_proofLib;
7+
open sptrees_fwd_proof_evalLib;
78

89

910
val _ = new_theory "internet_firewall_4";
@@ -158,7 +159,7 @@ val policy_me = “[
158159
]”;
159160

160161

161-
(*
162+
(*
162163
(* Grouped policy ordering *)
163164
val policy_full_order = “[
164165
("srcPortGrp",["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"]);
@@ -169,8 +170,8 @@ val policy_full_order = “[
169170
170171
(* Flat policy order (grouped) *)
171172
172-
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"]”;
173-
*)
173+
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"]”; *)
174+
174175

175176

176177
(*

0 commit comments

Comments
 (0)