add comparison functions to currency

src/lib/coda_numbers/intf.ml

@@ -185,3 +185,13 @@ module type F = functor
     end)
   (Bits : Bits_intf.Convertible_bits with type t := N.t)
   -> S with type t := N.t and module Bits := Bits
+
+[%%ifdef
+consensus_mechanism]
+
+module type F_checked = functor
+  (N : Unsigned_extended.S)
+  (Bits : Bits_intf.Convertible_bits with type t := N.t)
+  -> S_checked with type unchecked := N.t
+
+[%%endif]

src/lib/coda_numbers/nat.ml

@@ -14,129 +14,133 @@ open Snark_bits
 let zero_checked =
   Snarky_integer.Integer.constant ~m:Snark_params.Tick.m Bigint.zero
 
-[%%else]
+module Make_checked
+    (N : Unsigned_extended.S)
+    (Bits : Bits_intf.Convertible_bits with type t := N.t) =
+struct
+  open Bitstring_lib
+  open Snark_params.Tick
+  open Snarky_integer
 
-open Snark_bits_nonconsensus
+  type var = field Integer.t
 
-[%%endif]
+  let () = assert (Int.(N.length_in_bits < Field.size_in_bits))
 
-module Make (N : sig
-  type t [@@deriving sexp, compare, hash]
+  let to_field = Integer.to_field
 
-  include Unsigned_extended.S with type t := t
+  let of_bits bs = Integer.of_bits ~m bs
 
-  val random : unit -> t
-end)
-(Bits : Bits_intf.Convertible_bits with type t := N.t) =
-struct
-  type t = N.t [@@deriving sexp, compare, hash, yojson]
+  let to_bits t =
+    with_label
+      (sprintf "to_bits: %s" __LOC__)
+      (make_checked (fun () -> Integer.to_bits ~length:N.length_in_bits ~m t))
 
-  (* can't be automatically derived *)
-  let dhall_type = Ppx_dhall_type.Dhall_type.Text
+  let to_input t =
+    Checked.map (to_bits t) ~f:(fun bits ->
+        Random_oracle.Input.bitstring
+          (Bitstring_lib.Bitstring.Lsb_first.to_list bits) )
 
-  let max_value = N.max_int
+  let constant n = Integer.constant ~length:N.length_in_bits ~m (N.to_bigint n)
 
-  include Comparable.Make (N)
+  (* warning: this typ does not work correctly with the generic if_ *)
+  let typ : (field Integer.t, N.t) Typ.t =
+    let typ = Typ.list ~length:N.length_in_bits Boolean.typ in
+    let of_bits bs = of_bits (Bitstring.Lsb_first.of_list bs) in
+    let alloc = Typ.Alloc.map typ.alloc ~f:of_bits in
+    let store t =
+      Typ.Store.map (typ.store (Fold.to_list (Bits.fold t))) ~f:of_bits
+    in
+    let check v =
+      typ.check (Bitstring.Lsb_first.to_list (Integer.to_bits_exn v))
+    in
+    let read v =
+      let of_field_elt x =
+        let bs = List.take (Field.unpack x) N.length_in_bits in
+        (* TODO: Make this efficient *)
+        List.foldi bs ~init:N.zero ~f:(fun i acc b ->
+            if b then N.(logor (shift_left one i) acc) else acc )
+      in
+      Typ.Read.map (Field.typ.read (Integer.to_field v)) ~f:of_field_elt
+    in
+    {alloc; store; check; read}
 
-  include (N : module type of N with type t := t)
+  type t = var
 
-  [%%ifdef
-  consensus_mechanism]
+  let is_succ ~pred ~succ =
+    let open Snark_params.Tick in
+    let open Field in
+    Checked.(equal (to_field pred + Var.constant one) (to_field succ))
 
-  module Checked = struct
-    open Bitstring_lib
-    open Snark_params.Tick
-    open Snarky_integer
+  let min a b = make_checked (fun () -> Integer.min ~m a b)
 
-    type var = field Integer.t
+  let if_ c ~then_ ~else_ =
+    make_checked (fun () -> Integer.if_ ~m c ~then_ ~else_)
 
-    let () = assert (Int.(N.length_in_bits < Field.size_in_bits))
+  let succ_if t c =
+    make_checked (fun () ->
+        let t = Integer.succ_if ~m t c in
+        t )
 
-    let to_field = Integer.to_field
+  let succ t =
+    make_checked (fun () ->
+        let t = Integer.succ ~m t in
+        t )
 
-    let of_bits bs = Integer.of_bits ~m bs
+  let op op a b = make_checked (fun () -> op ~m a b)
 
-    let to_bits t =
-      with_label
-        (sprintf "to_bits: %s" __LOC__)
-        (make_checked (fun () -> Integer.to_bits ~length:N.length_in_bits ~m t))
+  let add a b = op Integer.add a b
 
-    let to_input t =
-      Checked.map (to_bits t) ~f:(fun bits ->
-          Random_oracle.Input.bitstring
-            (Bitstring_lib.Bitstring.Lsb_first.to_list bits) )
+  let equal a b = op Integer.equal a b
 
-    let constant n =
-      Integer.constant ~length:N.length_in_bits ~m (N.to_bigint n)
+  let ( < ) a b = op Integer.lt a b
 
-    (* warning: this typ does not work correctly with the generic if_ *)
-    let typ : (field Integer.t, t) Typ.t =
-      let typ = Typ.list ~length:N.length_in_bits Boolean.typ in
-      let of_bits bs = of_bits (Bitstring.Lsb_first.of_list bs) in
-      let alloc = Typ.Alloc.map typ.alloc ~f:of_bits in
-      let store t =
-        Typ.Store.map (typ.store (Fold.to_list (Bits.fold t))) ~f:of_bits
-      in
-      let check v =
-        typ.check (Bitstring.Lsb_first.to_list (Integer.to_bits_exn v))
-      in
-      let read v =
-        let of_field_elt x =
-          let bs = List.take (Field.unpack x) N.length_in_bits in
-          (* TODO: Make this efficient *)
-          List.foldi bs ~init:N.zero ~f:(fun i acc b ->
-              if b then N.(logor (shift_left one i) acc) else acc )
-        in
-        Typ.Read.map (Field.typ.read (Integer.to_field v)) ~f:of_field_elt
-      in
-      {alloc; store; check; read}
+  let ( <= ) a b = op Integer.lte a b
 
-    type t = var
+  let ( > ) a b = op Integer.gt a b
 
-    let is_succ ~pred ~succ =
-      let open Snark_params.Tick in
-      let open Field in
-      Checked.(equal (to_field pred + Var.constant one) (to_field succ))
+  let ( >= ) a b = op Integer.gte a b
 
-    let min a b = make_checked (fun () -> Integer.min ~m a b)
+  let ( = ) = equal
 
-    let if_ c ~then_ ~else_ =
-      make_checked (fun () -> Integer.if_ ~m c ~then_ ~else_)
+  let to_integer = Fn.id
 
-    let succ_if t c =
-      make_checked (fun () ->
-          let t = Integer.succ_if ~m t c in
-          t )
+  module Unsafe = struct
+    let of_integer = Fn.id
+  end
 
-    let succ t =
-      make_checked (fun () ->
-          let t = Integer.succ ~m t in
-          t )
+  let zero = zero_checked
+end
 
-    let op op a b = make_checked (fun () -> op ~m a b)
+[%%else]
 
-    let add a b = op Integer.add a b
+open Snark_bits_nonconsensus
 
-    let equal a b = op Integer.equal a b
+[%%endif]
 
-    let ( < ) a b = op Integer.lt a b
+module Make (N : sig
+  type t [@@deriving sexp, compare, hash]
 
-    let ( <= ) a b = op Integer.lte a b
+  include Unsigned_extended.S with type t := t
 
-    let ( > ) a b = op Integer.gt a b
+  val random : unit -> t
+end)
+(Bits : Bits_intf.Convertible_bits with type t := N.t) =
+struct
+  type t = N.t [@@deriving sexp, compare, hash, yojson]
 
-    let ( >= ) a b = op Integer.gte a b
+  (* can't be automatically derived *)
+  let dhall_type = Ppx_dhall_type.Dhall_type.Text
 
-    let ( = ) = equal
+  let max_value = N.max_int
 
-    let to_integer = Fn.id
+  include Comparable.Make (N)
 
-    module Unsafe = struct
-      let of_integer = Fn.id
-    end
+  include (N : module type of N with type t := t)
 
-    let zero = zero_checked
-  end
+  [%%ifdef
+  consensus_mechanism]
+
+  module Checked = Make_checked (N) (Bits)
 
   (* warning: this typ does not work correctly with the generic if_ *)
   let typ = Checked.typ

src/lib/coda_numbers/nat.mli

@@ -1,7 +1,15 @@
+[%%import "/src/config.mlh"]
+
 module Intf = Intf
 
 module Make : Intf.F
 
+[%%ifdef consensus_mechanism]
+
+module Make_checked : Intf.F_checked
+
+[%%endif]
+
 module Make32 () : Intf.UInt32
 
 module Make64 () : Intf.UInt64

src/lib/currency/currency.ml

@@ -137,8 +137,9 @@ end = struct
       else Infix.(v land lognot (one lsl i))
   end
 
-  include (
-    Bits.Vector.Make (Vector) : Bits_intf.Convertible_bits with type t := t)
+  module B = Bits.Vector.Make (Vector)
+
+  include (B : Bits_intf.Convertible_bits with type t := t)
 
   [%%ifdef
   consensus_mechanism]
@@ -255,6 +256,8 @@ end = struct
         ~value_of_hlist:typ_of_hlist
 
     module Checked = struct
+      type t = var
+
       let to_bits {magnitude; sgn} =
         Sgn.Checked.is_pos sgn :: (var_to_bits magnitude :> Boolean.var list)
 
@@ -344,6 +347,10 @@ end = struct
   consensus_mechanism]
 
   module Checked = struct
+    module N = Coda_numbers.Nat.Make_checked (Unsigned) (B)
+
+    type t = var
+
     let if_ = if_
 
     let if_value cond ~then_ ~else_ : var =
@@ -373,6 +380,20 @@ end = struct
 
     let equal x y = Field.Checked.equal (pack_var x) (pack_var y)
 
+    let ( = ) = equal
+
+    let op f (x : var) (y : var) : (Boolean.var, 'a) Checked.t =
+      let g = Fn.compose N.of_bits var_to_bits in
+      f (g x) (g y)
+
+    let ( <= ) x = op N.( <= ) x
+
+    let ( >= ) x = op N.( >= ) x
+
+    let ( < ) x = op N.( < ) x
+
+    let ( > ) x = op N.( > ) x
+
     (* Unpacking protects against overflow *)
     let add (x : Unpacked.var) (y : Unpacked.var) =
       unpack_var (Field.Var.add (pack_var x) (pack_var y))
@@ -482,7 +503,7 @@ end = struct
           qc_test_fast generator ~shrinker ~f:(fun num ->
               match of_formatted_string (to_formatted_string num) with
               | after_format ->
-                  if after_format = num then ()
+                  if Unsigned.equal after_format num then ()
                   else
                     Error.(
                       raise

src/lib/currency/currency.mli

@@ -51,7 +51,7 @@ module Fee : sig
       Checked_arithmetic_intf
       with type var := var
        and type signed_var := Signed.var
-       and type t := t
+       and type value := t
 
     val add_signed : var -> Signed.var -> (var, _) Checked.t
   end
@@ -102,7 +102,7 @@ module Amount : sig
       Checked_arithmetic_intf
       with type var := var
        and type signed_var := Signed.var
-       and type t := t
+       and type value := t
 
     val add_signed : var -> Signed.var -> (var, _) Checked.t
 

src/lib/currency/dune

@@ -3,7 +3,7 @@
  (public_name currency)
  (library_flags -linkall)
  (inline_tests)
- (libraries core fold_lib tuple_lib snark_bits sgn snark_params random_oracle
+ (libraries core coda_numbers fold_lib tuple_lib snark_bits sgn snark_params random_oracle
    unsigned_extended test_util codable ppx_dhall_type)
  (preprocessor_deps ../../config.mlh)
  (preprocess

src/lib/currency/intf.ml

@@ -159,6 +159,8 @@ module type Signed_intf = sig
       -> (magnitude_var, Sgn.t) Signed_poly.t
          * (magnitude_var, Sgn.t) Signed_poly.t
       -> (var * var, _) Checked.t
+
+    type t = var
   end
 
   [%%endif]
@@ -168,15 +170,17 @@ end
 consensus_mechanism]
 
 module type Checked_arithmetic_intf = sig
-  type t
+  type value
 
   type var
 
+  type t = var
+
   type signed_var
 
   val if_ : Boolean.var -> then_:var -> else_:var -> (var, _) Checked.t
 
-  val if_value : Boolean.var -> then_:t -> else_:t -> var
+  val if_value : Boolean.var -> then_:value -> else_:value -> var
 
   val add : var -> var -> (var, _) Checked.t
 
@@ -198,6 +202,16 @@ module type Checked_arithmetic_intf = sig
 
   val equal : var -> var -> (Boolean.var, _) Checked.t
 
+  val ( = ) : t -> t -> (Boolean.var, _) Checked.t
+
+  val ( < ) : t -> t -> (Boolean.var, _) Checked.t
+
+  val ( > ) : t -> t -> (Boolean.var, _) Checked.t
+
+  val ( <= ) : t -> t -> (Boolean.var, _) Checked.t
+
+  val ( >= ) : t -> t -> (Boolean.var, _) Checked.t
+
   val scale : Field.Var.t -> var -> (var, _) Checked.t
 end
 
@@ -217,7 +231,7 @@ module type S = sig
     Checked_arithmetic_intf
     with type var := var
      and type signed_var := Signed.var
-     and type t := t
+     and type value := t
 
   [%%else]