added a few test cases for time

AnoudAlshnakat · AnoudAlshnakat · commit ad402681362e · 2025-09-04T15:04:04.000+02:00
diff --git a/hol/policy_to_table/fwd_proofLib.sml b/hol/policy_to_table/fwd_proofLib.sml
@@ -41,29 +41,38 @@ open table_bs_propertiesTheory;
      
 open bdd_utilsLib;   
 
+        
 
+    fun time_stage (stage_name, timer_cpu, timer_real) = 
+        let
+            val cpu_time = Timer.checkCPUTimer timer_cpu
+            val real_time = Timer.checkRealTimer timer_real
+            val _ = HOL_MESG (stage_name ^ " completed in: " ^ 
+                          Time.toString (#usr cpu_time) ^ " user, " ^ 
+                          Time.toString (#sys cpu_time) ^ " system, " ^ 
+                          Time.toString real_time ^ " real\n")
+        in
+            (cpu_time, real_time)
+        end
 
-(* a few types abbreviations *)
-(*
-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)”);
-
-val _ = type_abbrev("action_rule_type", “:((string# num list) action_expr) rule”);
-val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
-*)
-        
 
 
     fun convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
 
     let
             
+    val start_cpu_total = Timer.startCPUTimer ();
+    val start_real_total = Timer.startRealTimer ();
+
+
         (***********************)
         (*       STAGE 1       *)
         (***********************)
 
+        val start_cpu_stage1 = Timer.startCPUTimer ();
+        val start_real_stage1 = Timer.startRealTimer ();
+
+
         (*convert arith policy to var policy*)        
         val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
         val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
@@ -81,25 +90,44 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
         (ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);  
 
 
+        val _ = time_stage ("Stage 1", start_cpu_stage1, start_real_stage1)
+
+
         (***********************)
         (*       STAGE 2       *)
         (***********************)
                               
+
+        val start_cpu_stage2 = Timer.startCPUTimer ();
+        val start_real_stage2 = Timer.startRealTimer ();
+
+
         (* create BDD of var policy  *)
         val eval_policy_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
         val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
 
+        val _ = time_stage ("Stage 2 from var policy to BDD", start_cpu_stage2, start_real_stage2);
+        val start_cpu_stage2_vbdd = Timer.startCPUTimer ();
+        val start_real_stage2_vbdd = Timer.startRealTimer ();
 
         (* automatically generate a var table from the var policy's BDD via sml*)
         val test_groupings = rhs(concl(EVAL policy_full_order));
         val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
 
             
+        val _ = time_stage ("Stage 2 from var BDD to table", start_cpu_stage2_vbdd, start_real_stage2_vbdd);
+        val start_cpu_stage2_tbl = Timer.startCPUTimer ();
+        val start_real_stage2_tbl = Timer.startRealTimer ();
+
         (* now create a BDD for the table*)    
         val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
         val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
 
             
+        val _ = time_stage ("Stage 2 from table to table BDD", start_cpu_stage2_tbl, start_real_stage2_tbl);
+        val start_cpu_stage2_tbdd = Timer.startCPUTimer ();
+        val start_real_stage2_tbdd = Timer.startRealTimer ();
+
         (* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
         val get_i_policy = bdd_utilsLib.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
         (*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
@@ -109,16 +137,23 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
             
         (* Theorem of correctness for conversion from var policy to var table *)
 
-        (* method 1 *)
         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 ”;     
         val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy_thm_init;    
 
+        val _ = time_stage ("Stage 2 proof", start_cpu_stage2_tbdd, start_real_stage2_tbdd);
+
+        val _ = time_stage ("Stage 2 total", start_cpu_stage2, start_real_stage2);
+
 
 
         (***********************)
         (*       STAGE 3       *)
         (***********************)   
 
+        val start_cpu_stage3 = Timer.startCPUTimer ();
+        val start_real_stage3 = Timer.startRealTimer ();
+
+
         (* covert var table to interval table *)
         val only_var_table = fst (dest_pair gen_var_table_auto);
         val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me  ^test_pd_type”;   
@@ -129,8 +164,17 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
         val var_table_sinterval_tbl_thm =
         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);        
 
+        val _ = time_stage ("Stage 3", start_cpu_stage3, start_real_stage3);
+
+
+
+
+        (***********************)
+        (*       FINAL PROOF   *)
+        (***********************)
+        val start_cpu_final = Timer.startCPUTimer ();
+        val start_real_final = Timer.startRealTimer ();
 
-                    
         (* to glue the theorems we need to take care of the conditions/ assumptions *)
                     
         (* condition1 *)                             
@@ -176,6 +220,13 @@ val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) p
           fs[cond1_thm, cond2_thm, cond3_thm]
         );
 
+
+        val _ = time_stage ("Final glue proof", start_cpu_final, start_real_final);
+
+        val _ = time_stage ("Total time of everything", start_cpu_total, start_real_total);
+
+
+
     in
     final_thm
     end;
diff --git a/hol/policy_to_table/policy_test_cases/auto_test2Script.sml b/hol/policy_to_table/policy_test_cases/auto_test2Script.sml
@@ -9,76 +9,72 @@ open fwd_proofLib;
 val _ = new_theory "auto_test2";
 
 val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
-
  
-val test_pd_type1 = “[("ip", type_record [("ttl", type_length 6)])]”;
-
-val is_le_than_10 = “(arithm_le (lv_acc (lv_x "ip") "ttl") ^(bdd_utilsLib.make_bv 10 6))”;
-val is_ge_than_10 = “(arithm_ge (lv_acc (lv_x "ip") "ttl") ^(bdd_utilsLib.make_bv 10 6))”;
-
-val is_ge_than_30 = “(arithm_ge (lv_acc (lv_x "ip") "ttl") ^(bdd_utilsLib.make_bv 30 6))”;
-val is_le_than_9  = “(arithm_le (lv_acc (lv_x "ip") "ttl") ^(bdd_utilsLib.make_bv 9 6))”;
-
-
-val policy_me1 =   “[("x", ^is_le_than_10)]”;
-
-val policy_full_order1 = “[("a",["x"])]”;
-
-val policy_order1 = “["x"]”;
-
-(* Rule 1: ttl <= 10 : accept *)
-val arith_policy_rule1 = “((arith_a ^is_le_than_10),
-                           action ("accept",[])):single_rule”;
-
-(* Default forward rule *)
-val arith_policy_default = “(arith_a a_True,
-                           action ("reject",[])):single_rule”;
-
-val arith_policy1 =   “[^arith_policy_rule1;
-                       ^arith_policy_default]:single_rule list”;
-
+val test_pd_type = “[("ip", type_record [("priority", type_length 3);
+                                         ("size", type_length 16);
+                                         ("age", type_length 8);
+                                         ("type", type_length 4)])]”;
 
+val is_high_priority = “(arithm_le (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 2 3))”;
+val is_medium_priority = “(arithm_ge (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 4 3))”;
 
-val final_thm_res1 =
-fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy1, policy_me1, test_pd_type1, policy_full_order1, policy_order1);
+val is_small_packet1 = “(arithm_le (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 500 16))”;
+val is_small_packet2 = “(arithm_le (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 400 16))”;
 
-(*********************************)
+val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^(bdd_utilsLib.make_bv 200 8))”;
 
-val arith_policy_rule2 = “((arith_a ^is_ge_than_30),
-                           action ("accept",[])):single_rule”;
+val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^(bdd_utilsLib.make_bv 3 4))”;
+val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^(bdd_utilsLib.make_bv 8 4))”;
 
 
-val arith_policy2 =   “[^arith_policy_rule2;
-                       ^arith_policy_default]:single_rule list”;
 
-val policy_me2 =   “[("x", ^is_ge_than_30)]”;
+val policy_me =   “[("x", ^is_high_priority);
+                    ("y", ^is_medium_priority);
+                    ("z1", ^is_small_packet1);
+                    ("z2", ^is_small_packet2);
+                    ("w", ^is_young_packet);
+                    ("q", ^is_control_type);
+                    ("r", ^is_data_type)]”;
 
+val policy_full_order = “[("a",["x";"y"]);
+                          ("b",["z1";"z2"]);
+                          ("c",["w"]);
+                          ("d",["q";"r"])]”;
 
-val final_thm_res2 =
-fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy2, policy_me2, test_pd_type1, policy_full_order1, policy_order1);
+val policy_order = “["x";"y";"z1";"z2";"w";"q";"r"]”;
 
-(***********************)
+(* Rule 1: High priority small control packets - expedited forwarding *)
+val arith_policy_rule1 = “(arith_and (arith_a ^is_high_priority) 
+                                     (arith_and (arith_a ^is_small_packet1) (arith_a ^is_control_type)),
+                           action ("fwd_priority",[1; 255])):single_rule”;
 
-val arith_policy_rule3 = “(arith_or (arith_a ^is_ge_than_10) (arith_a ^is_le_than_9),
-                           action ("reject",[])):single_rule”;
+(* Rule 2: High priority data packets *)
+val arith_policy_rule2 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_data_type),
+                           action ("fwd",[1])):single_rule”;
 
+(* Rule 3: Medium priority young packets *)
+val arith_policy_rule3 = “(arith_and (arith_a ^is_medium_priority) (arith_a ^is_young_packet),
+                           action ("fwd",[2])):single_rule”;
 
+(* Rule 3: Medium priority young packets *)
+val arith_policy_rule4 = “((arith_a ^is_small_packet2),
+                           action ("fwd",[3])):single_rule”;
 
-val arith_policy3 =   “[^arith_policy_default;
-                       ^arith_policy_rule3]:single_rule list”;
-
-val policy_me3 =   “[("x", ^is_ge_than_10);("y", ^is_le_than_9)]”;
-
-val policy_full_order3 = “[("a",["x";"y"])]”;
-
-val policy_order3 = “["x";"y"]”;
 
+(* Default forward rule *)
+val arith_policy_rule_default = “(arith_a a_True,
+                           action ("fwd",[5])):single_rule”;
 
-val final_thm_res3 =
-fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy3, policy_me3, test_pd_type1, policy_full_order3, policy_order3);
+val arith_policy =   “[^arith_policy_rule1;
+                       ^arith_policy_rule2;
+                       ^arith_policy_rule3;
+                       ^arith_policy_rule4;
+                       ^arith_policy_rule_default]:single_rule list”;
 
 
 
+val final_thm_res =
+fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/policy_test_cases/auto_test3Script.sml b/hol/policy_to_table/policy_test_cases/auto_test3Script.sml
@@ -0,0 +1,97 @@
+open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+open policy_arith_to_varTheory;
+
+open bdd_utilsLib;
+open fwd_proofLib;   
+
+
+val _ = new_theory "auto_test3";
+
+val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
+ 
+val test_pd_type = “[("ip", type_record [("priority", type_length 3);
+                                         ("size", type_length 16);
+                                         ("age", type_length 8);
+                                         ("type", type_length 4)])]”;
+
+val is_high_priority = “(arithm_le (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 2 3))”;
+val is_medium_priority = “(arithm_ge (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 4 3))”;
+
+val is_size_packet1 = “(arithm_ge (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 30000 16))”;
+val is_size_packet2 = “(arithm_ge (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 27000 16))”;
+val is_size_packet3 = “(arithm_ge (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 25000 16))”;
+val is_size_packet4 = “(arithm_ge (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 23000 16))”;
+
+
+val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^(bdd_utilsLib.make_bv 200 8))”;
+
+val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^(bdd_utilsLib.make_bv 3 4))”;
+val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^(bdd_utilsLib.make_bv 8 4))”;
+
+
+
+val policy_me =   “[("x1", ^is_high_priority);
+                    ("x2", ^is_medium_priority);
+
+                    ("z1", ^is_size_packet1);
+                    ("z2", ^is_size_packet2);
+                    ("z3", ^is_size_packet3);
+                    ("z4", ^is_size_packet4);
+
+                    ("q1", ^is_control_type);
+                    ("q2", ^is_data_type)]”;
+
+val policy_full_order = “[("a",["x1";"x2"]);
+                          ("b",["z1";"z2";"z3";"z4"]);
+                          ("d",["q1";"q2"])]”;
+
+val policy_order = “["x1";"x2";"z1";"z2";"z3";"z4";"q1";"q2"]”;
+
+val arith_policy_rule1 = “(arith_and (arith_a ^is_high_priority) 
+                                     (arith_and (arith_a ^is_size_packet1) (arith_a ^is_control_type)),
+                           action ("fwd_priority",[1; 255])):single_rule”;
+
+val arith_policy_rule2 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_size_packet2),
+                           action ("fwd",[1])):single_rule”;
+
+val arith_policy_rule3 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_size_packet3),
+                           action ("fwd",[2])):single_rule”;
+
+val arith_policy_rule4 = “(arith_and (arith_a ^is_high_priority) (arith_a ^is_size_packet4),
+                           action ("fwd",[3])):single_rule”;
+
+val arith_policy_rule5 = “(arith_and (arith_a ^is_medium_priority) 
+                                     (arith_and (arith_a ^is_size_packet1) (arith_a ^is_data_type)),
+                           action ("fwd_priority",[1; 4])):single_rule”;
+
+
+
+
+(* Default forward rule *)
+val arith_policy_rule_default = “(arith_a a_True,
+                           action ("fwd",[5])):single_rule”;
+
+val arith_policy =   “[^arith_policy_rule1;
+                       ^arith_policy_rule2;
+                       ^arith_policy_rule3;
+                       ^arith_policy_rule4;
+                       ^arith_policy_rule5;
+                       ^arith_policy_rule_default]:single_rule list”;
+
+
+
+val final_thm_res =
+fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+
+
+
+
+                      
+val _ = export_theory ();
+
+
+
+
+
+             
diff --git a/hol/policy_to_table/policy_test_cases/auto_test_rndScript.sml b/hol/policy_to_table/policy_test_cases/auto_test_rndScript.sml
