Put GMP-related arithmetic primitives in separate machine integer modules

drivers/c.drv

@@ -39,7 +39,7 @@ module mach.int.Int32
   syntax val (>)     "%1 > %2"
 end
 
-module mach.int.UInt32
+module mach.int.UInt32GMP
 
   prelude
 
@@ -160,7 +160,7 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
 
 end
 
-module mach.int.UInt64
+module mach.int.UInt64GMP
 
   prelude
 

examples/in_progress/multiprecision/mp2.mlw

@@ -86,7 +86,7 @@ module N
 
   use import mach.int.Int32
   use import ref.Ref
-  use import mach.int.UInt64 as Limb
+  use import mach.int.UInt64GMP as Limb
   use import int.Int
   use import int.Power
 

examples/in_progress/multiprecision/toom.mlw

@@ -5,7 +5,7 @@ module Toom
   use import mach.c.C
   use import ref.Ref
   use import mach.int.Int32
-  use import mach.int.UInt64 as Limb
+  use import mach.int.UInt64GMP as Limb
   use import int.Int
   use import int.Power
   use import mp2.N

stdlib/mach/c.mlw

@@ -2,7 +2,7 @@ module C
 
   use import mach.int.Unsigned
   use import mach.int.Int32
-  use import mach.int.UInt32
+  use import mach.int.UInt32GMP as UInt32
   use import array.Array
   use import map.Map
   use import int.Int
@@ -155,7 +155,7 @@ module C
     ensures  { pelts result = old pelts p }
     ensures  { plength result = old plength p }
     (* NOT alias result.data old p.data *)
-                   
+
   val join_r (p1 p2: ptr 'a) : unit
     requires { p1.zone = p2.zone }
     requires { p1.max = p2.min }

stdlib/mach/int.mlw

@@ -110,7 +110,6 @@ end
 module Unsigned
 
   use import int.Int
-  use import int.EuclideanDivision
 
   let constant min_unsigned : int = 0
 
@@ -125,6 +124,16 @@ module Unsigned
 
   axiom radix_def : radix = max+1
 
+end
+
+module UnsignedGMP
+
+  (** Additional GMP-inspired arithmetic primitives *)
+
+  use import int.Int
+  clone export Unsigned
+  use import int.EuclideanDivision
+
   val add_mod (x y:t) : t
     ensures { to_int result = mod (to_int x + to_int y) (max+1) }
 
@@ -228,12 +237,9 @@ module Int32BV
 
 end
 
-module UInt32
+module UInt32Gen
 
   use import int.Int
-  use import int.EuclideanDivision
-  use import int.Power
-  use import Int32
 
   type uint32 = < range 0 0xffff_ffff >
 
@@ -242,6 +248,12 @@ module UInt32
   let constant radix : int = max_uint32 + 1
   function to_int (x : uint32) : int = uint32'int x
 
+end
+
+module UInt32
+
+  use export UInt32Gen
+
   clone export Unsigned with
     type t = uint32,
     constant max = uint32'maxInt,
@@ -252,6 +264,26 @@ module UInt32
     lemma to_int_in_bounds,
     lemma extensionality
 
+end
+
+module UInt32GMP
+
+  use import int.Int
+  use import int.EuclideanDivision
+  use import int.Power
+  use import Int32
+  use export UInt32Gen
+
+  clone export UnsignedGMP with
+    type t = uint32,
+    constant max = uint32'maxInt,
+    constant radix = radix,
+    goal radix_def,
+    function to_int = uint32'int,
+    lemma zero_unsigned_is_zero,
+    lemma to_int_in_bounds,
+    lemma extensionality
+
   val lsld (x cnt:uint32) : (uint32,uint32)
     requires { 0 < to_int cnt < 32 }
     returns { (r,d) -> to_int r + (max_uint32+1) * to_int d =
@@ -460,12 +492,9 @@ module Int64
 *)
 end
 
-module UInt64
+module UInt64Gen
 
   use import int.Int
-  use import int.EuclideanDivision
-  use import int.Power
-  use import Int32
 
   type uint64 = < range 0 0xffff_ffff_ffff_ffff >
 
@@ -475,6 +504,12 @@ module UInt64
 
   function to_int (x : uint64) : int = uint64'int x
 
+end
+
+module UInt64
+
+  use export UInt64Gen
+
   clone export Unsigned with
     type t = uint64,
     constant max = uint64'maxInt,
@@ -485,6 +520,33 @@ module UInt64
     lemma to_int_in_bounds,
     lemma extensionality
 
+(*  use bv.BV64
+
+  val to_bv (x: uint64) : BV64.t
+    ensures { BV64.to_uint result = to_int x }
+  val of_bv (x: BV64.t) : uint64
+    ensures { to_int result = BV64.to_uint x }
+*)
+end
+
+module UInt64GMP
+
+  use import int.Int
+  use import int.EuclideanDivision
+  use import int.Power
+  use import Int32
+  use export UInt64Gen
+
+  clone export UnsignedGMP with
+    type t = uint64,
+    constant max = uint64'maxInt,
+    constant radix = radix,
+    goal radix_def,
+    function to_int = uint64'int,
+    lemma zero_unsigned_is_zero,
+    lemma to_int_in_bounds,
+    lemma extensionality
+
   val lsld (x cnt:uint64) : (uint64,uint64)
     requires { 0 < to_int cnt < 64 }
     returns { (r,d) -> to_int r + (max_uint64+1) * to_int d =
@@ -526,11 +588,4 @@ module UInt64
     requires { Int32.to_int x >= 0 }
     ensures { to_int result = Int32.to_int x }
 
-(*  use bv.BV64
-
-  val to_bv (x: uint64) : BV64.t
-    ensures { BV64.to_uint result = to_int x }
-  val of_bv (x: BV64.t) : uint64
-    ensures { to_int result = BV64.to_uint x }
-*)
-end
+end
\ No newline at end of file