Skip to content

Commit 7dcac97

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
fwd_proof file with an example
1 parent abe4b14 commit 7dcac97

File tree

5 files changed

+363
-2
lines changed

5 files changed

+363
-2
lines changed

‎Makefile‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ hol/p4_from_json: hol
1212
Holmake -r -I hol/p4_from_json
1313

1414
policy_to_table: hol
15+
cd hol/policy_to_table && Holmake bdd_utils.uo && Holmake fwd_proof.uo
1516
Holmake -r -I hol -I hol/policy_to_table
16-
17+
1718
validate: hol/p4_from_json
1819
cd hol/p4_from_json && ./validate.sh
1920

@@ -31,4 +32,7 @@ clean:
3132
cd hol && Holmake clean -r && cd p4_from_json && Holmake clean && cd validation_tests && Holmake clean
3233
cd hol/policy_to_table && Holmake clean
3334

35+
clean_policy:
36+
cd hol/policy_to_table && Holmake clean
37+
3438
.PHONY: default clean hol

‎hol/policy_to_table/Holmakefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ DEPENDENCIES = ..
66
# configuration
77
# ----------------------------------
88
HOLHEAP = ../p4-heap
9-
NEWHOLHEAP = table_to_policy-heap
9+
NEWHOLHEAP = policy_to_table-heap
1010

1111
HEAPINC_EXTRA = wordsLib
1212

‎hol/policy_to_table/auto_test1Script.sml‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
val _ = load "bdd_utils";
6+
val _ = load "fwd_proof";
7+
8+
9+
val _ = new_theory "auto_test1";
10+
11+
12+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
13+
14+
15+
val test_pd_type1 = “[("ip", type_record [("ttl", type_length 6)])]”;
16+
17+
val is_le_than_10 = “(arithm_le (lv_acc (lv_x "ip") "ttl") ^(BDDUtils.make_bv 10 6))”;
18+
val is_ge_than_10 = “(arithm_ge (lv_acc (lv_x "ip") "ttl") ^(BDDUtils.make_bv 10 6))”;
19+
20+
val is_ge_than_30 = “(arithm_ge (lv_acc (lv_x "ip") "ttl") ^(BDDUtils.make_bv 30 6))”;
21+
val is_le_than_9 = “(arithm_le (lv_acc (lv_x "ip") "ttl") ^(BDDUtils.make_bv 9 6))”;
22+
23+
24+
val policy_me1 = “[("x", ^is_le_than_10)]”;
25+
26+
val policy_full_order1 = “[("a",["x"])]”;
27+
28+
val policy_order1 = “["x"]”;
29+
30+
(* Rule 1: ttl <= 10 : accept *)
31+
val arith_policy_rule1 = “((arith_a ^is_le_than_10),
32+
action ("accept",[])):single_rule”;
33+
34+
(* Default forward rule *)
35+
val arith_policy_default = “(arith_a a_True,
36+
action ("reject",[])):single_rule”;
37+
38+
val arith_policy1 = “[^arith_policy_rule1;
39+
^arith_policy_default]:single_rule list”;
40+
41+
42+
43+
val final_thm_res1 =
44+
mk_fwd_proof.convert_arith_policy_to_interval_tables (arith_policy1, policy_me1, test_pd_type1, policy_full_order1, policy_order1);
45+
46+
(*********************************)
47+
48+
val arith_policy_rule2 = “((arith_a ^is_ge_than_30),
49+
action ("accept",[])):single_rule”;
50+
51+
52+
val arith_policy2 = “[^arith_policy_rule2;
53+
^arith_policy_default]:single_rule list”;
54+
55+
val policy_me2 = “[("x", ^is_ge_than_30)]”;
56+
57+
58+
val final_thm_res2 =
59+
mk_fwd_proof.convert_arith_policy_to_interval_tables (arith_policy2, policy_me2, test_pd_type1, policy_full_order1, policy_order1);
60+
61+
(***********************)
62+
63+
val arith_policy_rule3 = “(arith_or (arith_a ^is_ge_than_10) (arith_a ^is_le_than_9),
64+
action ("reject",[])):single_rule”;
65+
66+
67+
68+
val arith_policy3 = “[^arith_policy_default;
69+
^arith_policy_rule3]:single_rule list”;
70+
71+
val policy_me3 = “[("x", ^is_ge_than_10);("y", ^is_le_than_9)]”;
72+
73+
val policy_full_order3 = “[("a",["x";"y"])]”;
74+
75+
val policy_order3 = “["x";"y"]”;
76+
77+
78+
val final_thm_res3 =
79+
mk_fwd_proof.convert_arith_policy_to_interval_tables (arith_policy3, policy_me3, test_pd_type1, policy_full_order3, policy_order3);
80+
81+
82+
83+
84+
85+
86+
87+
88+
val _ = export_theory ();
89+
90+
91+
92+
93+
94+

‎hol/policy_to_table/auto_test_pipelineScript.sml‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
val _ = load "bdd_utils";
6+
val _ = load "fwd_proof";
7+
8+
9+
val _ = new_theory "auto_test_pipeline";
10+
11+
12+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
13+
14+
15+
val test_pd_type = “[("ip", type_record [("priority", type_length 3);
16+
("size", type_length 16);
17+
("age", type_length 8);
18+
("type", type_length 4)])]”;
19+
20+
val is_high_priority = “(arithm_le (lv_acc (lv_x "ip") "priority") ^(BDDUtils.make_bv 2 3))”;
21+
val is_medium_priority = “(arithm_ge (lv_acc (lv_x "ip") "priority") ^(BDDUtils.make_bv 4 3))”;
22+
val is_small_packet = “(arithm_le (lv_acc (lv_x "ip") "size") ^(BDDUtils.make_bv 500 16))”;
23+
val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^(BDDUtils.make_bv 200 8))”;
24+
val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 3 4))”;
25+
val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 8 4))”;
26+
27+
val policy_me = “[("x", ^is_high_priority);
28+
("y", ^is_medium_priority);
29+
("z", ^is_small_packet);
30+
("w", ^is_young_packet);
31+
("q", ^is_control_type);
32+
("r", ^is_data_type)]”;
33+
34+
val policy_full_order = “[("a",["x";"y"]);
35+
("b",["z"]);
36+
("c",["w"]);
37+
("d",["q";"r"])]”;
38+
39+
val policy_order = “["x";"y";"z";"w";"q";"r"]”;
40+
41+
(* Rule 1: High priority small control packets - expedited forwarding *)
42+
val arith_policy_rule1 = “(arith_and (arith_a ^is_high_priority)
43+
(arith_and (arith_a ^is_small_packet) (arith_a ^is_control_type)),
44+
action ("fwd_priority",[1; 255])):single_rule”;
45+
46+
(* Rule 2: High priority data packets *)
47+
val arith_policy_rule2 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_data_type),
48+
action ("fwd",[1])):single_rule”;
49+
50+
(* Rule 3: Medium priority young packets *)
51+
val arith_policy_rule3 = “(arith_and (arith_a ^is_medium_priority) (arith_a ^is_young_packet),
52+
action ("fwd",[2])):single_rule”;
53+
54+
(* Rule 7: Default forward rule *)
55+
val arith_policy_rule7 = “(arith_a a_True,
56+
action ("fwd",[5])):single_rule”;
57+
58+
val arith_policy = “[^arith_policy_rule1;
59+
^arith_policy_rule2;
60+
^arith_policy_rule3;
61+
^arith_policy_rule7]:single_rule list”;
62+
63+
64+
65+
val final_thm_res =
66+
mk_fwd_proof.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
67+
68+
69+
val _ = export_theory ();
70+
71+
72+
73+
74+
75+

‎hol/policy_to_table/fwd_proof.sml‎

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
open arithmeticTheory stringTheory containerTheory pred_setTheory
3+
listTheory finite_mapTheory;
4+
5+
open bitstringTheory;
6+
open wordsTheory;
7+
open optionTheory;
8+
open sumTheory;
9+
open stringTheory;
10+
open ottTheory;
11+
open pairTheory;
12+
open rich_listTheory;
13+
open arithmeticTheory;
14+
open alistTheory;
15+
open numeralTheory;
16+
open alistTheory;
17+
18+
19+
open p4Lib;
20+
open blastLib bitstringLib;
21+
open p4Theory;
22+
open p4_auxTheory;
23+
open p4_coreTheory;
24+
25+
open bdd_genTheory;
26+
open pred_specTheory;
27+
open policy_specTheory;
28+
open tables_specTheory;
29+
open bdd_isomorphTheory;
30+
open bdd_end_to_endTheory;
31+
32+
open policy_arith_to_varTheory;
33+
open table_var_to_arithTheory;
34+
open table_arith_to_intervalTheory;
35+
36+
open bdd_auxTheory;
37+
open table_bs_propertiesTheory;
38+
39+
40+
41+
val _ = load "bdd_utils";
42+
43+
44+
45+
(* a few types abbreviations *)
46+
(*
47+
val _ = type_abbrev("BDD_tbl_type", “:(( (string# num list) var_table_list, (string# num list) action_expr) BDD)”);
48+
49+
val _ = type_abbrev("struc_tbl_type", “:((( atom_var list # num # (string# num list) action_expr) list list # num,
50+
(string# num list) action_expr) decision_structure)”);
51+
52+
val _ = type_abbrev("action_rule_type", “:((string# num list) action_expr) rule”);
53+
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
54+
*)
55+
56+
57+
58+
structure mk_fwd_proof = struct
59+
60+
61+
fun convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
62+
63+
let
64+
65+
(***********************)
66+
(* STAGE 1 *)
67+
(***********************)
68+
69+
(*convert arith policy to var policy*)
70+
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
71+
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
72+
73+
74+
(* first establish distinction of domain and range of me*)
75+
val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
76+
val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
77+
78+
val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
79+
80+
81+
(* Theorem of correctness for conversion from arith policy to var policy *)
82+
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
83+
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
84+
85+
86+
(***********************)
87+
(* STAGE 2 *)
88+
(***********************)
89+
90+
(* create BDD of var policy *)
91+
val eval_policy_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
92+
val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
93+
94+
95+
(* automatically generate a var table from the var policy's BDD via sml*)
96+
val test_groupings = rhs(concl(EVAL policy_full_order));
97+
val gen_var_table_auto = BDDUtils.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
98+
99+
100+
(* now create a BDD for the table*)
101+
val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
102+
val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
103+
104+
105+
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
106+
val get_i_policy = BDDUtils.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
107+
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
108+
^eval_table_full_opt_auto_rhs”;
109+
*)
110+
111+
112+
(* Theorem of correctness for conversion from var policy to var table *)
113+
114+
(* method 1 *)
115+
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 ”;
116+
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy_thm_init;
117+
118+
119+
120+
(***********************)
121+
(* STAGE 3 *)
122+
(***********************)
123+
124+
(* covert var table to interval table *)
125+
val only_var_table = fst (dest_pair gen_var_table_auto);
126+
val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
127+
val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
128+
129+
130+
(* Theorem of correctness for conversion from var table to inteval table *)
131+
val var_table_sinterval_tbl_thm =
132+
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);
133+
134+
135+
136+
(* to glue the theorems we need to take care of the conditions/ assumptions *)
137+
138+
(* condition1 *)
139+
val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
140+
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);
141+
142+
143+
(* condition2 *)
144+
val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
145+
val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
146+
147+
val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
148+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
149+
(ISPECL[policy_me, test_pd_type, policy_order ]
150+
wf_format_imp_cond2);
151+
152+
(* condition3 *)
153+
val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
154+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
155+
(ISPECL[policy_me, test_pd_type]
156+
wf_format_imp_cond3);
157+
158+
159+
val final_thm = prove(
160+
“! packet_input .
161+
wf_packet ^test_pd_type packet_input ⇒
162+
sem_arith_policy ^arith_policy packet_input =
163+
sem_sinterval_tables (^only_interval_table1,0) packet_input”
164+
,
165+
166+
rpt strip_tac >>
167+
168+
assume_tac arith_policy_var_policy_thm >>
169+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
170+
171+
assume_tac var_policy_var_table_thm >>
172+
first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
173+
174+
175+
assume_tac var_table_sinterval_tbl_thm >>
176+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
177+
178+
fs[cond1_thm, cond2_thm, cond3_thm]
179+
);
180+
181+
in
182+
final_thm
183+
end;
184+
185+
end;
186+
187+
188+

0 commit comments

Comments
 (0)