From 1181aecddbcb3232c21b191fbde59c2e9596846a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 16:02:43 +0200 Subject: Fix some issues --- backends/coq/Primitives.v | 14 ++++ backends/fstar/Primitives.fst | 47 +++++++++--- backends/hol4/primitivesScript.sml | 26 +++++++ backends/hol4/primitivesTheory.sig | 120 ++++++++++++++++++++++++++++++ backends/lean/Base/Primitives/Scalar.lean | 48 ++++++------ 5 files changed, 221 insertions(+), 34 deletions(-) (limited to 'backends') 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.? -- cgit v1.2.3