Merge branch 'master' into patch-1

README.md

@@ -31,7 +31,7 @@ and answering yes to the prompts.
 
 ## Design
 
-The intention of this library is to allow writing snarks by writing what look
+The intention of this library is to allow writing snarks by writing what looks
 like normal programs (whose executions the snarks verify). If you're an experienced
 functional programmer, the basic idea (simplifying somewhat) is that there is a monad
 `Checked.t` so that a value of type `'a Checked.t` is an `'a` whose computation is

src/base/as_prover0.ml

@@ -6,7 +6,9 @@ module Make (Backend : sig
   end
 end)
 (Types : Types.Types
-           with type 'a As_prover.t =
+           with type field = Backend.Field.t
+            and type field_var = Backend.Field.t Cvar.t
+            and type 'a As_prover.t =
              (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a) =
 struct
   type 'a t = 'a Types.As_prover.t
@@ -37,8 +39,8 @@ struct
   let read_var (v : 'var) : 'field t = fun tbl -> tbl v
 
   let read
-      (Typ { var_to_fields; value_of_fields; _ } :
-        ('var, 'value, 'field) Types.Typ.t ) (var : 'var) : 'value t =
+      (Typ { var_to_fields; value_of_fields; _ } : ('var, 'value) Types.Typ.t)
+      (var : 'var) : 'value t =
    fun tbl ->
     let field_vars, aux = var_to_fields var in
     let fields = Array.map ~f:tbl field_vars in

src/base/as_prover_intf.ml

@@ -13,7 +13,7 @@ module type Basic = sig
 
   val read_var : field Cvar.t -> field t
 
-  val read : ('var, 'value, field) Types.Typ.t -> 'var -> 'value t
+  val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t
 
   module Provider : sig
     type 'a t

src/base/backend_extended.ml

@@ -59,38 +59,41 @@ module type S = sig
     val to_constant : t -> Field.t option
   end
 
-  module R1CS_constraint_system :
-    Backend_intf.Constraint_system_intf with module Field := Field
-
   module Constraint : sig
-    type t = (Cvar.t, Field.t) Constraint.t [@@deriving sexp]
-
-    type 'k with_constraint_args = ?label:string -> 'k
+    type t [@@deriving sexp]
 
-    val boolean : (Cvar.t -> t) with_constraint_args
+    val boolean : Cvar.t -> t
 
-    val equal : (Cvar.t -> Cvar.t -> t) with_constraint_args
+    val equal : Cvar.t -> Cvar.t -> t
 
-    val r1cs : (Cvar.t -> Cvar.t -> Cvar.t -> t) with_constraint_args
+    val r1cs : Cvar.t -> Cvar.t -> Cvar.t -> t
 
-    val square : (Cvar.t -> Cvar.t -> t) with_constraint_args
+    val square : Cvar.t -> Cvar.t -> t
 
-    val annotation : t -> string
+    val eval : t -> (Cvar.t -> Field.t) -> bool
 
-    val eval :
-         (Cvar.t, Field.t) Constraint.basic_with_annotation
-      -> (Cvar.t -> Field.t)
-      -> bool
+    val log_constraint : t -> (Cvar.t -> Field.t) -> string
   end
+
+  module R1CS_constraint_system :
+    Constraint_system.S
+      with module Field := Field
+      with type constraint_ = Constraint.t
+
+  module Run_state :
+    Run_state_intf.S
+      with type field := Field.t
+       and type constraint_ := Constraint.t
 end
 
 module Make (Backend : Backend_intf.S) :
   S
     with type Field.t = Backend.Field.t
      and type Field.Vector.t = Backend.Field.Vector.t
      and type Bigint.t = Backend.Bigint.t
-     and type R1CS_constraint_system.t = Backend.R1CS_constraint_system.t =
-struct
+     and type R1CS_constraint_system.t = Backend.R1CS_constraint_system.t
+     and type Run_state.t = Backend.Run_state.t
+     and type Constraint.t = Backend.Constraint.t = struct
   open Backend
 
   module Bigint = struct
@@ -206,18 +209,7 @@ struct
           None
   end
 
-  module Constraint = struct
-    open Constraint
-    include Constraint.T
-
-    type 'k with_constraint_args = ?label:string -> 'k
-
-    type t = (Cvar.t, Field.t) Constraint.t [@@deriving sexp]
-
-    let m = (module Field : Snarky_intf.Field.S with type t = Field.t)
-
-    let eval { basic; _ } get_value = Constraint.Basic.eval m get_value basic
-  end
-
+  module Constraint = Constraint
   module R1CS_constraint_system = R1CS_constraint_system
+  module Run_state = Run_state
 end

src/base/backend_intf.ml

@@ -1,37 +1,33 @@
-open Core_kernel
-
-module type Constraint_system_intf = sig
-  module Field : sig
-    type t
-  end
-
-  type t
-
-  val create : unit -> t
-
-  val finalize : t -> unit
+module type S = sig
+  module Field : Snarky_intf.Field.S
 
-  val add_constraint :
-    ?label:string -> t -> (Field.t Cvar.t, Field.t) Constraint.basic -> unit
+  module Bigint : Snarky_intf.Bigint_intf.Extended with type field := Field.t
 
-  val digest : t -> Md5.t
+  val field_size : Bigint.t
 
-  val set_primary_input_size : t -> int -> unit
+  module Constraint : sig
+    type t [@@deriving sexp]
 
-  val set_auxiliary_input_size : t -> int -> unit
+    val boolean : Field.t Cvar.t -> t
 
-  val get_public_input_size : t -> int Core_kernel.Set_once.t
+    val equal : Field.t Cvar.t -> Field.t Cvar.t -> t
 
-  val get_rows_len : t -> int
-end
+    val r1cs : Field.t Cvar.t -> Field.t Cvar.t -> Field.t Cvar.t -> t
 
-module type S = sig
-  module Field : Snarky_intf.Field.S
+    val square : Field.t Cvar.t -> Field.t Cvar.t -> t
 
-  module Bigint : Snarky_intf.Bigint_intf.Extended with type field := Field.t
+    val eval : t -> (Field.t Cvar.t -> Field.t) -> bool
 
-  val field_size : Bigint.t
+    val log_constraint : t -> (Field.t Cvar.t -> Field.t) -> string
+  end
 
   module R1CS_constraint_system :
-    Constraint_system_intf with module Field := Field
+    Constraint_system.S
+      with module Field := Field
+      with type constraint_ = Constraint.t
+
+  module Run_state :
+    Run_state_intf.S
+      with type field := Field.t
+       and type constraint_ := Constraint.t
 end

src/base/checked.ml

@@ -1,19 +1,23 @@
 open Core_kernel
 
-module Make (Field : sig
-  type t [@@deriving sexp]
-
-  val equal : t -> t -> bool
-end)
-(Types : Types.Types)
-(Basic : Checked_intf.Basic with type field = Field.t with module Types := Types)
-(As_prover : As_prover_intf.Basic
-               with type field := Basic.field
-               with module Types := Types) :
-  Checked_intf.S with module Types := Types with type field = Field.t = struct
+module Make
+    (Backend : Backend_extended.S)
+    (Types : Types.Types)
+    (Basic : Checked_intf.Basic
+               with type field = Backend.Field.t
+                and type constraint_ = Backend.Constraint.t
+               with module Types := Types)
+    (As_prover : As_prover_intf.Basic
+                   with type field := Basic.field
+                   with module Types := Types) :
+  Checked_intf.S
+    with module Types := Types
+    with type field = Backend.Field.t
+     and type run_state = Basic.run_state
+     and type constraint_ = Basic.constraint_ = struct
   include Basic
 
-  let request_witness (typ : ('var, 'value, field) Types.Typ.t)
+  let request_witness (typ : ('var, 'value) Types.Typ.t)
       (r : 'value Request.t As_prover.t) =
     let%map h = exists typ (Request r) in
     Handle.var h
@@ -66,23 +70,25 @@ end)
     in
     handle t (fun request -> (Option.value_exn !handler) request)
 
-  let assert_ ?label c = add_constraint (Constraint.override_label c label)
+  let assert_ c = add_constraint c
 
-  let assert_r1cs ?label a b c = assert_ (Constraint.r1cs ?label a b c)
+  let assert_r1cs a b c = assert_ (Backend.Constraint.r1cs a b c)
 
-  let assert_square ?label a c = assert_ (Constraint.square ?label a c)
+  let assert_square a c = assert_ (Backend.Constraint.square a c)
 
-  let assert_all ?label cs =
+  let assert_all cs =
     List.fold_right cs ~init:(return ()) ~f:(fun c (acc : _ t) ->
-        bind acc ~f:(fun () ->
-            add_constraint (Constraint.override_label c label) ) )
+        bind acc ~f:(fun () -> add_constraint c) )
 
-  let assert_equal ?label x y =
+  let assert_equal x y =
     match (x, y) with
     | Cvar.Constant x, Cvar.Constant y ->
-        if Field.equal x y then return ()
+        if Backend.Field.equal x y then return ()
         else
-          failwithf !"assert_equal: %{sexp: Field.t} != %{sexp: Field.t}" x y ()
+          failwithf
+            !"assert_equal: %{sexp: Backend.Field.t} != %{sexp: \
+              Backend.Field.t}"
+            x y ()
     | _ ->
-        assert_ (Constraint.equal ?label x y)
+        assert_ (Backend.Constraint.equal x y)
 end

src/base/checked_intf.ml

@@ -3,11 +3,15 @@ module type Basic = sig
 
   type field
 
+  type constraint_
+
   type 'a t = 'a Types.Checked.t
 
+  type run_state
+
   include Monad_let.S with type 'a t := 'a t
 
-  val add_constraint : (field Cvar.t, field) Constraint.t -> unit t
+  val add_constraint : constraint_ -> unit t
 
   val as_prover : unit Types.As_prover.t -> unit t
 
@@ -18,16 +22,16 @@ module type Basic = sig
   val with_handler : Request.Handler.single -> (unit -> 'a t) -> 'a t
 
   val exists :
-       ('var, 'value, field) Types.Typ.t
+       ('var, 'value) Types.Typ.t
     -> 'value Types.Provider.t
     -> ('var, 'value) Handle.t t
 
   val next_auxiliary : unit -> int t
 
-  val direct : (field Run_state.t -> field Run_state.t * 'a) -> 'a t
+  val direct : (run_state -> run_state * 'a) -> 'a t
 
   val constraint_count :
-       ?weight:((field Cvar.t, field) Constraint.t -> int)
+       ?weight:(constraint_ -> int)
     -> ?log:(?start:bool -> string -> int -> unit)
     -> (unit -> 'a t)
     -> int
@@ -38,6 +42,10 @@ module type S = sig
 
   type field
 
+  type constraint_
+
+  type run_state
+
   type 'a t = 'a Types.Checked.t
 
   include Monad_let.S with type 'a t := 'a t
@@ -47,26 +55,24 @@ module type S = sig
   val mk_lazy : (unit -> 'a t) -> 'a Lazy.t t
 
   val request_witness :
-       ('var, 'value, field) Types.Typ.t
-    -> 'value Request.t Types.As_prover.t
-    -> 'var t
+    ('var, 'value) Types.Typ.t -> 'value Request.t Types.As_prover.t -> 'var t
 
   val request :
        ?such_that:('var -> unit t)
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'value Request.t
     -> 'var t
 
   val exists_handle :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> ('var, 'value) Handle.t t
 
   val exists :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'var t
 
   type response = Request.response
@@ -87,25 +93,20 @@ module type S = sig
 
   val with_label : string -> (unit -> 'a t) -> 'a t
 
-  val assert_ :
-    ?label:Base.string -> (field Cvar.t, field) Constraint.t -> unit t
+  val assert_ : constraint_ -> unit t
 
-  val assert_r1cs :
-    ?label:Base.string -> field Cvar.t -> field Cvar.t -> field Cvar.t -> unit t
+  val assert_r1cs : field Cvar.t -> field Cvar.t -> field Cvar.t -> unit t
 
-  val assert_square :
-    ?label:Base.string -> field Cvar.t -> field Cvar.t -> unit t
+  val assert_square : field Cvar.t -> field Cvar.t -> unit t
 
-  val assert_all :
-    ?label:Base.string -> (field Cvar.t, field) Constraint.t list -> unit t
+  val assert_all : constraint_ list -> unit t
 
-  val assert_equal :
-    ?label:Base.string -> field Cvar.t -> field Cvar.t -> unit t
+  val assert_equal : field Cvar.t -> field Cvar.t -> unit t
 
-  val direct : (field Run_state.t -> field Run_state.t * 'a) -> 'a t
+  val direct : (run_state -> run_state * 'a) -> 'a t
 
   val constraint_count :
-       ?weight:((field Cvar.t, field) Constraint.t -> int)
+       ?weight:(constraint_ -> int)
     -> ?log:(?start:bool -> string -> int -> unit)
     -> (unit -> 'a t)
     -> int
@@ -114,5 +115,5 @@ end
 module type Extended = sig
   include S
 
-  val run : 'a t -> field Run_state.t -> field Run_state.t * 'a
+  val run : 'a t -> run_state -> run_state * 'a
 end