Remove unused _underspec functions in signed integers

If these were exposed for Int{8,16,32,64}, they would be UB. Remove
them.

Author: mtzguido

ulib/FStar.Int.fst

@@ -34,24 +34,6 @@ let pow2_values x =
    | 64 -> assert_norm (pow2 64 == 18446744073709551616)
    | _  -> ()
 
-let incr_underspec #n a =
-  if a < max_int n then a + 1 else 0
-
-let decr_underspec #n a =
-  if a > min_int n then a - 1 else 0
-
-let add_underspec #n a b =
-  if fits (a+b) n then a + b else 0
-
-let sub_underspec #n a b =
-  if fits (a-b) n then a - b else 0
-
-let mul_underspec #n a b =
-  if fits (a*b) n then a * b else 0
-
-let div_underspec #n a b =
-  if fits (a /- b) n then a /- b else 0
-
 let div_size #n a b =
   FStar.Math.Lib.slash_decr_axiom (abs a) (abs b)
 

ulib/FStar.Int.fsti

@@ -88,14 +88,6 @@ let decr (#n:pos) (a:int_t n)
       (requires (b2t (a > min_int n))) (ensures (fun _ -> True))
   = a - 1
 
-val incr_underspec: #n:pos -> a:int_t n -> Pure (int_t n)
-  (requires (b2t (a < max_int n)))
-  (ensures (fun b -> a + 1 = b))
-
-val decr_underspec: #n:pos -> a:int_t n -> Pure (int_t n)
-  (requires (b2t (a > min_int n)))
-  (ensures (fun b -> a - 1 = b))
-
 let incr_mod (#n:pos) (a:int_t n) : Tot (int_t n) =
   (a + 1) % (pow2 (n-1))
 
@@ -109,11 +101,6 @@ let add (#n:pos) (a:int_t n) (b:int_t n)
       (ensures (fun _ -> True))
   = a + b
 
-val add_underspec: #n:pos -> a:int_t n -> b:int_t n -> Pure (int_t n)
-  (requires True)
-  (ensures (fun c ->
-    size (a + b) n ==> a + b = c))
-
 #push-options "--fuel 1"
 
 let add_mod (#n:pos) (a:int_t n) (b:int_t n) : Tot (int_t n) =
@@ -126,11 +113,6 @@ let sub (#n:pos) (a:int_t n) (b:int_t n)
       (ensures (fun _ -> True))    
   = a - b
 
-val sub_underspec: #n:pos -> a:int_t n -> b:int_t n -> Pure (int_t n)
-  (requires True)
-  (ensures (fun c ->
-    size (a - b) n ==> a - b = c))
-
 let sub_mod (#n:pos) (a:int_t n) (b:int_t n) : Tot (int_t n) =
   (a - b) @% (pow2 n)
 
@@ -141,11 +123,6 @@ let mul (#n:pos) (a:int_t n) (b:int_t n)
       (ensures (fun _ -> True))
   = a * b
 
-val mul_underspec: #n:pos -> a:int_t n -> b:int_t n -> Pure (int_t n)
-  (requires True)
-  (ensures (fun c ->
-    size (a * b) n ==> a * b = c))
-
 let mul_mod (#n:pos) (a:int_t n) (b:int_t n) : Tot (int_t n) =
   (a * b) @% (pow2 n)
 
@@ -158,11 +135,6 @@ let div (#n:pos) (a:int_t n) (b:int_t n{b <> 0})
       (ensures (fun c -> b <> 0 ==> a /- b = c))
 = a /- b
 
-val div_underspec: #n:pos -> a:int_t n -> b:int_t n{b <> 0} -> Pure (int_t n)
-  (requires True)
-  (ensures (fun c ->
-    (b <> 0 /\ size (a /- b) n) ==> a /- b = c))
-
 val div_size: #n:pos -> a:int_t n{min_int n < a} -> b:int_t n{b <> 0} ->
   Lemma (requires (size a n)) (ensures (size (a / b) n))