Skip to content

Commit b7cf2f3

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
a few updates for printing and a shell script to process sequentially
1 parent 526905f commit b7cf2f3

File tree

8 files changed

+470
-171
lines changed

8 files changed

+470
-171
lines changed

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sig‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,6 @@ sig
33
include Abbrev
44

55
val sptrees_gen_bdds_policy_and_table : term * term * term -> (term * term * term)
6+
val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
67

78
end

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml‎

Lines changed: 179 additions & 165 deletions
Large diffs are not rendered by default.

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/build_sequential.sh‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
#!/bin/bash
2+
for file in *Script.sml; do
3+
base=$(basename "$file" Script.sml)
4+
Holmake "${base}Theory.uo"
5+
done

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_dstPort
8282

8383

8484

85-
val _ = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
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)
8686

8787

8888
val _ = export_theory ();

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

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
open bdd_utilsLib;
6+
open sptrees_fwd_proofLib;
7+
8+
9+
val _ = new_theory "internet_firewall_2";
10+
11+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
12+
13+
val test_pd_type = “[("h", type_record [("srcPort", type_length 16);
14+
("dstPort", type_length 16);
15+
("srcNAT", type_length 16);
16+
("dstNAT", type_length 16)])]”;
17+
18+
(************************************************)
19+
20+
(* rule 1 *)
21+
22+
val is_srcPort_le_57222 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
23+
val is_srcPort_ge_57222 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
24+
25+
val is_dstPort_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
26+
val is_dstPort_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
27+
28+
val is_srcNAT_le_54587 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
29+
val is_srcNAT_ge_54587 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
30+
31+
val is_dstNAT_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
32+
val is_dstNAT_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
33+
34+
35+
val arith_policy_rule1 = “((arith_and (arith_a ^is_srcPort_le_57222)
36+
(arith_and (arith_a ^is_srcPort_ge_57222)
37+
(arith_and (arith_a ^is_dstPort_le_53)
38+
(arith_and (arith_a ^is_dstPort_ge_53)
39+
(arith_and (arith_a ^is_srcNAT_le_54587)
40+
(arith_and (arith_a ^is_srcNAT_ge_54587)
41+
(arith_and (arith_a ^is_dstNAT_le_53)
42+
(arith_a ^is_dstNAT_ge_53)))))))) ,
43+
action ("allow",[1])):single_rule”;
44+
45+
(* rule 2 *)
46+
47+
val is_srcPort_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
48+
val is_srcPort_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
49+
50+
val is_dstPort_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
51+
val is_dstPort_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
52+
53+
val is_srcNAT_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
54+
val is_srcNAT_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
55+
56+
val is_dstNAT_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
57+
val is_dstNAT_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
58+
59+
60+
val arith_policy_rule2 = “((arith_and (arith_a ^is_srcPort_le_56258)
61+
(arith_and (arith_a ^is_srcPort_ge_56258)
62+
(arith_and (arith_a ^is_dstPort_le_3389)
63+
(arith_and (arith_a ^is_dstPort_ge_3389)
64+
(arith_and (arith_a ^is_srcNAT_le_56258)
65+
(arith_and (arith_a ^is_srcNAT_ge_56258)
66+
(arith_and (arith_a ^is_dstNAT_le_3389)
67+
(arith_a ^is_dstNAT_ge_3389)))))))) ,
68+
action ("allow",[1])):single_rule”;
69+
70+
(* Default policy rule *)
71+
val arith_policy_rule_default = “(arith_a a_True, action ("drop", [])):single_rule”;
72+
73+
(* Combined arith policy list *)
74+
val arith_policy = “[
75+
^arith_policy_rule1;
76+
^arith_policy_rule2;
77+
^arith_policy_rule_default
78+
]:single_rule list”;
79+
80+
81+
82+
(* Combined policy mapping *)
83+
val policy_me = “[
84+
("is_srcPort_le_57222", ^is_srcPort_le_57222);
85+
("is_srcPort_ge_57222", ^is_srcPort_ge_57222);
86+
("is_dstPort_le_53", ^is_dstPort_le_53);
87+
("is_dstPort_ge_53", ^is_dstPort_ge_53);
88+
("is_srcNAT_le_54587", ^is_srcNAT_le_54587);
89+
("is_srcNAT_ge_54587", ^is_srcNAT_ge_54587);
90+
("is_dstNAT_le_53", ^is_dstNAT_le_53);
91+
("is_dstNAT_ge_53", ^is_dstNAT_ge_53);
92+
("is_srcPort_le_56258", ^is_srcPort_le_56258);
93+
("is_srcPort_ge_56258", ^is_srcPort_ge_56258);
94+
("is_dstPort_le_3389", ^is_dstPort_le_3389);
95+
("is_dstPort_ge_3389", ^is_dstPort_ge_3389);
96+
("is_srcNAT_le_56258", ^is_srcNAT_le_56258);
97+
("is_srcNAT_ge_56258", ^is_srcNAT_ge_56258);
98+
("is_dstNAT_le_3389", ^is_dstNAT_le_3389);
99+
("is_dstNAT_ge_3389", ^is_dstNAT_ge_3389);
100+
]”;
101+
102+
(* Grouped policy ordering *)
103+
val policy_full_order = “[
104+
("srcPortGrp",["is_srcPort_le_57222";"is_srcPort_ge_57222";"is_srcPort_le_56258";"is_srcPort_ge_56258"]);
105+
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389"]);
106+
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258"]);
107+
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389"])
108+
]”;
109+
110+
(* Flat policy order (grouped) *)
111+
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"]”;
112+
113+
114+
(***********************************************)
115+
116+
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)
117+
118+
119+
val _ = export_theory ();

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

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
open bdd_utilsLib;
6+
open sptrees_fwd_proofLib;
7+
8+
9+
val _ = new_theory "internet_firewall_3";
10+
11+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
12+
13+
val test_pd_type = “[("h", type_record [("srcPort", type_length 16);
14+
("dstPort", type_length 16);
15+
("srcNAT", type_length 16);
16+
("dstNAT", type_length 16)])]”;
17+
18+
(************************************************)
19+
20+
(* rule 1 *)
21+
22+
val is_srcPort_le_57222 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
23+
val is_srcPort_ge_57222 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
24+
25+
val is_dstPort_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
26+
val is_dstPort_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
27+
28+
val is_srcNAT_le_54587 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
29+
val is_srcNAT_ge_54587 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
30+
31+
val is_dstNAT_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
32+
val is_dstNAT_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
33+
34+
35+
val arith_policy_rule1 = “((arith_and (arith_a ^is_srcPort_le_57222)
36+
(arith_and (arith_a ^is_srcPort_ge_57222)
37+
(arith_and (arith_a ^is_dstPort_le_53)
38+
(arith_and (arith_a ^is_dstPort_ge_53)
39+
(arith_and (arith_a ^is_srcNAT_le_54587)
40+
(arith_and (arith_a ^is_srcNAT_ge_54587)
41+
(arith_and (arith_a ^is_dstNAT_le_53)
42+
(arith_a ^is_dstNAT_ge_53)))))))) ,
43+
action ("allow",[1])):single_rule”;
44+
45+
(* rule 2 *)
46+
47+
val is_srcPort_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
48+
val is_srcPort_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
49+
50+
val is_dstPort_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
51+
val is_dstPort_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
52+
53+
val is_srcNAT_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
54+
val is_srcNAT_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
55+
56+
val is_dstNAT_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
57+
val is_dstNAT_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
58+
59+
60+
val arith_policy_rule2 = “((arith_and (arith_a ^is_srcPort_le_56258)
61+
(arith_and (arith_a ^is_srcPort_ge_56258)
62+
(arith_and (arith_a ^is_dstPort_le_3389)
63+
(arith_and (arith_a ^is_dstPort_ge_3389)
64+
(arith_and (arith_a ^is_srcNAT_le_56258)
65+
(arith_and (arith_a ^is_srcNAT_ge_56258)
66+
(arith_and (arith_a ^is_dstNAT_le_3389)
67+
(arith_a ^is_dstNAT_ge_3389)))))))) ,
68+
action ("allow",[1])):single_rule”;
69+
70+
(* rule 3 *)
71+
72+
val is_srcPort_le_6881 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 6881 16))”;
73+
val is_srcPort_ge_6881 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 6881 16))”;
74+
75+
val is_dstPort_le_50321 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 50321 16))”;
76+
val is_dstPort_ge_50321 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 50321 16))”;
77+
78+
val is_srcNAT_le_43265 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 43265 16))”;
79+
val is_srcNAT_ge_43265 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 43265 16))”;
80+
81+
val is_dstNAT_le_50321 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 50321 16))”;
82+
val is_dstNAT_ge_50321 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 50321 16))”;
83+
84+
85+
val arith_policy_rule3 = “((arith_and (arith_a ^is_srcPort_le_6881)
86+
(arith_and (arith_a ^is_srcPort_ge_6881)
87+
(arith_and (arith_a ^is_dstPort_le_50321)
88+
(arith_and (arith_a ^is_dstPort_ge_50321)
89+
(arith_and (arith_a ^is_srcNAT_le_43265)
90+
(arith_and (arith_a ^is_srcNAT_ge_43265)
91+
(arith_and (arith_a ^is_dstNAT_le_50321)
92+
(arith_a ^is_dstNAT_ge_50321)))))))) ,
93+
action ("allow",[1])):single_rule”;
94+
95+
(* Default policy rule *)
96+
val arith_policy_rule_default = “(arith_a a_True, action ("drop", [])):single_rule”;
97+
98+
(* Combined arith policy list *)
99+
val arith_policy = “[
100+
^arith_policy_rule1;
101+
^arith_policy_rule2;
102+
^arith_policy_rule3;
103+
^arith_policy_rule_default
104+
]:single_rule list”;
105+
106+
107+
108+
(* Combined policy mapping *)
109+
val policy_me = “[
110+
("is_srcPort_le_57222", ^is_srcPort_le_57222);
111+
("is_srcPort_ge_57222", ^is_srcPort_ge_57222);
112+
("is_dstPort_le_53", ^is_dstPort_le_53);
113+
("is_dstPort_ge_53", ^is_dstPort_ge_53);
114+
("is_srcNAT_le_54587", ^is_srcNAT_le_54587);
115+
("is_srcNAT_ge_54587", ^is_srcNAT_ge_54587);
116+
("is_dstNAT_le_53", ^is_dstNAT_le_53);
117+
("is_dstNAT_ge_53", ^is_dstNAT_ge_53);
118+
("is_srcPort_le_56258", ^is_srcPort_le_56258);
119+
("is_srcPort_ge_56258", ^is_srcPort_ge_56258);
120+
("is_dstPort_le_3389", ^is_dstPort_le_3389);
121+
("is_dstPort_ge_3389", ^is_dstPort_ge_3389);
122+
("is_srcNAT_le_56258", ^is_srcNAT_le_56258);
123+
("is_srcNAT_ge_56258", ^is_srcNAT_ge_56258);
124+
("is_dstNAT_le_3389", ^is_dstNAT_le_3389);
125+
("is_dstNAT_ge_3389", ^is_dstNAT_ge_3389);
126+
("is_srcPort_le_6881", ^is_srcPort_le_6881);
127+
("is_srcPort_ge_6881", ^is_srcPort_ge_6881);
128+
("is_dstPort_le_50321", ^is_dstPort_le_50321);
129+
("is_dstPort_ge_50321", ^is_dstPort_ge_50321);
130+
("is_srcNAT_le_43265", ^is_srcNAT_le_43265);
131+
("is_srcNAT_ge_43265", ^is_srcNAT_ge_43265);
132+
("is_dstNAT_le_50321", ^is_dstNAT_le_50321);
133+
("is_dstNAT_ge_50321", ^is_dstNAT_ge_50321);
134+
]”;
135+
136+
(* Grouped policy ordering *)
137+
val policy_full_order = “[
138+
("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"]);
139+
("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"]);
140+
("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"]);
141+
("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"])
142+
]”;
143+
144+
(* Flat policy order (grouped) *)
145+
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"]”;
146+
147+
148+
(***********************************************)
149+
150+
val final_thm_res =
151+
sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
152+
153+
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sig‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ sig
33
include Abbrev
44

55

6-
val convert_arith_policy_to_interval_tables : term * term * term * term * term -> thm
6+
val sptrees_convert_arith_policy_to_interval_tables : term * term * term * term * term -> thm
77
val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
88

99

‎hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sml‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,10 @@ open apply_trans_to_IOLib;
6767
(* STAGE 1 *)
6868
(***********************)
6969

70+
val start_cpu_stage1 = Timer.startCPUTimer ();
71+
val start_real_stage1 = Timer.startRealTimer ();
72+
73+
7074
(*convert arith policy to var policy*)
7175
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
7276
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
@@ -83,6 +87,8 @@ open apply_trans_to_IOLib;
8387
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
8488
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
8589

90+
val _ = time_stage ("Stage 1", start_cpu_stage1, start_real_stage1)
91+
8692

8793
(***********************)
8894
(* STAGE 2 *)
@@ -93,9 +99,10 @@ open apply_trans_to_IOLib;
9399
val (final_policy_bdd, tbl, final_table_bdd) =
94100
apply_trans_to_IOLib.sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order);
95101

102+
val _ = time_stage ("Stage 2 from var policy to BDD", start_cpu_stage2, start_real_stage2);
103+
96104

97105

98-
val get_i_policy = bdd_utilsLib.pairBDDs (final_policy_bdd, final_table_bdd);
99106

100107

101108

@@ -104,7 +111,7 @@ open apply_trans_to_IOLib;
104111
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 ”);
105112

106113

107-
114+
(*
108115
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”;
109116
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;
110117
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] var_eq_thm_extract_red;
@@ -183,9 +190,9 @@ open apply_trans_to_IOLib;
183190
fs[cond1_thm, cond2_thm, cond3_thm]
184191
);
185192
186-
193+
*)
187194
in
188-
final_thm
195+
eval_table_full_opt_auto (*final_thm*)
189196
end;
190197

191198
end;

0 commit comments

Comments
 (0)