Fix some issues

7 files changed, 247 insertions, 49 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.?
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 74540787..8baa3c88 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -8,7 +8,6 @@ open Pure
 open PureUtils
 open TranslateCore
 open ExtractBase
-open ExtractAssumed
 open StringUtils
 open Config
 module F = Format
diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml
index bbcedb2b..7f094b24 100644
--- a/compiler/ExtractAssumed.ml
+++ b/compiler/ExtractAssumed.ml
@@ -1,8 +1,6 @@
 (** This file declares external identifiers that we catch to map them to
     definitions coming from the standard libraries in our backends. *)
 
-open Utils
-open StringUtils
 open Names
 
 type simple_name = string list [@@deriving show, ord]
@@ -30,18 +28,32 @@ module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
 
 let assumed_globals : (string * string) list =
   [
-    ("core::num::usize::MAX", "usize_max");
-    ("core::num::u8::MAX", "u8_max");
-    ("core::num::u16::MAX", "u16_max");
-    ("core::num::u32::MAX", "u32_max");
-    ("core::num::u64::MAX", "u64_max");
-    ("core::num::u128::MAX", "u128_max");
-    ("core::num::isize::MAX", "isize_max");
-    ("core::num::i8::MAX", "i8_max");
-    ("core::num::i16::MAX", "i16_max");
-    ("core::num::i32::MAX", "i32_max");
-    ("core::num::i64::MAX", "i64_max");
-    ("core::num::i128::MAX", "i128_max");
+    (* Min *)
+    ("core::num::usize::MIN", "core_usize_min");
+    ("core::num::u8::MIN", "core_u8_min");
+    ("core::num::u16::MIN", "core_u16_min");
+    ("core::num::u32::MIN", "core_u32_min");
+    ("core::num::u64::MIN", "core_u64_min");
+    ("core::num::u128::MIN", "core_u128_min");
+    ("core::num::isize::MIN", "core_isize_min");
+    ("core::num::i8::MIN", "core_i8_min");
+    ("core::num::i16::MIN", "core_i16_min");
+    ("core::num::i32::MIN", "core_i32_min");
+    ("core::num::i64::MIN", "core_i64_min");
+    ("core::num::i128::MIN", "core_i128_min");
+    (* Max *)
+    ("core::num::usize::MAX", "core_usize_max");
+    ("core::num::u8::MAX", "core_u8_max");
+    ("core::num::u16::MAX", "core_u16_max");
+    ("core::num::u32::MAX", "core_u32_max");
+    ("core::num::u64::MAX", "core_u64_max");
+    ("core::num::u128::MAX", "core_u128_max");
+    ("core::num::isize::MAX", "core_isize_max");
+    ("core::num::i8::MAX", "core_i8_max");
+    ("core::num::i16::MAX", "core_i16_max");
+    ("core::num::i32::MAX", "core_i32_max");
+    ("core::num::i64::MAX", "core_i64_max");
+    ("core::num::i128::MAX", "core_i128_max");
   ]
 
 let assumed_globals_map : string SimpleNameMap.t =