diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 71 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 21 |
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. |