summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/hol4/primitivesScript.sml119
-rw-r--r--backends/hol4/primitivesTheory.sig99
2 files changed, 216 insertions, 2 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index e10ce7e5..4a1f5fdd 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -504,6 +504,33 @@ val all_mk_int_defs = [
mk_u128_def
]
+(* Unfolding theorems for “mk_usize” and “mk_isize”: we need specific unfolding
+ theorems because the isize/usize bounds are opaque, and may make the evaluation
+ get stuck in the unit tests *)
+Theorem mk_usize_unfold:
+ ∀ n. mk_usize n =
+ if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then Return (int_to_usize n)
+ else Fail Failure
+Proof
+ rw [mk_usize_def] >> fs [] >>
+ assume_tac usize_bounds >>
+ int_tac
+QED
+val _ = evalLib.add_unfold_thm "mk_usize_unfold"
+
+Theorem mk_isize_unfold:
+ ∀ n. mk_isize n =
+ if (i16_min ≤ n ∨ isize_min ≤ n) ∧
+ (n ≤ i16_max ∨ n ≤ isize_max)
+ then Return (int_to_isize n)
+ else Fail Failure
+Proof
+ rw [mk_isize_def] >> fs [] >>
+ assume_tac isize_bounds >>
+ int_tac
+QED
+val _ = evalLib.add_unfold_thm "mk_isize_unfold"
+
val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’
val i8_neg_def = Define ‘i8_neg x = mk_i8 (- (i8_to_int x))’
val i16_neg_def = Define ‘i16_neg x = mk_i16 (- (i16_to_int x))’
@@ -1521,6 +1548,98 @@ Definition isize_ge_def:
End
+(* Equality theorems for the comparisons between integers - used by evalLib *)
+
+val prove_scalar_eq_equiv_tac = metis_tac all_scalar_to_int_to_scalar_lemmas
+
+Theorem isize_eq_equiv:
+ ∀x y. (x = y) = (isize_to_int x = isize_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem i8_eq_equiv:
+ ∀x y. (x = y) = (i8_to_int x = i8_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem i16_eq_equiv:
+ ∀x y. (x = y) = (i16_to_int x = i16_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem i32_eq_equiv:
+ ∀x y. (x = y) = (i32_to_int x = i32_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem i64_eq_equiv:
+ ∀x y. (x = y) = (i64_to_int x = i64_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem i128_eq_equiv:
+ ∀x y. (x = y) = (i128_to_int x = i128_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem usize_eq_equiv:
+ ∀x y. (x = y) = (usize_to_int x = usize_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem u8_eq_equiv:
+ ∀x y. (x = y) = (u8_to_int x = u8_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem u16_eq_equiv:
+ ∀x y. (x = y) = (u16_to_int x = u16_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem u32_eq_equiv:
+ ∀x y. (x = y) = (u32_to_int x = u32_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem u64_eq_equiv:
+ ∀x y. (x = y) = (u64_to_int x = u64_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+Theorem u128_eq_equiv:
+ ∀x y. (x = y) = (u128_to_int x = u128_to_int y)
+Proof
+ prove_scalar_eq_equiv_tac
+QED
+
+(* Remark.: don't move this up, it will break some proofs *)
+val _ = BasicProvers.export_rewrites [
+ "isize_eq_equiv",
+ "i8_eq_equiv",
+ "i16_eq_equiv",
+ "i32_eq_equiv",
+ "i64_eq_equiv",
+ "i128_eq_equiv",
+ "usize_eq_equiv",
+ "u8_eq_equiv",
+ "u16_eq_equiv",
+ "u32_eq_equiv",
+ "u64_eq_equiv",
+ "u128_eq_equiv"
+]
+
(***
* Vectors
*)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 1908cbcb..45caf234 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -221,6 +221,7 @@ sig
val error_nchotomy : thm
val i128_add_eq : thm
val i128_div_eq : thm
+ val i128_eq_equiv : thm
val i128_mul_eq : thm
val i128_neg_eq : thm
val i128_rem_eq : thm
@@ -228,6 +229,7 @@ sig
val i128_to_int_int_to_i128_unfold : thm
val i16_add_eq : thm
val i16_div_eq : thm
+ val i16_eq_equiv : thm
val i16_mul_eq : thm
val i16_neg_eq : thm
val i16_rem_eq : thm
@@ -235,6 +237,7 @@ sig
val i16_to_int_int_to_i16_unfold : thm
val i32_add_eq : thm
val i32_div_eq : thm
+ val i32_eq_equiv : thm
val i32_mul_eq : thm
val i32_neg_eq : thm
val i32_rem_eq : thm
@@ -242,6 +245,7 @@ sig
val i32_to_int_int_to_i32_unfold : thm
val i64_add_eq : thm
val i64_div_eq : thm
+ val i64_eq_equiv : thm
val i64_mul_eq : thm
val i64_neg_eq : thm
val i64_rem_eq : thm
@@ -249,6 +253,7 @@ sig
val i64_to_int_int_to_i64_unfold : thm
val i8_add_eq : thm
val i8_div_eq : thm
+ val i8_eq_equiv : thm
val i8_mul_eq : thm
val i8_neg_eq : thm
val i8_rem_eq : thm
@@ -258,11 +263,14 @@ sig
val index_update_same : thm
val isize_add_eq : thm
val isize_div_eq : thm
+ val isize_eq_equiv : thm
val isize_mul_eq : thm
val isize_neg_eq : thm
val isize_rem_eq : thm
val isize_sub_eq : thm
val isize_to_int_int_to_isize_unfold : thm
+ val mk_isize_unfold : thm
+ val mk_usize_unfold : thm
val mk_vec_unfold : thm
val num2error_11 : thm
val num2error_ONTO : thm
@@ -277,30 +285,35 @@ sig
val result_nchotomy : thm
val u128_add_eq : thm
val u128_div_eq : thm
+ val u128_eq_equiv : thm
val u128_mul_eq : thm
val u128_rem_eq : thm
val u128_sub_eq : thm
val u128_to_int_int_to_u128_unfold : thm
val u16_add_eq : thm
val u16_div_eq : thm
+ val u16_eq_equiv : thm
val u16_mul_eq : thm
val u16_rem_eq : thm
val u16_sub_eq : thm
val u16_to_int_int_to_u16_unfold : thm
val u32_add_eq : thm
val u32_div_eq : thm
+ val u32_eq_equiv : thm
val u32_mul_eq : thm
val u32_rem_eq : thm
val u32_sub_eq : thm
val u32_to_int_int_to_u32_unfold : thm
val u64_add_eq : thm
val u64_div_eq : thm
+ val u64_eq_equiv : thm
val u64_mul_eq : thm
val u64_rem_eq : thm
val u64_sub_eq : thm
val u64_to_int_int_to_u64_unfold : thm
val u8_add_eq : thm
val u8_div_eq : thm
+ val u8_eq_equiv : thm
val u8_mul_eq : thm
val u8_rem_eq : thm
val u8_sub_eq : thm
@@ -309,6 +322,7 @@ sig
val update_spec : thm
val usize_add_eq : thm
val usize_div_eq : thm
+ val usize_eq_equiv : thm
val usize_mul_eq : thm
val usize_rem_eq : thm
val usize_sub_eq : thm
@@ -1366,6 +1380,11 @@ sig
∃z. i128_div x y = Return z ∧
i128_to_int z = i128_to_int x / i128_to_int y
+ [i128_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_i128_i128_to_int] []
+ ⊢ ∀x y. x = y ⇔ i128_to_int x = i128_to_int y
+
[i128_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1436,6 +1455,11 @@ sig
∃z. i16_div x y = Return z ∧
i16_to_int z = i16_to_int x / i16_to_int y
+ [i16_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_i16_i16_to_int] []
+ ⊢ ∀x y. x = y ⇔ i16_to_int x = i16_to_int y
+
[i16_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1505,6 +1529,11 @@ sig
∃z. i32_div x y = Return z ∧
i32_to_int z = i32_to_int x / i32_to_int y
+ [i32_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_i32_i32_to_int] []
+ ⊢ ∀x y. x = y ⇔ i32_to_int x = i32_to_int y
+
[i32_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1574,6 +1603,11 @@ sig
∃z. i64_div x y = Return z ∧
i64_to_int z = i64_to_int x / i64_to_int y
+ [i64_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_i64_i64_to_int] []
+ ⊢ ∀x y. x = y ⇔ i64_to_int x = i64_to_int y
+
[i64_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1643,6 +1677,11 @@ sig
∃z. i8_div x y = Return z ∧
i8_to_int z = i8_to_int x / i8_to_int y
+ [i8_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_i8_i8_to_int] []
+ ⊢ ∀x y. x = y ⇔ i8_to_int x = i8_to_int y
+
[i8_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1730,6 +1769,11 @@ sig
∃z. isize_div x y = Return z ∧
isize_to_int z = isize_to_int x / isize_to_int y
+ [isize_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_isize_isize_to_int] []
+ ⊢ ∀x y. x = y ⇔ isize_to_int x = isize_to_int y
+
[isize_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1787,6 +1831,24 @@ sig
if i16_min ≤ n ∧ n ≤ i16_max then n
else isize_to_int (int_to_isize n)
+ [mk_isize_unfold] Theorem
+
+ [oracles: DISK_THM] [axioms: isize_bounds] []
+ ⊢ ∀n. mk_isize n =
+ if
+ (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max)
+ then
+ Return (int_to_isize n)
+ else Fail Failure
+
+ [mk_usize_unfold] Theorem
+
+ [oracles: DISK_THM] [axioms: usize_bounds] []
+ ⊢ ∀n. mk_usize n =
+ if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then
+ Return (int_to_usize n)
+ else Fail Failure
+
[mk_vec_unfold] Theorem
[oracles: DISK_THM] [axioms: mk_vec_axiom] []
@@ -1866,6 +1928,11 @@ sig
∃z. u128_div x y = Return z ∧
u128_to_int z = u128_to_int x / u128_to_int y
+ [u128_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_u128_u128_to_int] []
+ ⊢ ∀x y. x = y ⇔ u128_to_int x = u128_to_int y
+
[u128_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1923,6 +1990,11 @@ sig
∃z. u16_div x y = Return z ∧
u16_to_int z = u16_to_int x / u16_to_int y
+ [u16_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_u16_u16_to_int] []
+ ⊢ ∀x y. x = y ⇔ u16_to_int x = u16_to_int y
+
[u16_mul_eq] Theorem
[oracles: DISK_THM]
@@ -1980,6 +2052,11 @@ sig
∃z. u32_div x y = Return z ∧
u32_to_int z = u32_to_int x / u32_to_int y
+ [u32_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_u32_u32_to_int] []
+ ⊢ ∀x y. x = y ⇔ u32_to_int x = u32_to_int y
+
[u32_mul_eq] Theorem
[oracles: DISK_THM]
@@ -2037,6 +2114,11 @@ sig
∃z. u64_div x y = Return z ∧
u64_to_int z = u64_to_int x / u64_to_int y
+ [u64_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_u64_u64_to_int] []
+ ⊢ ∀x y. x = y ⇔ u64_to_int x = u64_to_int y
+
[u64_mul_eq] Theorem
[oracles: DISK_THM]
@@ -2094,6 +2176,11 @@ sig
∃z. u8_div x y = Return z ∧
u8_to_int z = u8_to_int x / u8_to_int y
+ [u8_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_u8_u8_to_int] []
+ ⊢ ∀x y. x = y ⇔ u8_to_int x = u8_to_int y
+
[u8_mul_eq] Theorem
[oracles: DISK_THM]
@@ -2164,6 +2251,11 @@ sig
∃z. usize_div x y = Return z ∧
usize_to_int z = usize_to_int x / usize_to_int y
+ [usize_eq_equiv] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+ ⊢ ∀x y. x = y ⇔ usize_to_int x = usize_to_int y
+
[usize_mul_eq] Theorem
[oracles: DISK_THM]
@@ -2207,7 +2299,8 @@ sig
[oracles: DISK_THM]
[axioms: vec_to_list_num_bounds, usize_bounds,
- usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] []
+ int_to_usize_usize_to_int, usize_to_int_bounds,
+ usize_to_int_int_to_usize, mk_vec_axiom] []
⊢ ∀v i x.
usize_to_int i < usize_to_int (vec_len v) ⇒
∃nv.
@@ -2219,7 +2312,9 @@ sig
[vec_len_spec] Theorem
- [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
+ [oracles: DISK_THM]
+ [axioms: int_to_usize_usize_to_int, usize_bounds,
+ vec_to_list_num_bounds] []
⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max