Merge branch 'master' into master

src/base/backend_extended.ml

@@ -59,8 +59,7 @@ 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 R1CS_constraint_system : Constraint_system.S with module Field := Field
 
   module Constraint : sig
     type t = (Cvar.t, Field.t) Constraint.t [@@deriving sexp]
@@ -82,15 +81,17 @@ module type S = sig
       -> (Cvar.t -> Field.t)
       -> bool
   end
+
+  module Run_state : Run_state_intf.S
 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 'field Run_state.t = 'field Backend.Run_state.t = struct
   open Backend
 
   module Bigint = struct
@@ -220,4 +221,5 @@ struct
   end
 
   module R1CS_constraint_system = R1CS_constraint_system
+  module Run_state = Run_state
 end

src/base/backend_intf.ml

@@ -1,37 +1,11 @@
-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
-
-  val add_constraint :
-    ?label:string -> t -> (Field.t Cvar.t, Field.t) Constraint.basic -> unit
-
-  val digest : t -> Md5.t
-
-  val set_primary_input_size : t -> int -> unit
-
-  val set_auxiliary_input_size : t -> int -> unit
-
-  val get_public_input_size : t -> int Core_kernel.Set_once.t
-
-  val get_rows_len : t -> int
-end
-
 module type S = sig
   module Field : Snarky_intf.Field.S
 
   module Bigint : Snarky_intf.Bigint_intf.Extended with type field := Field.t
 
   val field_size : Bigint.t
 
-  module R1CS_constraint_system :
-    Constraint_system_intf with module Field := Field
+  module R1CS_constraint_system : Constraint_system.S with module Field := Field
+
+  module Run_state : Run_state_intf.S
 end

src/base/checked.ml

@@ -10,7 +10,10 @@ end)
 (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
+  Checked_intf.S
+    with module Types := Types
+    with type field = Field.t
+     and type run_state = Basic.run_state = struct
   include Basic
 
   let request_witness (typ : ('var, 'value) Types.Typ.t)

src/base/checked_intf.ml

@@ -5,6 +5,8 @@ module type Basic = sig
 
   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
@@ -24,7 +26,7 @@ module type Basic = sig
 
   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)
@@ -38,6 +40,8 @@ module type S = sig
 
   type field
 
+  type run_state
+
   type 'a t = 'a Types.Checked.t
 
   include Monad_let.S with type 'a t := 'a t
@@ -100,7 +104,7 @@ module type S = sig
   val assert_equal :
     ?label:Base.string -> 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)
@@ -112,5 +116,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

src/base/checked_runner.ml

@@ -7,26 +7,54 @@ let eval_constraints = ref true
 
 let eval_constraints_ref = eval_constraints
 
-type ('a, 'f) t =
-  | Pure of 'a
-  | Function of ('f Run_state.t -> 'f Run_state.t * 'a)
+module T (Backend : Backend_extended.S) = struct
+  type 'a t =
+    | Pure of 'a
+    | Function of
+        (   Backend.Field.t Backend.Run_state.t
+         -> Backend.Field.t Backend.Run_state.t * 'a )
+end
 
 module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct
   type field = Backend.Field.t
 
   type field_var = field Cvar.t
 
-  type 'a checked = ('a, field) t
+  type 'a checked = 'a T(Backend).t
 
   type 'a as_prover = (field_var -> field) -> 'a
 end)
 
-module Simple = struct
-  let eval (t : ('a, 'f) t) : 'f Run_state.t -> 'f Run_state.t * 'a =
+module Make_checked
+    (Backend : Backend_extended.S)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Field.t Cvar.t
+                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
+                and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
+                and type ('var, 'value, 'aux) Typ.typ' =
+                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
+                and type ('var, 'value) Typ.typ =
+                 ('var, 'value) Simple_types(Backend).Typ.typ)
+    (As_prover : As_prover_intf.Basic
+                   with type field := Backend.Field.t
+                   with module Types := Types) =
+struct
+  type run_state = Backend.Field.t Backend.Run_state.t
+
+  type field = Backend.Field.t
+
+  type 'a t = 'a T(Backend).t =
+    | Pure of 'a
+    | Function of
+        (   Backend.Field.t Backend.Run_state.t
+         -> Backend.Field.t Backend.Run_state.t * 'a )
+
+  let eval (t : 'a t) : run_state -> run_state * 'a =
     match t with Pure a -> fun s -> (s, a) | Function g -> g
 
-  include Monad_let.Make2 (struct
-    type nonrec ('a, 'f) t = ('a, 'f) t
+  include Monad_let.Make (struct
+    type nonrec 'a t = 'a t
 
     let return x : _ t = Pure x
 
@@ -52,40 +80,6 @@ module Simple = struct
               let s, a = g s in
               eval (f a) s )
   end)
-end
-
-module Make_checked
-    (Backend : Backend_extended.S)
-    (Types : Types.Types
-               with type field = Backend.Field.t
-                and type field_var = Backend.Field.t Cvar.t
-                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
-                and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
-                and type ('var, 'value, 'aux) Typ.typ' =
-                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
-                and type ('var, 'value) Typ.typ =
-                 ('var, 'value) Simple_types(Backend).Typ.typ)
-    (As_prover : As_prover_intf.Basic
-                   with type field := Backend.Field.t
-                   with module Types := Types) =
-struct
-  type run_state = Backend.Field.t Run_state.t
-
-  type field = Backend.Field.t
-
-  type 'a t = 'a Types.Checked.t
-
-  let eval : 'a t -> run_state -> run_state * 'a = Simple.eval
-
-  include Monad_let.Make (struct
-    include Types.Checked
-
-    let map = `Custom Simple.map
-
-    let bind = Simple.bind
-
-    let return = Simple.return
-  end)
 
   open Backend
 
@@ -133,7 +127,7 @@ struct
               *)
               let label = "\nLazy value forced at:" in
               let _s', y =
-                Simple.eval (x ())
+                eval (x ())
                   (Run_state.set_stack s (old_stack @ (label :: stack)))
               in
               y ) ) )
@@ -144,7 +138,7 @@ struct
         let stack = Run_state.stack s in
         Option.iter (Run_state.log_constraint s) ~f:(fun f ->
             f ~at_label_boundary:(`Start, lab) None ) ;
-        let s', y = Simple.eval (t ()) (Run_state.set_stack s (lab :: stack)) in
+        let s', y = eval (t ()) (Run_state.set_stack s (lab :: stack)) in
         Option.iter (Run_state.log_constraint s) ~f:(fun f ->
             f ~at_label_boundary:(`End, lab) None ) ;
         (Run_state.set_stack s' stack, y) )
@@ -215,8 +209,7 @@ struct
       (fun s ->
         let handler = Run_state.handler s in
         let s', y =
-          Simple.eval (t ())
-            (Run_state.set_handler s (Request.Handler.push handler h))
+          eval (t ()) (Run_state.set_handler s (Request.Handler.push handler h))
         in
         (Run_state.set_handler s' handler, y) )
 
@@ -261,7 +254,7 @@ struct
             var_of_fields (field_vars, aux)
           in
           (* TODO: Push a label onto the stack here *)
-          let s, () = Simple.eval (check var) s in
+          let s, () = eval (check var) s in
           (s, { Handle.var; value = Some value }) )
         else
           let var =
@@ -271,7 +264,7 @@ struct
               , constraint_system_auxiliary () )
           in
           (* TODO: Push a label onto the stack here *)
-          let s, () = Simple.eval (check var) s in
+          let s, () = eval (check var) s in
           (s, { Handle.var; value = None }) )
 
   let next_auxiliary () : _ t =
@@ -297,7 +290,7 @@ struct
         ~next_auxiliary:(ref 1) ~aux:Run_state.Vector.null
         ~eval_constraints:false ~log_constraint ~with_witness:false ()
     in
-    let _ = Simple.eval (t ()) state in
+    let _ = eval (t ()) state in
     !count
 end
 
@@ -306,14 +299,14 @@ module type Run_extras = sig
 
   type cvar
 
+  type run_state
+
   module Types : Types.Types
 
-  val get_value : field Run_state.t -> cvar -> field
+  val get_value : run_state -> cvar -> field
 
   val run_as_prover :
-       'a Types.As_prover.t option
-    -> field Run_state.t
-    -> field Run_state.t * 'a option
+    'a Types.As_prover.t option -> run_state -> run_state * 'a option
 end
 
 module Make
@@ -356,15 +349,17 @@ struct
           Checked_intf.Basic
             with module Types := Types
             with type field := Checked_runner.field
+             and type run_state := run_state
 
         include
           Run_extras
             with module Types := Types
             with type field := Backend.Field.t
              and type cvar := Backend.Cvar.t
+             and type run_state := run_state
       end )
 
-  let run = Simple.eval
+  let run = Checked_runner.eval
 
   let dummy_vector = Run_state.Vector.null
 
@@ -418,8 +413,6 @@ module type S = sig
 
   val clear_constraint_logger : unit -> unit
 
-  type run_state = field Run_state.t
-
   type state = run_state
 
   type ('a, 't) run = 't -> run_state -> run_state * 'a
@@ -441,6 +434,6 @@ module type S = sig
             -> (field Cvar.t, field) Constraint.t option
             -> unit )
       -> unit
-      -> field Run_state.t
+      -> run_state
   end
 end

src/base/constraint_system.ml

@@ -1,7 +1,28 @@
-type 'f t =
-  | T :
-      (module Backend_intf.Constraint_system_intf
-         with type Field.t = 'f
-          and type t = 't )
-      * 't
-      -> 'f t
+open Core_kernel
+
+module type S = sig
+  module Field : sig
+    type t
+  end
+
+  type t
+
+  val create : unit -> t
+
+  val finalize : t -> unit
+
+  val add_constraint :
+    ?label:string -> t -> (Field.t Cvar.t, Field.t) Constraint.basic -> unit
+
+  val digest : t -> Md5.t
+
+  val set_primary_input_size : t -> int -> unit
+
+  val set_auxiliary_input_size : t -> int -> unit
+
+  val get_public_input_size : t -> int Core_kernel.Set_once.t
+
+  val get_rows_len : t -> int
+end
+
+type 'f t = T : (module S with type Field.t = 'f and type t = 't) * 't -> 'f t

src/base/dune

@@ -4,6 +4,7 @@
  (inline_tests)
  (libraries bitstring_lib core_kernel h_list interval_union snarky_intf
    bignum.bigint)
+ (modules_without_implementation run_state_intf)
  (preprocess
   (pps ppx_sexp_conv ppx_bin_prot ppx_let ppx_hash ppx_compare
     ppx_deriving.enum ppx_assert ppx_deriving.eq ppx_snarky ppx_fields_conv

src/base/run_state.ml

@@ -1,7 +1,7 @@
 module Vector = struct
   open Core_kernel
 
-  type 'elt t =
+  type 'elt t = 'elt Run_state_intf.Vector.t =
     | T :
         (module Snarky_intf.Vector.S with type elt = 'elt and type t = 't)
         * 't Type_equal.Id.t