changed the strategy for the last part of the pipeline, now it is 3 stages instead of one shot

Author: AnoudAlshnakat

hol/bdd_end_to_endScript.sml

@@ -171,7 +171,7 @@ Theorem table_mk_bdd_correct_thm:
     correct_sem table_structure BDD (REVERSE vars)
 Proof
   rpt strip_tac >>
-  assume_tac (INST_TYPE [“:'a” |-> “: (('a table) list # num)”, “:'b” |-> “: 'a action_expr”] correct_sem_translation)  >>
+  assume_tac (INST_TYPE [“:'a” |-> “: (('a var_table) list # num)”, “:'b” |-> “: 'a action_expr”] correct_sem_translation)  >>
   first_x_assum (strip_assume_tac o (Q.SPECL [‘vars’, ‘[]’,
                                               ‘(0,[],[(0,non_termn (NONE,(var_table)))])’,
                                               ‘BDD’, ‘table_structure’, ‘1’])) >>
@@ -530,7 +530,7 @@ Theorem table_mk_bdd_correct_valid_opt_thm:
 Proof
 
   rpt strip_tac >>
-  assume_tac (INST_TYPE [“:'a” |-> “: (('a table) list # num)”, “:'b” |-> “: 'a action_expr”]
+  assume_tac (INST_TYPE [“:'a” |-> “: (('a var_table) list # num)”, “:'b” |-> “: 'a action_expr”]
                         correct_sem_valid_translation_opt)  >>
 
   first_x_assum (strip_assume_tac o (Q.SPECL [‘vars’, ‘[]’,

hol/bdd_test_casesScript.sml

@@ -32,11 +32,12 @@ val _ = load "bdd_utils";
 
 val _ = new_theory "bdd_test_cases";
 
-
+(* TODO: update the sml definition that takes a var bdd and generates var table, now the var_table has new syntax. Var x | True | False | Not atom --> 
+Var x | Not x | Not True | Not False | True | False
 
 
 (* a few types abbreviations *)
-val _ = type_abbrev("BDD_tbl_type", “:(( (string# num list) table_list, (string# num list) action_expr) BDD)”);
+val _ = type_abbrev("BDD_tbl_type", “:(( (string# num list) var_table_list, (string# num list) action_expr) BDD)”);
 
 val _ = type_abbrev("struc_tbl_type", “:((( atom_var list # num # (string# num list) action_expr) list list # num,
                                           (string# num list) action_expr) decision_structure)”);
@@ -113,8 +114,8 @@ val var_tbl3_line2 = ``([True] , 7, action ("fwd",[2])): (string# num list) line
 val var_tbl3_line3 = ``([True] , 8, action ("drop",[])): (string# num list) line``;
 val var_tbl3 = ``[^var_tbl3_line1; ^var_tbl3_line2; ^var_tbl3_line3] : (string# num list) table``;
 
-val var_tbls1 = ``[^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) table_list) ``;
-val var_tbls1_start = ``([^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) table_list),(0:num)) ``;
+val var_tbls1 = ``[^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list) ``;
+val var_tbls1_start = ``([^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list),(0:num)) ``;
 
      
 val eval_table1_full_opt = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^var_tbls1_start))]) [] ["x";"y";"z"] 1”;
@@ -219,8 +220,8 @@ val var_tbl3_line6 = ``([True] , 10, action ("drop",[])): (string# num list) lin
 val var_tbl3 = ``[^var_tbl3_line1; ^var_tbl3_line2; ^var_tbl3_line3;
                  ^var_tbl3_line4; ^var_tbl3_line5; ^var_tbl3_line6] : (string# num list) table``;
 
-val var_tbls2 = ``[^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) table_list) ``;
-val var_tbls2_start = ``([^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) table_list),(0:num)) ``;
+val var_tbls2 = ``[^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list) ``;
+val var_tbls2_start = ``([^var_tbl1; ^var_tbl2; ^var_tbl3] : ((string# num list) var_table_list),(0:num)) ``;
 
 
 val eval_table2_full_opt = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^var_tbls2_start))]) [] ["x";"y";"z";"w"] 1”;
@@ -280,7 +281,7 @@ val arith_policy3 =   “[ ^arith_policy3_rule1 ;
                         ^arith_policy3_rule3]:((string# num list) action_expr) arith_policy”;
 
 
-val arith_policy3_eval = EVAL “convert ^arith_policy3 ^policy3_me1”;
+val arith_policy3_eval = EVAL convert_arith_to_var_policy ^arith_policy3 ^policy3_me1”;
 
 val var_policy3 = optionSyntax.dest_some (rhs (concl arith_policy3_eval));
 
@@ -300,6 +301,6 @@ val arith_policy3_var_policy3_thm = REWRITE_RULE[all_distinct_conj, arith_policy
 
 *)
 
-                       
+*)                       
 val _ = export_theory ();
 

hol/policy_arith_to_varScript.sml

@@ -46,8 +46,8 @@ val _ = Hol_datatype `
   arithm_atom = 
      a_True               (* T *)
    | a_False              (* F *)
-   | arithm_gt of arith_lv => bitv  (* lval > v *)
-   | arithm_lt of arith_lv => bitv  (* lval < v *)
+   | arithm_ge of arith_lv => bitv  (* lval ≤ v *)
+   | arithm_le of arith_lv => bitv  (* lval ≥ v *)
    (*| arithm_eq of arith_lv => num  (* lval = v *)*) (* this will be added to input policy *)
 `;
 
@@ -93,13 +93,13 @@ End
 Definition eval_arithm_atom_def:
   (eval_arithm_atom pd a_True = SOME T) ∧
   (eval_arithm_atom pd a_False = SOME F) ∧
-  (eval_arithm_atom pd (arithm_gt lval bv) = 
+  (eval_arithm_atom pd (arithm_ge lval bv) = 
     case resolve_lval pd lval of
-    | SOME (val_bs bv') => bitv_binpred binop_gt bv' bv
+    | SOME (val_bs bv') => bitv_binpred binop_ge bv' bv
     | _ => NONE) ∧
-  (eval_arithm_atom pd (arithm_lt lval bv) = 
+  (eval_arithm_atom pd (arithm_le lval bv) = 
     case resolve_lval pd lval of
-      SOME (val_bs bv') => bitv_binpred binop_lt bv' bv
+      SOME (val_bs bv') => bitv_binpred binop_le bv' bv
     | _ => NONE)
 End
 
@@ -271,15 +271,15 @@ End
 
 
 
-Definition all_convertable_def:
-  all_convertable m_e policy =
+Definition all_convertable_to_var_def:
+  all_convertable_to_var m_e policy =
   EVERY (λ(pred,_). pred_a2v m_e pred ≠ NONE) policy
 End
 
 
-Definition convert_def:
-  convert policy m_e =
-    if all_convertable m_e policy then
+Definition convert_arith_to_var_policy_def:
+  convert_arith_to_var_policy policy m_e =
+    if all_convertable_to_var m_e policy then
       SOME (MAP (λ(pred,act). (THE (pred_a2v m_e pred), act)) policy)
     else
       NONE
@@ -295,7 +295,7 @@ val test_me = ``[
 
 (* Sample policies *)
 val empty_policy = ``[] : (arith_pred # string) list``;
-val all_convertable_policy = ``[
+val all_convertable_to_var_policy = ``[
   (arith_a (arithm_gt (lv_x "x") 5), "allow");
   (arith_a (arithm_lt (lv_x "y") 2), "deny")
 ]``;
@@ -304,18 +304,18 @@ val partially_convertable_policy = ``[
   (arith_a (arithm_eq (lv_x "z") 1), "log")  (* Unmapped *)
 ]``;
 
-EVAL ``convert ^empty_policy ^test_me``;
+EVAL ``convert_arith_to_var_policy ^empty_policy ^test_me``;
 (*SOME []*)
-EVAL ``convert ^all_convertable_policy ^test_me``;
+EVAL ``convert_arith_to_var_policy ^all_convertable_to_var_policy ^test_me``;
 (*[(Var "x_gt_5", "allow"); (Var "y_lt_2", "deny")]*)
-EVAL ``convert ^partially_convertable_policy ^test_me``;
+EVAL ``convert_arith_to_var_policy ^partially_convertable_policy ^test_me``;
 (*NONE*)
 
 val complex_policy = ``[
   (arith_not (arith_a (arithm_gt (lv_x "x") 5)), "reject");
   (arith_and (arith_a a_True) (arith_a (arithm_lt (lv_x "y") 2)), "special")
 ]``;
-EVAL ``convert ^complex_policy ^test_me``;
+EVAL ``convert_arith_to_var_policy ^complex_policy ^test_me``;
 
 (*
    SOME [
@@ -413,7 +413,7 @@ Theorem policy_airth_to_var_sem_conversion_correct:
     (∀var atom. 
        ALOOKUP m_e var = SOME atom ⇒ 
        ALOOKUP m_v var = eval_arithm_atom packet_input atom) ∧
-    (convert arith_policy m_e = SOME var_policy)
+    (convert_arith_to_var_policy arith_policy m_e = SOME var_policy)
     ⇒
     sem_arith_policy arith_policy packet_input = 
     sem_policy var_policy m_v
@@ -423,7 +423,7 @@ Proof
   ‘check_arith_pred_sem arith_policy packet_input = check_sem_pred var_policy m_v’ 
     suffices_by rw[] >>
 
-  fs[convert_def] >>
+  fs[convert_arith_to_var_policy_def] >>
   rw[check_arith_pred_sem_def, check_sem_pred_def] >>
 
   rw[MAP_MAP_o] >>
@@ -433,9 +433,9 @@ Proof
   Cases_on ‘x’ >> rw[] >>
   rename1 ‘(pred, act)’ >>
 
-  (* Since all_convertable holds, pred_a2v m_e pred ≠ NONE *)
+  (* Since all_convertable_to_var holds, pred_a2v m_e pred ≠ NONE *)
   ‘pred_a2v m_e pred ≠ NONE’ by (
-    fs[all_convertable_def, EVERY_MEM] >>
+    fs[all_convertable_to_var_def, EVERY_MEM] >>
     rgs[ELIM_UNCURRY] >>
     res_tac >>
     fs[FST]