summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/coq/Primitives.v14
-rw-r--r--backends/fstar/Primitives.fst47
-rw-r--r--backends/hol4/primitivesScript.sml26
-rw-r--r--backends/hol4/primitivesTheory.sig120
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean48
5 files changed, 221 insertions, 34 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
/// The scalar types
type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8 : eqtype = scalar I8
+type i16 : eqtype = scalar I16
+type i32 : eqtype = scalar I32
+type i64 : eqtype = scalar I64
+type i128 : eqtype = scalar I128
type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8 : eqtype = scalar U8
+type u16 : eqtype = scalar U16
+type u32 : eqtype = scalar U32
+type u64 : eqtype = scalar U64
+type u128 : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min : i8 = i8_min
+let core_i8_max : i8 = i8_max
+let core_i16_min : i16 = i16_min
+let core_i16_max : i16 = i16_max
+let core_i32_min : i32 = i32_min
+let core_i32_max : i32 = i32_max
+let core_i64_min : i64 = i64_min
+let core_i64_max : i64 = i64_max
+let core_i128_min : i128 = i128_min
+let core_i128_max : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min : u8 = u8_min
+let core_u8_max : u8 = u8_max
+let core_u16_min : u16 = u16_min
+let core_u16_max : u16 = u16_max
+let core_u32_min : u32 = u32_min
+let core_u32_max : u32 = u32_max
+let core_u64_min : u64 = u64_min
+let core_u64_max : u64 = u64_max
+let core_u128_min : u128 = u128_min
+let core_u128_max : u128 = u128_max
/// Negation
let isize_neg = scalar_neg #Isize
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 82da4de9..916988be 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -555,6 +555,32 @@ Proof
QED
val _ = evalLib.add_unfold_thm "mk_isize_unfold"
+(** Constants *)
+val core_i8_min_def = Define ‘core_i8_min = int_to_i8 i8_min’
+val core_i8_max_def = Define ‘core_i8_max = int_to_i8 i8_max’
+val core_i16_min_def = Define ‘core_i16_min = int_to_i16 i16_min’
+val core_i16_max_def = Define ‘core_i16_max = int_to_i16 i16_max’
+val core_i32_min_def = Define ‘core_i32_min = int_to_i32 i32_min’
+val core_i32_max_def = Define ‘core_i32_max = int_to_i32 i32_max’
+val core_i64_min_def = Define ‘core_i64_min = int_to_i64 i64_min’
+val core_i64_max_def = Define ‘core_i64_max = int_to_i64 i64_max’
+val core_i128_min_def = Define ‘core_i128_min = int_to_i128 i128_min’
+val core_i128_max_def = Define ‘core_i128_max = int_to_i128 i128_max’
+val core_isize_min_def = Define ‘core_isize_min = int_to_isize isize_min’
+val core_isize_max_def = Define ‘core_isize_max = int_to_isize isize_max’
+val core_u8_min_def = Define ‘core_u8_min = int_to_u8 0’
+val core_u8_max_def = Define ‘core_u8_max = int_to_u8 u8_max’
+val core_u16_min_def = Define ‘core_u16_min = int_to_u16 0’
+val core_u16_max_def = Define ‘core_u16_max = int_to_u16 u16_max’
+val core_u32_min_def = Define ‘core_u32_min = int_to_u32 0’
+val core_u32_max_def = Define ‘core_u32_max = int_to_u32 u32_max’
+val core_u64_min_def = Define ‘core_u64_min = int_to_u64 0’
+val core_u64_max_def = Define ‘core_u64_max = int_to_u64 u64_max’
+val core_u128_min_def = Define ‘core_u128_min = int_to_u128 0’
+val core_u128_max_def = Define ‘core_u128_max = int_to_u128 u128_max’
+val core_usize_min_def = Define ‘core_usize_min = int_to_usize 0’
+val core_usize_max_def = Define ‘core_usize_max = int_to_usize usize_max’
+
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))’
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 6660b02d..4ae6bb3e 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -46,6 +46,30 @@ sig
(* Definitions *)
val bind_def : thm
+ val core_i128_max_def : thm
+ val core_i128_min_def : thm
+ val core_i16_max_def : thm
+ val core_i16_min_def : thm
+ val core_i32_max_def : thm
+ val core_i32_min_def : thm
+ val core_i64_max_def : thm
+ val core_i64_min_def : thm
+ val core_i8_max_def : thm
+ val core_i8_min_def : thm
+ val core_isize_max_def : thm
+ val core_isize_min_def : thm
+ val core_u128_max_def : thm
+ val core_u128_min_def : thm
+ val core_u16_max_def : thm
+ val core_u16_min_def : thm
+ val core_u32_max_def : thm
+ val core_u32_min_def : thm
+ val core_u64_max_def : thm
+ val core_u64_min_def : thm
+ val core_u8_max_def : thm
+ val core_u8_min_def : thm
+ val core_usize_max_def : thm
+ val core_usize_min_def : thm
val error_BIJ : thm
val error_CASE : thm
val error_TY_DEF : thm
@@ -566,6 +590,102 @@ sig
monad_bind x f =
case x of Return y => f y | Fail e => Fail e | Diverge => Diverge
+ [core_i128_max_def] Definition
+
+ ⊢ core_i128_max = int_to_i128 i128_max
+
+ [core_i128_min_def] Definition
+
+ ⊢ core_i128_min = int_to_i128 i128_min
+
+ [core_i16_max_def] Definition
+
+ ⊢ core_i16_max = int_to_i16 i16_max
+
+ [core_i16_min_def] Definition
+
+ ⊢ core_i16_min = int_to_i16 i16_min
+
+ [core_i32_max_def] Definition
+
+ ⊢ core_i32_max = int_to_i32 i32_max
+
+ [core_i32_min_def] Definition
+
+ ⊢ core_i32_min = int_to_i32 i32_min
+
+ [core_i64_max_def] Definition
+
+ ⊢ core_i64_max = int_to_i64 i64_max
+
+ [core_i64_min_def] Definition
+
+ ⊢ core_i64_min = int_to_i64 i64_min
+
+ [core_i8_max_def] Definition
+
+ ⊢ core_i8_max = int_to_i8 i8_max
+
+ [core_i8_min_def] Definition
+
+ ⊢ core_i8_min = int_to_i8 i8_min
+
+ [core_isize_max_def] Definition
+
+ ⊢ core_isize_max = int_to_isize isize_max
+
+ [core_isize_min_def] Definition
+
+ ⊢ core_isize_min = int_to_isize isize_min
+
+ [core_u128_max_def] Definition
+
+ ⊢ core_u128_max = int_to_u128 u128_max
+
+ [core_u128_min_def] Definition
+
+ ⊢ core_u128_min = int_to_u128 0
+
+ [core_u16_max_def] Definition
+
+ ⊢ core_u16_max = int_to_u16 u16_max
+
+ [core_u16_min_def] Definition
+
+ ⊢ core_u16_min = int_to_u16 0
+
+ [core_u32_max_def] Definition
+
+ ⊢ core_u32_max = int_to_u32 u32_max
+
+ [core_u32_min_def] Definition
+
+ ⊢ core_u32_min = int_to_u32 0
+
+ [core_u64_max_def] Definition
+
+ ⊢ core_u64_max = int_to_u64 u64_max
+
+ [core_u64_min_def] Definition
+
+ ⊢ core_u64_min = int_to_u64 0
+
+ [core_u8_max_def] Definition
+
+ ⊢ core_u8_max = int_to_u8 u8_max
+
+ [core_u8_min_def] Definition
+
+ ⊢ core_u8_min = int_to_u8 0
+
+ [core_usize_max_def] Definition
+
+ ⊢ core_usize_max = int_to_usize usize_max
+
+ [core_usize_min_def] Definition
+
+ ⊢ core_usize_min = int_to_usize 0
+
[error_BIJ] Definition
⊢ (∀a. num2error (error2num a) = a) ∧
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index fa5a63cd..6e7733a7 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -410,32 +410,32 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
@[reducible] def U128 := Scalar .U128
-- TODO: reducible?
-@[reducible] def isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
-@[reducible] def isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
-@[reducible] def i8_min : I8 := Scalar.ofInt I8.min
-@[reducible] def i8_max : I8 := Scalar.ofInt I8.max
-@[reducible] def i16_min : I16 := Scalar.ofInt I16.min
-@[reducible] def i16_max : I16 := Scalar.ofInt I16.max
-@[reducible] def i32_min : I32 := Scalar.ofInt I32.min
-@[reducible] def i32_max : I32 := Scalar.ofInt I32.max
-@[reducible] def i64_min : I64 := Scalar.ofInt I64.min
-@[reducible] def i64_max : I64 := Scalar.ofInt I64.max
-@[reducible] def i128_min : I128 := Scalar.ofInt I128.min
-@[reducible] def i128_max : I128 := Scalar.ofInt I128.max
+@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min
+@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max
+@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min
+@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max
+@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min
+@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max
+@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min
+@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max
+@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min
+@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max
-- TODO: reducible?
-@[reducible] def usize_min : Usize := Scalar.ofInt Usize.min
-@[reducible] def usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
-@[reducible] def u8_min : U8 := Scalar.ofInt U8.min
-@[reducible] def u8_max : U8 := Scalar.ofInt U8.max
-@[reducible] def u16_min : U16 := Scalar.ofInt U16.min
-@[reducible] def u16_max : U16 := Scalar.ofInt U16.max
-@[reducible] def u32_min : U32 := Scalar.ofInt U32.min
-@[reducible] def u32_max : U32 := Scalar.ofInt U32.max
-@[reducible] def u64_min : U64 := Scalar.ofInt U64.min
-@[reducible] def u64_max : U64 := Scalar.ofInt U64.max
-@[reducible] def u128_min : U128 := Scalar.ofInt U128.min
-@[reducible] def u128_max : U128 := Scalar.ofInt U128.max
+@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min
+@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
+@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min
+@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max
+@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min
+@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max
+@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min
+@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max
+@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min
+@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max
+@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min
+@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max
-- TODO: below: not sure this is the best way.
-- Should we rather overload operations like +, -, etc.?
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 15:50:56 +0000