Merge pull request #50 from kth-step/dev_polyml

Update to Poly/ML 5.9.2 and trindemossen-2

Author: AnoudAlshnakat

.github/workflows/build.yaml

@@ -15,8 +15,8 @@ jobs:
 
     strategy:
       matrix:
-        polyml: ['5.7.1', '5.9.1']
-        hol4: ['trindemossen-1']
+        polyml: ['5.7.1', '5.9.2']
+        hol4: ['trindemossen-2']
 
     env:
       CACHE_DIR: /home/runner/cache

INSTALL.md

@@ -34,21 +34,21 @@ First, navigate to the directory where you want to put the source code of Poly/M
 
 		sudo apt-get install build-essential git
 
-2. Install Poly/ML 5.9.1
+2. Install Poly/ML 5.9.2
 
 		git clone https://github.com/polyml/polyml.git
 		cd polyml
-		git checkout v5.9.1
+		git checkout v5.9.2
 		./configure --prefix=/usr
 		make
 		sudo make install
 		cd ..
 
-3. Install HOL4 Trindemossen-1
+3. Install HOL4 Trindemossen-2
 
 		git clone https://github.com/HOL-Theorem-Prover/HOL.git
 		cd HOL
-		git checkout trindemossen-1
+		git checkout trindemossen-2
 		poly < tools/smart-configure.sml
 		bin/build
 		cd ..
@@ -124,4 +124,4 @@ The same tools used to edit HOL4 theories and run the HOL4 REPL can also be used
 
 The `scripts` directory contains installation scripts. These may be run when installing HOL4P4 e.g. on a fresh virtual machine by
 
-	scripts/install.sh
+	scripts/install.sh

hol/ottLib.sml

@@ -76,15 +76,15 @@ in
   HO_MATCH_MP_TAC list_induction THEN STRIP_TAC THENL 
   [ALL_TAC, STRIP_TAC THEN STRIP_TAC THEN PAIR_CASES_TAC] THEN
   SRW_TAC [] [] THEN 
-  CONV_TAC TotalDefn.TC_SIMP_CONV THEN 
+  TotalDefn.TC_SIMP_TAC std_ss [] THEN 
   SRW_TAC [] [] THEN
   RES_TAC THEN
   DECIDE_TAC THEN NO_TAC
 end;
 
 fun ONE_TERM_TAC measure =
   WF_REL_TAC `^measure` THEN
-  CONV_TAC TotalDefn.TC_SIMP_CONV THEN  
+  TotalDefn.TC_SIMP_TAC std_ss [] THEN  
   SRW_TAC [] [] THEN
   APPLY_FILTER_SIZE THEN 
   TRY (ASSUM_LIST (MAP_FIRST MEM_IND_TAC o List.filter is_mem o List.map concl))

hol/p4_auxScript.sml

@@ -7,7 +7,7 @@ open pairTheory optionTheory arithmeticTheory;
 open p4Theory;
 
 (* OPTION_BIND as infix *)
-Definition app_opt_def:
+Definition app_opt_def[simp]:
  $>>= x_opt f =
   OPTION_BIND x_opt f
 End
@@ -1335,7 +1335,6 @@ Theorem  EL_relation_to_INDEX_lesseq:
             i <= LENGTH l ==>
             m = n 
 Proof
-
 Induct >>
 REPEAT STRIP_TAC >>
 fs[INDEX_FIND_def] >>
@@ -1464,32 +1463,23 @@ Theorem index_find_concat1:
 ! l1 l2 n P.
 INDEX_FIND 0 P l1 = NONE  /\
 INDEX_FIND 0 P (l2 ⧺ l1) = SOME n ==>
-INDEX_FIND 0 P (l2) = SOME n 
+INDEX_FIND 0 P (l2) = SOME n
 Proof
 Induct_on `l1` >>
 Induct_on `l2` >>
-fs[INDEX_FIND_def] >>
-REPEAT STRIP_TAC >>
-CASE_TAC >| [
- rfs[]
- ,
- Cases_on `P h'` >| [
-  gvs[]
-  ,
-  gvs[] >>
-
-  ASSUME_TAC P_hold_on_next>> 
-  FIRST_X_ASSUM
-  (STRIP_ASSUME_TAC o (Q.SPECL [`0`,`(l2 ⧺ h'::l1)`,`P`,`n`])) >>
-  gvs[GSYM ADD1] >> 
-  RES_TAC >>
-  gvs[] >>
-
-  IMP_RES_TAC P_implies_next >>
-  Cases_on `n` >>
-  fs[]
-  ]
- ]
+gs[INDEX_FIND_def, AllCaseEqs()] >>
+REPEAT STRIP_TAC >> (
+ gs[]
+) >>
+ASSUME_TAC P_hold_on_next >> 
+FIRST_X_ASSUM
+ (STRIP_ASSUME_TAC o (Q.SPECL [`0`,`(l2 ⧺ h'::l1)`,`P`,`n`])) >>
+gvs[GSYM ADD1] >> 
+RES_TAC >>
+gvs[] >>
+IMP_RES_TAC P_implies_next >>
+Cases_on `n` >>
+fs[]
 QED
 
 
@@ -1835,17 +1825,16 @@ QED
 Theorem index_find_not_mem:
  ! l P e n. (INDEX_FIND n P l = NONE) /\ P e ==> ~ MEM e l 
 Proof
-
 Induct >>
 fs[INDEX_FIND_def] >>
 REPEAT GEN_TAC >>
-CASE_TAC >>
+gs[AllCaseEqs()] >>
 STRIP_TAC >>
-FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL
-[`P`, `e` , `SUC n`])) >>
+FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [`P`, `e` , `SUC n`])) >>
 IMP_RES_TAC P_NONE_hold2 >>
-Cases_on `e=h` >>
-fs[]
+Cases_on `e=h` >> (
+ fs[]
+)
 QED
 
 
@@ -2573,8 +2562,6 @@ Definition deparameterise_tau_def:
   deparameterise_tau p_tau >>=
   \tau. deparameterise_x_taus t >>=
   \tau_l. SOME ((name, tau)::tau_l))
-Termination
-WF_REL_TAC `measure ( \ t. case t of | (INL p_tau) => p_tau_size p_tau | (INR p_tau_list) => p_tau1_size p_tau_list)`
 End
 
 Definition deparameterise_taus_def:
@@ -2594,8 +2581,6 @@ Definition parameterise_tau_def:
   | tau_ext => p_tau_ext "") /\
 (parameterise_x_taus [] = []) /\
 (parameterise_x_taus ((name, tau)::t) = ((name, parameterise_tau tau)::(parameterise_x_taus t)))
-Termination
-WF_REL_TAC `measure ( \ t. case t of | (INL tau) => tau_size tau | (INR tau_list) => tau1_size tau_list)`
 End
 
 Definition parameterise_taus_def:

hol/p4_coreScript.sml

@@ -183,8 +183,6 @@ Definition set_fields_def:
       | NONE => NONE)
     | NONE => NONE)
   | _ => NONE)
-Termination
-WF_REL_TAC `measure ( \ (t, acc, packet_in). v1_size t)`
 End
 
 Definition set_header_def:
@@ -389,8 +387,6 @@ Definition header_entries2v_def:
   | (v_header validity x_v_l) => header_entries2v x_v_l
   | _ => NONE
  )
-Termination
-WF_REL_TAC `measure ( \ t. case t of | (INL x_v_l) => v1_size x_v_l | (INR (x,v)) => v_size v)`
 End
 
 

hol/p4_e_progressScript.sml

@@ -629,7 +629,7 @@ IMP_RES_TAC bit_range >>
 fs[] >>
 
 fs[bitv_binop_def] >>
-RW.ONCE_RW_TAC [bitv_binop_inner_def] >>
+ONCE_REWRITE_TAC [bitv_binop_inner_def] >>
 fs[] >>
 srw_tac [numSimps.SUC_FILTER_ss][] 
 );
@@ -663,7 +663,7 @@ RES_TAC >>
 gvs[NOT_CLAUSES] >>
 
 fs[bitv_binop_def] >>
-RW.ONCE_RW_TAC [bitv_binop_inner_def] >>
+ONCE_REWRITE_TAC [bitv_binop_inner_def] >>
 fs[] >>
 srw_tac [numSimps.SUC_FILTER_ss][] 
 );
@@ -698,7 +698,7 @@ RES_TAC >>
 gvs[NOT_CLAUSES] >>
 
 fs[] >>
-RW.ONCE_RW_TAC [bitv_binpred_inner_def] >>
+ONCE_REWRITE_TAC [bitv_binpred_inner_def] >>
 fs[] >>
 srw_tac [numSimps.SUC_FILTER_ss][]
 );

hol/p4_from_json/parse_jsonScript.sml

@@ -159,14 +159,6 @@ Definition json_to_string_def:
   (mem_to_string n_obj = let (n, obj) = n_obj in
        [CONCAT ["\""; n; "\""]]
        ++ [":"] ++ json_to_string obj)
-Termination
-   WF_REL_TAC `measure (\x. case x of
-       | INL obj => json_size obj
-       | INR p => json2_size p)`
-  >> rw[]
-  >> imp_res_tac json_size_MEM1
-  >> imp_res_tac json_size_MEM2
-  >> fs[]
 End
 
 (* lexing *)
@@ -582,14 +574,6 @@ Definition json_to_tok_def:
   /\
   (mem_to_tok n_obj = let (n, obj) = n_obj in
         json_to_tok obj ++ [COLON;Str n])
-Termination
-   WF_REL_TAC `measure (\x. case x of
-       | INL obj => json_size obj
-       | INR p => json2_size p)`
-  >> rw[]
-  >> imp_res_tac json_size_MEM1
-  >> imp_res_tac json_size_MEM2
-  >> fs[]
 End
 
 (*

hol/p4_from_json/petr4_to_hol4p4Script.sml

@@ -393,33 +393,36 @@ Triviality json_parse_obj_size:
 Proof
 Induct_on ‘json_list’ >- (
  rpt strip_tac >>
- fs[json_parse_obj_def, json_dest_obj_def, app_opt_def] >>
+ gs[json_parse_obj_def, json_dest_obj_def] >>
  Cases_on ‘json’ >> (fs[json_size_def])
 ) >>
 rpt strip_tac >>
-fs[json_parse_obj_def, app_opt_def] >>
-Cases_on ‘json’ >> (fs[json_dest_obj_def]) >>
-rw[] >>
-Cases_on ‘str_list’ >> (fs[json_parse_obj'_def, json_size_def]) >>
-(Cases_on ‘l’ >> (fs[json_parse_obj'_def, json_size_def])) >>
-
-Cases_on ‘h''’ >> (fs[json_parse_obj'_def, json_size_def, app_opt_def]) >>
-Cases_on ‘json_parse_obj' t t'’ >> (fs[json_parse_obj'_def, json_size_def]) >>
-rw[] >>
-subgoal ‘(case (Object t') of
+gs[json_parse_obj_def] >>
+Cases_on ‘str_list’ >> (Cases_on ‘x’ >> (gs[json_parse_obj'_def, json_size_def])) >>
+PairCases_on ‘h''’ >>
+gvs[json_parse_obj'_def, json_size_def] >>
+Cases_on ‘json’ >> (gvs[json_dest_obj_def]) >>
+subgoal ‘?x. (case (Object t') of
                 Object obj => SOME obj
               | Array v8 => NONE
               | String v9 => NONE
               | Number v10 v11 v12 => NONE
               | Bool v13 => NONE
               | Null => NONE) =
              SOME t'’ >- (
- fs[]
+ gs[]
 ) >>
-subgoal ‘json3_size json_list < json_size (Object t')’ >- (
- metis_tac[]
-) >>
-fs[json_size_def]
+res_tac >>
+gs[]
+QED
+
+Theorem list_size_json3:
+!json_list.
+list_size json_size json_list = json3_size json_list
+Proof
+Induct >> (
+ gs[list_size_def, json_size_def]
+)
 QED
 
 (* Parses compile-time known constants, e.g. in bitstring widths *)
@@ -1227,24 +1230,24 @@ Definition petr4_parse_expression_gen_def:
   | SOME_msg (SetExp e) => get_error_msg "set expression in unsupported location: " h1
   | NONE_msg exp_msg => NONE_msg ("could not parse expression: "++exp_msg))
 Termination
-WF_REL_TAC `measure ( \ t. case t of
+WF_REL_TAC ‘measure ( \ t. case t of
                            | (INL (maps, json, p_tau_opt)) => json_size json
                            | (INR $ INL (maps, json_list)) => json_p_tau_opt_list_size json_list
-                           | (INR $ INR (maps, json_list)) => json_p_tau_opt_list_size json_list)` >>
-fs[json_p_tau_opt_list_size_def] >>
-rpt strip_tac >> (fs[json_size_def]) >- (
- subgoal ‘?l1 l2. UNZIP t = (l1, l2)’ >- (fs[UNZIP_MAP]) >>
- fs []
+                           | (INR $ INR (maps, json_list)) => json_p_tau_opt_list_size json_list)’ >>
+gs[json_p_tau_opt_list_size_def] >>
+rpt strip_tac >> (gs[json_size_def]) >- (
+ gs[UNZIP_MAP]
 ) >- (
- subgoal ‘?l1 l2. UNZIP t = (l1, l2)’ >- (fs[UNZIP_MAP]) >>
- fs []
+ gs[UNZIP_MAP]
 ) >- (
- subgoal ‘?l1 l2. UNZIP t = (l1, l2)’ >- (fs[UNZIP_MAP]) >>
- fs []
+ gs[UNZIP_MAP]
 ) >- (
- subgoal ‘LENGTH args = LENGTH p_1'5'’ >- (imp_res_tac find_fty_match_args_LENGTH >> fs[]) >>
- fs[listTheory.UNZIP_ZIP]
-)
+ gs[list_size_json3]
+) >- (
+ gs[list_size_json3]
+) >>
+‘LENGTH args = LENGTH p_1'5'’ by (imp_res_tac find_fty_match_args_LENGTH >> gs[]) >>
+gs[UNZIP_MAP, listTheory.MAP_ZIP, list_size_json3]
 End
 
 (* TODO: Baking this into the above messes up the termination proof... *)
@@ -2282,25 +2285,48 @@ Definition petr4_parse_stmts_def:
     | NONE_msg msg' => NONE_msg msg')
   | NONE_msg msg => NONE_msg msg)
 Termination
-WF_REL_TAC `measure ( \ t. case t of | (INL (maps, json_list)) => json3_size json_list | (INR (maps, json_list_list)) => SUM (MAP (\ el . json3_size el + 1) json_list_list))` >>
+WF_REL_TAC ‘measure ( \ t. case t of | (INL (maps, json_list)) => json3_size json_list | (INR (maps, json_list_list)) => SUM (MAP (\ el . json3_size el + 1) json_list_list))’ >>
 rpt strip_tac >> (fs[json_size_def]) >- (
- fs[json_parse_obj_def, json_dest_obj_def, app_opt_def] >>
+ fs[json_parse_obj_def, json_dest_obj_def] >>
  Cases_on ‘p_2'’ >> (fs[]) >>
  rw[] >>
- Cases_on ‘l’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
- Cases_on ‘h’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
- Cases_on ‘t'’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
- Cases_on ‘h’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
+ Cases_on ‘l’ >> (fs[json_parse_obj'_def]) >>
+ Cases_on ‘h’ >> (fs[json_parse_obj'_def]) >>
+ Cases_on ‘t'’ >> (fs[json_parse_obj'_def]) >>
+ Cases_on ‘h’ >> (fs[json_parse_obj'_def]) >>
  Cases_on ‘q' = "annotations"’ >> (fs[]) >>
- Cases_on ‘t''’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
- Cases_on ‘h’ >> (fs[json_parse_obj'_def, app_opt_def]) >>
+ Cases_on ‘t''’ >> (fs[json_parse_obj'_def]) >>
+ Cases_on ‘h’ >> (fs[json_parse_obj'_def]) >>
  Cases_on ‘q'' = "statements"’ >> (fs[]) >>
- Cases_on ‘json_parse_obj' [] t'’ >> (fs[json_size_def, app_opt_def])
+ Cases_on ‘json_parse_obj' [] t'’ >> (fs[json_size_def]) >>
+
+ gvs[char_size_def] >>
+ ‘json3_size t +
+   (json_size annotations +
+    (json_size p_2 +
+     (json_size r +
+      (list_size json_size stmts +
+       (list_size (pair_size (list_size char_size) json_size) t' + 57))))) =
+   json3_size stmts + 1 +
+   json3_size t +
+   (json_size annotations +
+    (json_size p_2 +
+     (json_size r +
+      (list_size (pair_size (list_size char_size) json_size) t' + 56))))’ suffices_by (
+  gs[]
+ ) >>
+ gvs[] >>
+ ‘list_size json_size stmts = json3_size stmts’ by (
+  Induct_on ‘stmts’ >> (
+   fs[json_size_def, list_size_def]
+  )
+ ) >>
+ gs[]
 ) >- (
  (* Switch case *)
  IMP_RES_TAC petr4_parse_switch_cases_size >>
  res_tac >>
- fs[json_size_def, app_opt_def]
+ fs[json_size_def]
 )
 End