Update the definitions of mk_vec and vec_insert_back

2 files changed, 71 insertions, 21 deletions

diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 2a13e76d..6f54fbfc 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -96,6 +96,16 @@ val _ = new_constant ("u32_to_int",   “:u32 -> int”)
 val _ = new_constant ("u64_to_int",   “:u64 -> int”)
 val _ = new_constant ("u128_to_int",  “:u128 -> int”)
 
+(* The functions which convert integers to machine scalars don't fail.
+
+   If we were to write a model of those functions, we would return an arbitrary
+   element (or saturate) if the input integer is not in bounds.
+
+   This design choice makes it a lot easier to manipulate those functions.
+   Moreover, it allows to define and prove rewriting theorems and custom
+   unfolding theorems which are necessary to evaluate terms (when doing
+   unit tests). For instance, we can prove: “int_to_isize (isize_to_int i) = i”.
+ *)
 val _ = new_constant ("int_to_isize", “:int -> isize”)
 val _ = new_constant ("int_to_i8", “:int -> i8”)
 val _ = new_constant ("int_to_i16", “:int -> i16”)
@@ -388,7 +398,21 @@ val all_scalar_to_int_to_scalar_lemmas = [
   int_to_u128_u128_to_int,
   int_to_usize_usize_to_int
 ]
-val _ = evalLib.add_rewrites all_scalar_to_int_to_scalar_lemmas
+
+val _ = BasicProvers.export_rewrites [
+  "int_to_i8_i8_to_int",
+  "int_to_i16_i16_to_int",
+  "int_to_i32_i32_to_int",
+  "int_to_i64_i64_to_int",
+  "int_to_i128_i128_to_int",
+  "int_to_isize_isize_to_int",
+  "int_to_u8_u8_to_int",
+  "int_to_u16_u16_to_int",
+  "int_to_u32_u32_to_int",
+  "int_to_u64_u64_to_int",
+  "int_to_u128_u128_to_int",
+  "int_to_usize_usize_to_int"
+]
 
 (** Utilities to define the arithmetic operations *)
 val mk_isize_def = Define
@@ -1489,8 +1513,16 @@ End
 
 val _ = new_type ("vec", 1)
 val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
-(* TODO: we could also make ‘mk_vec’ return ‘'a vec’ (no result) *)
-val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”)
+
+(* Similarly to the "int_to_scalar" functions, the “mk_vec” function always
+   succeeds (it must however make sure vectors have a length which is at most
+   usize_max). In case the input list is too long, a model could return
+   an arbitrary vector (a truncated vector for instance).
+
+   Once again, this design choice makes it a lot easier to manipulate vectors,
+   and allows to define and prove simpler rewriting and unfolding theorems.
+ *)
+val _ = new_constant ("mk_vec", “:'a list -> 'a vec”)
 
 val vec_to_list_num_bounds =
   new_axiom ("vec_to_list_num_bounds",
@@ -1573,17 +1605,28 @@ val vec_index_def = Define ‘
     then Return (index (usize_to_int i) (vec_to_list v))
     else Fail Failure’
 
-val mk_vec_spec = new_axiom ("mk_vec_spec",
-  “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
+val mk_vec_axiom = new_axiom ("mk_vec_axiom",
+  “∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l”)
+
+(* A custom unfolding theorem for evaluation *)
+Theorem mk_vec_unfold:
+  ∀l. vec_to_list (mk_vec l) = if len l ≤ usize_max then l else vec_to_list (mk_vec l)
+Proof
+  metis_tac [mk_vec_axiom]
+QED
+val _ = evalLib.add_unfold_thm mk_vec_unfold
 
-(* Redefining ‘vec_insert_back’ *)
+(* Defining ‘vec_insert_back’ *)
 val vec_insert_back_def = Define ‘
-  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (usize_to_int i) x)’
+  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) =
+    if usize_to_int i < usize_to_int (vec_len v) then
+      Return (mk_vec (update (vec_to_list v) (usize_to_int i) x))
+    else Fail Failure’
 
 Theorem vec_insert_back_spec:
   ∀v i x.
     usize_to_int i < usize_to_int (vec_len v) ⇒
-    ∃nv. vec_insert_back v i x = Return nv ∧
+    ∃ nv. vec_insert_back v i x = Return nv ∧
     vec_len v = vec_len nv ∧
     vec_index i nv = Return x ∧
     (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
@@ -1591,17 +1634,15 @@ Theorem vec_insert_back_spec:
           vec_index j nv = vec_index j v)
 Proof
   rpt strip_tac >> fs [vec_insert_back_def] >>
-  (* TODO: improve this? *)
-  qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_spec >>
+  qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_axiom >>
   sg_dep_rewrite_all_tac update_len >> fs [] >>
-  qspec_assume ‘v’ vec_len_spec >>
-  rw [] >> gvs [] >>
+  qspec_assume ‘v’ vec_len_spec >> gvs [] >>
   fs [vec_len_def, vec_index_def] >>
   qspec_assume ‘i’ usize_to_int_bounds >>
   sg_dep_rewrite_all_tac usize_to_int_int_to_usize >- cooper_tac >> fs [] >>
-  sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >>
-  rw [] >>
-  irule index_update_same >> cooper_tac
+  rw []
+  >- (irule index_update_diff >> cooper_tac) >>
+  sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
 QED
 
 (* TODO: add theorems to the rewriting theorems
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 3e82565c..1908cbcb 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -28,7 +28,7 @@ sig
     val isize_bounds : thm
     val isize_to_int_bounds : thm
     val isize_to_int_int_to_isize : thm
-    val mk_vec_spec : thm
+    val mk_vec_axiom : thm
     val u128_to_int_bounds : thm
     val u128_to_int_int_to_u128 : thm
     val u16_to_int_bounds : thm
@@ -263,6 +263,7 @@ sig
     val isize_rem_eq : thm
     val isize_sub_eq : thm
     val isize_to_int_int_to_isize_unfold : thm
+    val mk_vec_unfold : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
     val num2error_error2num : thm
@@ -518,10 +519,10 @@ sig
       ⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧
             LENGTH (vec_to_list v) ≤ Num usize_max
    
-   [mk_vec_spec]  Axiom
+   [mk_vec_axiom]  Axiom
       
-      [oracles: ] [axioms: mk_vec_spec] []
-      ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
+      [oracles: ] [axioms: mk_vec_axiom] []
+      ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l
    
    [bind_def]  Definition
       
@@ -1282,7 +1283,9 @@ sig
       
       ⊢ ∀v i x.
           vec_insert_back v i x =
-          mk_vec (update (vec_to_list v) (usize_to_int i) x)
+          if usize_to_int i < usize_to_int (vec_len v) then
+            Return (mk_vec (update (vec_to_list v) (usize_to_int i) x))
+          else Fail Failure
    
    [vec_len_def]  Definition
       
@@ -1784,6 +1787,12 @@ sig
             if i16_min ≤ n ∧ n ≤ i16_max then n
             else isize_to_int (int_to_isize n)
    
+   [mk_vec_unfold]  Theorem
+      
+      [oracles: DISK_THM] [axioms: mk_vec_axiom] []
+      ⊢ ∀l. vec_to_list (mk_vec l) =
+            if len l ≤ usize_max then l else vec_to_list (mk_vec l)
+   
    [num2error_11]  Theorem
       
       ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
@@ -2198,7 +2207,7 @@ sig
       
       [oracles: DISK_THM]
       [axioms: vec_to_list_num_bounds, usize_bounds,
-       usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_spec] []
+       usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] []
       ⊢ ∀v i x.
           usize_to_int i < usize_to_int (vec_len v) ⇒
           ∃nv.