Skip to content

Commit a0413e3

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
debugging forward proof, now blue print
1 parent 67dd0cb commit a0413e3

File tree

1 file changed

+20
-202
lines changed

1 file changed

+20
-202
lines changed

‎hol/bdd_test_casesScript.sml‎

Lines changed: 20 additions & 202 deletions
Original file line numberDiff line numberDiff line change
@@ -69,41 +69,6 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
6969
(* policy 1: arith POLICY representation *)
7070

7171

72-
73-
(*
74-
val test_pd_type1 = “[("h" , type_record [("ttl", type_length 8);
75-
("flag", type_length 4)])]”;
76-
77-
78-
val is_high_ttl = “(arithm_le (lv_acc (lv_x "h") "ttl") ^(BDDUtils.make_bv 100 8) )”;
79-
val is_low_ttl = “(arithm_ge (lv_acc (lv_x "h") "ttl") ^(BDDUtils.make_bv 1 8) )”;
80-
val is_flag_ok = “(arithm_le (lv_acc (lv_x "h") "flag") ^(BDDUtils.make_bv 3 4) )”;
81-
82-
83-
val policy1_me1 = “[("x", ^is_high_ttl);
84-
("y", ^is_low_ttl );
85-
("z", ^is_flag_ok)]”;
86-
87-
val policy1_full_order = “[("a",["x";"y"]);("b",["z"])]”;
88-
89-
val policy1_order = “["x";"y";"z"]”;
90-
91-
92-
val arith_policy1_rule1 = “(arith_and (arith_a ^is_high_ttl) ( arith_a ^is_low_ttl) ,
93-
action ("fwd",[(1:num)])):((string# num list) action_expr) arith_rule”;
94-
95-
val arith_policy1_rule2 = “(arith_a (^is_flag_ok) , action ("fwd",[2]))
96-
:((string# num list) action_expr) arith_rule”;
97-
98-
val arith_policy1_rule3 = “(arith_a a_True, action ("drop",[])):((string# num list) action_expr) arith_rule”;
99-
100-
101-
val arith_policy1 = “[^arith_policy1_rule1 ;
102-
^arith_policy1_rule2 ;
103-
^arith_policy1_rule3]:((string# num list) action_expr) arith_policy”;
104-
*)
105-
106-
10772

10873
val test_pd_type1 = “[("ip", type_record [("priority", type_length 3);
10974
("size", type_length 16);
@@ -156,7 +121,12 @@ val arith_policy1 = “[^arith_policy1_rule1;
156121

157122
(********************************)
158123

159-
124+
125+
126+
(***********************)
127+
(* STAGE 1 *)
128+
(***********************)
129+
160130
(*convert arith policy to var policy*)
161131
val arith_policy1_eval = EVAL “convert_arith_to_var_policy ^arith_policy1 ^policy1_me1”;
162132
val var_policy1 = optionSyntax.dest_some (rhs (concl arith_policy1_eval));
@@ -173,6 +143,10 @@ val all_distinct_conj = CONJ policy1_me1_fst_distinct policy1_me1_snd_distinct;
173143
val arith_policy1_var_policy1_thm = REWRITE_RULE[all_distinct_conj, arith_policy1_eval]
174144
(ISPECL[arith_policy1, var_policy1, policy1_me1] policy_airth_to_var_sem_conversion_correct);
175145

146+
147+
(***********************)
148+
(* STAGE 2 *)
149+
(***********************)
176150

177151
(* create BDD of var policy *)
178152
val eval_policy1_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy1))]) [] ^policy1_order 1”;
@@ -191,15 +165,24 @@ val eval_table1_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_tabl
191165

192166
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
193167
val get_i_policy1 = BDDUtils.pairBDDs (eval_policy1_full_opt_rhs, eval_table1_full_opt_auto_rhs);
194-
val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy1 ^eval_policy1_full_opt_rhs
168+
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy1 ^eval_policy1_full_opt_rhs
195169
^eval_table1_full_opt_auto_rhs”;
170+
*)
196171

197172

198173
(* Theorem of correctness for conversion from var policy to var table *)
174+
175+
(* we can do it in two methods, this is: *)
176+
(* method 1 *)
199177
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 ”;
200178
val policy1_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy1_thm_init;
201179

202180

181+
182+
(***********************)
183+
(* STAGE 3 *)
184+
(***********************)
185+
203186
(* covert var table to interval table *)
204187
val only_var_table1 = fst (dest_pair test_action_table1_auto);
205188
val convert_to_interval1 = EVAL “convert_var_to_sinterval_tables ^only_var_table1 ^policy1_me1 ^test_pd_type1”;
@@ -272,171 +255,6 @@ TODO:
272255

273256

274257

275-
276-
277-
(*
278-
279-
(****************************************************************)
280-
(****************************************************************)
281-
(* POLICY 2 *)
282-
(****************************************************************)
283-
(****************************************************************)
284-
285-
(* This is the camus paper example
286-
x : fwd(1)
287-
x ∧ z : fwd(2)
288-
y ∧ w : fwd(3)
289-
T : drop()
290-
*)
291-
292-
293-
294-
(* policy 2: var policy representation *)
295-
val var_policy2_rule1 = ``(Var "x", action ("fwd",[1])): action_rule_type``;
296-
val var_policy2_rule2 = ``(And (Var "x") (Var "z"), action ("fwd",[2])): action_rule_type``;
297-
val var_policy2_rule3 = ``(And (Var "y") (Var "w"), action ("fwd",[3])): action_rule_type``;
298-
val var_policy2_rule4 = ``(True, action ("drop",[])): action_rule_type``;
299-
300-
val var_policy2 = ``[ ^var_policy2_rule1; ^var_policy2_rule2; ^var_policy2_rule3; ^var_policy2_rule4 ] : action_policy_type``;
301-
302-
val eval_policy2_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy2))]) [] ["x";"y";"z";"w"] 1”;
303-
val eval_policy2_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy2_full_opt));
304-
305-
306-
307-
(* automatically generate a table*)
308-
val test_groupings2 = rhs(concl(EVAL “[("a",["x";"y"]);("b",["z";"w"])]”));
309-
val test_action_table2_auto =BDDUtils.bdd_to_tables_iterative eval_policy2_full_opt_rhs test_groupings2;
310-
311-
(* now create a BDD for the table*)
312-
val eval_table2_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^test_action_table2_auto))]) [] ["x";"y";"z";"w"] 1”;
313-
val eval_table2_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table2_full_opt_auto));
314-
315-
(* get I, and check if isisIsomorph *)
316-
val get_i_policy2 = BDDUtils.pairBDDs (eval_table2_full_opt_auto_rhs , eval_table2_full_opt_auto_rhs);
317-
val is_tbl_policy2_iso = EVAL “isIsomorph_exec ^get_i_policy2 ^eval_table2_full_opt_auto_rhs ^eval_table2_full_opt_auto_rhs”;
318-
319-
(* get a theorem out*)
320-
val policy2_thm_init = computeLib.RESTR_EVAL_CONV [“sem_tables”,“sem_policy”, “mv_dom_vars”] “correct_var_policy_var_tables_exec ^var_policy2 ^test_action_table2_auto ["x";"y";"z";"w"] ^get_i_policy2 ”;
321-
val policy2_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy2_thm_init;
322-
323-
324-
*)
325-
326-
327-
328-
329-
(* (* Manual effort*)
330-
(* policy 2: var table representation *)
331-
val var_tbl1_line1 = ``([(Var "x")] , 0, state 1): (string# num list) line``;
332-
val var_tbl1_line2 = ``([Not (Var "x"); (Var "y")] , 0, state 3): (string# num list) line``;
333-
val var_tbl1_line3 = ``([Not (Var "x"); Not (Var "y")] , 0, state 4): (string# num list) line``;
334-
335-
val var_tbl1 = ``[^var_tbl1_line1; ^var_tbl1_line2; ^var_tbl1_line3] : (string# num list) table``;
336-
337-
338-
val var_tbl2_line1 = ``([(Var "z"); (Var "w")] , 3, state 7): (string# num list) line``;
339-
val var_tbl2_line2 = ``([(Var "z"); Not (Var "w")] , 3, state 8): (string# num list) line``;
340-
val var_tbl2_line3 = ``([Not (Var "z"); (Var "w")] , 3, state 9): (string# num list) line``;
341-
val var_tbl2_line4 = ``([Not (Var "z"); Not (Var "w")] , 3, state 10): (string# num list) line``;
342-
val var_tbl2_line5 = ``([True] , 1, state 1): (string# num list) line``;
343-
val var_tbl2_line6 = ``([True] , 4, state 4): (string# num list) line``;
344-
345-
346-
val var_tbl2 = ``[^var_tbl2_line1; ^var_tbl2_line2; ^var_tbl2_line3;
347-
^var_tbl2_line4; ^var_tbl2_line5; ^var_tbl2_line6] : (string# num list) table``;
348-
349-
350-
val var_tbl3_line1 = ``([True] , 1, action ("fwd",[1])): (string# num list) line``;
351-
val var_tbl3_line2 = ``([True] , 4, action ("drop",[])): (string# num list) line``;
352-
val var_tbl3_line3 = ``([True] , 7, action ("fwd",[3])): (string# num list) line``;
353-
val var_tbl3_line4 = ``([True] , 8, action ("drop",[])): (string# num list) line``;
354-
val var_tbl3_line5 = ``([True] , 9, action ("fwd",[3])): (string# num list) line``;
355-
val var_tbl3_line6 = ``([True] , 10, action ("drop",[])): (string# num list) line``;
356-
357-
val var_tbl3 = ``[^var_tbl3_line1; ^var_tbl3_line2; ^var_tbl3_line3;
358-
^var_tbl3_line4; ^var_tbl3_line5; ^var_tbl3_line6] : (string# num list) table``;
359-
360-
val var_tbls2 = ``[^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list) ``;
361-
val var_tbls2_start = ``([^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list),(0:num)) ``;
362-
363-
364-
val eval_table2_full_opt = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^var_tbls2_start))]) [] ["x";"y";"z";"w"] 1”;
365-
val eval_table1_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_table2_full_opt));
366-
367-
val get_i_policy2 = BDDUtils.pairBDDs (eval_policy2_full_opt_rhs, eval_table1_full_opt_rhs);
368-
val is_tbl_policy2_iso = EVAL “isIsomorph_exec ^get_i_policy2 ^eval_policy2_full_opt_rhs ^eval_table1_full_opt_rhs”;
369-
*)
370-
371-
372-
373-
374-
375-
(***************************************************)
376-
377-
(*
378-
val AND = ``λ(p1,a1) (p2,a2). (arith_and p1 p2, a2)``;
379-
val OR = ``λ(p1,a1) (p2,a2). (arith_or p1 p2, a1)``;
380-
val NOT = ``λ(p,a). (arith_not p, a)``;
381-
*)
382-
383-
(*
384-
val test_packet = “[
385-
("h", val_record [
386-
("ip", val_record [
387-
("ttl", val_num 64);
388-
("proto", val_num 6);
389-
("version", val_num 4)
390-
]);
391-
("src_zone", val_num 1);
392-
("threat_score", val_num 30);
393-
("auth_status", val_num 1)
394-
])
395-
]”;
396-
397-
398-
val is_tcp = “arith_a (arithm_le (lv_acc (lv_acc (lv_x "h") "ip") "proto") 6)”;
399-
val is_high_ttl = “arith_a (arithm_ge (lv_acc (lv_acc (lv_x "h") "ip") "ttl") 60)”;
400-
val is_internal = “arith_a (arithm_le (lv_acc (lv_x "h") "src_zone") 1)”;
401-
val is_malicious = “arith_a (arithm_ge (lv_acc (lv_x "h") "threat_score") 80)”;
402-
403-
404-
val policy3_me1 = “[
405-
("is_tcp", (arithm_eq (lv_acc (lv_acc (lv_x "h") "ip") "proto") 6));
406-
("is_high_ttl", (arithm_gt (lv_acc (lv_acc (lv_x "h") "ip") "ttl") 60));
407-
("is_internal", (arithm_eq (lv_acc (lv_x "h") "src_zone") 1));
408-
("is_malicious", (arithm_gt (lv_acc (lv_x "h") "threat_score") 80))
409-
]”;
410-
411-
val arith_policy3_rule1 = “(arith_and ^is_tcp ^is_high_ttl , action ("fwd",[(1:num)])):((string# num list) action_expr) arith_rule”;
412-
val arith_policy3_rule2 = “(arith_or (arith_not ^is_tcp) (^is_high_ttl), action ("fwd",[2])) :((string# num list) action_expr) arith_rule”;
413-
val arith_policy3_rule3 = “(arith_a a_True, action ("drop",[])):((string# num list) action_expr) arith_rule”;
414-
415-
416-
val arith_policy3 = “[ ^arith_policy3_rule1 ;
417-
^arith_policy3_rule2 ;
418-
^arith_policy3_rule3]:((string# num list) action_expr) arith_policy”;
419-
420-
421-
val arith_policy3_eval = EVAL convert_arith_to_var_policy ^arith_policy3 ^policy3_me1”;
422-
423-
val var_policy3 = optionSyntax.dest_some (rhs (concl arith_policy3_eval));
424-
425-
426-
(* first establish distinction *)
427-
val policy3_me1_fst_distinct = EVAL ``ALL_DISTINCT (MAP FST ^policy3_me1)``;
428-
val policy3_me1_snd_distinct = EVAL ``ALL_DISTINCT (MAP SND ^policy3_me1)``;
429-
430-
(*second, combine them *)
431-
val all_distinct_conj = CONJ policy3_me1_fst_distinct policy3_me1_snd_distinct;
432-
433-
val alookup_cond_thm = EVAL “∀var atom. ALOOKUP ^policy3_me1 var = SOME atom ⇒ ALOOKUP m_v var = eval_arithm_atom packet_input atom”;
434-
435-
436-
val arith_policy3_var_policy3_thm = REWRITE_RULE[all_distinct_conj, arith_policy3_eval]
437-
(ISPECL[arith_policy3, var_policy3, policy3_me1] policy_airth_to_var_sem_conversion_correct);
438-
439-
*)
440258

441259

442260
val _ = export_theory ();

0 commit comments

Comments
 (0)