diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index c3d77eac5..998a4dd36 100644 --- a/src/base/backend_extended.ml +++ b/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,6 +81,8 @@ module type S = sig -> (Cvar.t -> Field.t) -> bool end + + module Run_state : Run_state_intf.S end module Make (Backend : Backend_intf.S) : @@ -89,8 +90,8 @@ module Make (Backend : Backend_intf.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 diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml index bd80cb798..005b3a464 100644 --- a/src/base/backend_intf.ml +++ b/src/base/backend_intf.ml @@ -1,30 +1,3 @@ -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 @@ -32,6 +5,7 @@ module type S = sig 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 diff --git a/src/base/checked.ml b/src/base/checked.ml index d6aa33b2c..631dd9ba3 100644 --- a/src/base/checked.ml +++ b/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) diff --git a/src/base/checked_intf.ml b/src/base/checked_intf.ml index 9d237f91b..e719fde4c 100644 --- a/src/base/checked_intf.ml +++ b/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 diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 6e481edbc..dc4a08901 100644 --- a/src/base/checked_runner.ml +++ b/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 diff --git a/src/base/constraint_system.ml b/src/base/constraint_system.ml index 809c2d837..e12bfd6e7 100644 --- a/src/base/constraint_system.ml +++ b/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 diff --git a/src/base/dune b/src/base/dune index 99cfab1fb..7c4b4a684 100644 --- a/src/base/dune +++ b/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 diff --git a/src/base/run_state.ml b/src/base/run_state.ml index c0cc1e1a4..cd148e418 100644 --- a/src/base/run_state.ml +++ b/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 diff --git a/src/base/run_state.mli b/src/base/run_state.mli index 6fe4f8513..82c540bbc 100644 --- a/src/base/run_state.mli +++ b/src/base/run_state.mli @@ -1,78 +1 @@ -module Vector : sig - type 'elt t = - | T : - (module Snarky_intf.Vector.S with type elt = 'elt and type t = 't) - * 't Base.Type_equal.Id.t - * 't - -> 'elt t - - val unit : unit Base.Type_equal.Id.t - - val null : 'a t - - val get : 'x t -> int -> 'x - - val emplace_back : 'x t -> 'x -> unit -end - -type 'field t - -val make : - num_inputs:int - -> input:'field Vector.t - -> next_auxiliary:int ref - -> aux:'field Vector.t - -> ?system:'field Constraint_system.t - -> eval_constraints:bool - -> ?log_constraint: - ( ?at_label_boundary:[ `End | `Start ] * string - -> ('field Cvar.t, 'field) Constraint.t option - -> unit ) - -> ?handler:Request.Handler.t - -> with_witness:bool - -> ?stack:string list - -> ?is_running:bool - -> unit - -> 'field t - -(** dumps some information about a state [t] *) -val dump : 'field t -> string - -val get_variable_value : 'field t -> int -> 'field - -val store_field_elt : 'field t -> 'field -> 'field Cvar.t - -val alloc_var : 'field t -> unit -> 'field Cvar.t - -val id : _ t -> int - -val has_witness : _ t -> bool - -val as_prover : _ t -> bool - -val set_as_prover : _ t -> bool -> unit - -val stack : _ t -> string list - -val set_stack : 'field t -> string list -> 'field t - -val log_constraint : - 'field t - -> ( ?at_label_boundary:[ `Start | `End ] * string - -> ('field Cvar.t, 'field) Constraint.t option - -> unit ) - option - -val eval_constraints : 'field t -> bool - -val system : 'field t -> 'field Constraint_system.t option - -val handler : _ t -> Request.Handler.t - -val set_handler : 'field t -> Request.Handler.t -> 'field t - -val is_running : _ t -> bool - -val set_is_running : 'f t -> bool -> 'f t - -val next_auxiliary : _ t -> int +include Run_state_intf.S diff --git a/src/base/run_state_intf.mli b/src/base/run_state_intf.mli new file mode 100644 index 000000000..a0959798f --- /dev/null +++ b/src/base/run_state_intf.mli @@ -0,0 +1,89 @@ +module Vector : sig + type 'elt t = + | T : + (module Snarky_intf.Vector.S with type elt = 'elt and type t = 't) + * 't Base.Type_equal.Id.t + * 't + -> 'elt t +end + +module type S = sig + module Vector : sig + type 'elt t = 'elt Vector.t = + | T : + (module Snarky_intf.Vector.S with type elt = 'elt and type t = 't) + * 't Base.Type_equal.Id.t + * 't + -> 'elt t + + val unit : unit Base.Type_equal.Id.t + + val null : 'a t + + val get : 'x t -> int -> 'x + + val emplace_back : 'x t -> 'x -> unit + end + + type 'field t + + val make : + num_inputs:int + -> input:'field Vector.t + -> next_auxiliary:int ref + -> aux:'field Vector.t + -> ?system:'field Constraint_system.t + -> eval_constraints:bool + -> ?log_constraint: + ( ?at_label_boundary:[ `End | `Start ] * string + -> ('field Cvar.t, 'field) Constraint.t option + -> unit ) + -> ?handler:Request.Handler.t + -> with_witness:bool + -> ?stack:string list + -> ?is_running:bool + -> unit + -> 'field t + + (** dumps some information about a state [t] *) + val dump : 'field t -> string + + val get_variable_value : 'field t -> int -> 'field + + val store_field_elt : 'field t -> 'field -> 'field Cvar.t + + val alloc_var : 'field t -> unit -> 'field Cvar.t + + val id : _ t -> int + + val has_witness : _ t -> bool + + val as_prover : _ t -> bool + + val set_as_prover : _ t -> bool -> unit + + val stack : _ t -> string list + + val set_stack : 'field t -> string list -> 'field t + + val log_constraint : + 'field t + -> ( ?at_label_boundary:[ `Start | `End ] * string + -> ('field Cvar.t, 'field) Constraint.t option + -> unit ) + option + + val eval_constraints : 'field t -> bool + + val system : 'field t -> 'field Constraint_system.t option + + val handler : _ t -> Request.Handler.t + + val set_handler : 'field t -> Request.Handler.t -> 'field t + + val is_running : _ t -> bool + + val set_is_running : 'f t -> bool -> 'f t + + val next_auxiliary : _ t -> int +end diff --git a/src/base/runners.ml b/src/base/runners.ml index 453e87e79..d7111c155 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -6,8 +6,9 @@ module Make with type field = Backend.Field.t and type field_var = Backend.Cvar.t) (Checked : Checked_intf.Extended + with module Types := Types with type field = Backend.Field.t - with module Types := Types) + and type run_state = Backend.Field.t Backend.Run_state.t) (As_prover : As_prover_intf.Basic with type field := Backend.Field.t with module Types := Types) @@ -16,7 +17,8 @@ module Make with type field := Backend.Field.t and type cvar := Backend.Cvar.t and type constr := Backend.Constraint.t option - and type r1cs := Backend.R1CS_constraint_system.t) = + and type r1cs := Backend.R1CS_constraint_system.t + and type run_state = Backend.Field.t Backend.Run_state.t) = struct open Backend @@ -215,7 +217,7 @@ struct Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system ~with_witness:false () in - let id = Run_state.id state in + let id = Backend.Run_state.id state in let state, () = (* create constraints to validate the input (using the input [Typ]'s [check]) *) let checked = @@ -226,7 +228,7 @@ struct in let run_computation k = k var state in let finish_computation (state, res) = - let final_id = Run_state.id state in + let final_id = Backend.Run_state.id state in if id <> final_id then failwith "Snarky's internal state has been clobbered." ; let res, _ = return_typ.var_to_fields res in diff --git a/src/base/snark0.ml b/src/base/snark0.ml index bfd72e48e..0a49ecf12 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -14,8 +14,9 @@ module Make_basic with type field = Backend.Field.t and type field_var = Backend.Cvar.t) (Checked : Checked_intf.Extended + with module Types := Types with type field = Backend.Field.t - with module Types := Types) + and type run_state = Backend.Field.t Backend.Run_state.t) (As_prover : As_prover_intf.Basic with type field := Backend.Field.t with module Types := Types) @@ -24,7 +25,8 @@ module Make_basic with type field := Backend.Field.t and type cvar := Backend.Cvar.t and type constr := Backend.Constraint.t option - and type r1cs := Backend.R1CS_constraint_system.t) = + and type r1cs := Backend.R1CS_constraint_system.t + and type run_state = Backend.Field.t Backend.Run_state.t) = struct open Backend @@ -74,14 +76,12 @@ struct Checked : Checked_intf.Extended with module Types := Types - with type field := field ) + with type field := field + and type run_state = Backend.Field.t Backend.Run_state.t ) let perform req = request_witness Typ.unit req module Runner = Runner - - type run_state = Runner.run_state - include Utils.Make (Backend) (Types) (Checked) (As_prover) (Typ) (Runner) module Control = struct end @@ -677,7 +677,8 @@ module Make (Backend : Backend_intf.S) = struct Checked_intf.S with module Types := Types with type 'a t := 'a Checked1.t - and type field := Backend_extended.Field.t ) + and type field := Backend_extended.Field.t + and type run_state = Backend.Field.t Backend.Run_state.t ) type field = Backend_extended.Field.t @@ -714,7 +715,7 @@ module Run = struct module Make_basic (Backend : Backend_intf.S) = struct module Snark = Make (Backend) - open Run_state + open Backend.Run_state open Snark let set_constraint_logger = set_constraint_logger @@ -725,16 +726,17 @@ module Run = struct let state = ref - (Run_state.make ~input:(field_vec ()) ~aux:(field_vec ()) + (Backend.Run_state.make ~input:(field_vec ()) ~aux:(field_vec ()) ~eval_constraints:false ~num_inputs:0 ~next_auxiliary:(ref 0) ~with_witness:false ~stack:[] ~is_running:false () ) - let dump () = Run_state.dump !state + let dump () = Backend.Run_state.dump !state - let in_prover () : bool = Run_state.has_witness !state + let in_prover () : bool = Backend.Run_state.has_witness !state let in_checked_computation () : bool = - is_active_functor_id this_functor_id && Run_state.is_running !state + is_active_functor_id this_functor_id + && Backend.Run_state.is_running !state let run (checked : _ Checked.t) = match checked with @@ -748,7 +750,7 @@ module Run = struct %i, but the module used to run it had internal ID %i. The same \ instance of Snarky.Snark.Run.Make must be used for both." this_functor_id (active_functor_id ()) () - else if not (Run_state.is_running !state) then + else if not (Backend.Run_state.is_running !state) then failwith "This function can't be run outside of a checked computation." ; let state', x = Runner.run checked !state in @@ -1127,12 +1129,15 @@ module Run = struct type 'a as_prover = 'a t let eval_as_prover f = - if Run_state.as_prover !state && Run_state.has_witness !state then + if + Backend.Run_state.as_prover !state + && Backend.Run_state.has_witness !state + then let a = f (Runner.get_value !state) in a else failwith "Can't evaluate prover code outside an as_prover block" - let in_prover_block () = Run_state.as_prover !state + let in_prover_block () = Backend.Run_state.as_prover !state let read_var var = eval_as_prover (As_prover.read_var var) @@ -1144,10 +1149,10 @@ module Run = struct (* Allow for nesting of prover blocks, by caching the current value and restoring it once we're done. *) - let old = Run_state.as_prover !state in - Run_state.set_as_prover !state true ; + let old = Backend.Run_state.as_prover !state in + Backend.Run_state.set_as_prover !state true ; let a = f () in - Run_state.set_as_prover !state old ; + Backend.Run_state.set_as_prover !state old ; a end @@ -1231,10 +1236,11 @@ module Run = struct let handle x h = let h = Request.Handler.create_single h in - let handler = Run_state.handler !state in - state := Run_state.set_handler !state (Request.Handler.push handler h) ; + let handler = Backend.Run_state.handler !state in + state := + Backend.Run_state.set_handler !state (Request.Handler.push handler h) ; let a = x () in - state := Run_state.set_handler !state handler ; + state := Backend.Run_state.set_handler !state handler ; a let handle_as_prover x h = @@ -1244,15 +1250,15 @@ module Run = struct let if_ b ~typ ~then_ ~else_ = run (if_ b ~typ ~then_ ~else_) let with_label lbl x = - let stack = Run_state.stack !state in - let log_constraint = Run_state.log_constraint !state in - state := Run_state.set_stack !state (lbl :: stack) ; + let stack = Backend.Run_state.stack !state in + let log_constraint = Backend.Run_state.log_constraint !state in + state := Backend.Run_state.set_stack !state (lbl :: stack) ; Option.iter log_constraint ~f:(fun f -> f ~at_label_boundary:(`Start, lbl) None ) ; let a = x () in Option.iter log_constraint ~f:(fun f -> f ~at_label_boundary:(`End, lbl) None ) ; - state := Run_state.set_stack !state stack ; + state := Backend.Run_state.set_stack !state stack ; a let inject_wrapper : @@ -1397,27 +1403,27 @@ module Run = struct let as_prover_manual (size_to_witness : int) : (field array option -> Field.t array) Staged.t = let s = !state in - let old_as_prover = Run_state.as_prover s in + let old_as_prover = Backend.Run_state.as_prover s in (* enter the as_prover block *) - Run_state.set_as_prover s true ; + Backend.Run_state.set_as_prover s true ; let finish_computation (values_to_witness : field array option) = (* leave the as_prover block *) - Run_state.set_as_prover s old_as_prover ; + Backend.Run_state.set_as_prover s old_as_prover ; (* return variables *) - match (Run_state.has_witness s, values_to_witness) with + match (Backend.Run_state.has_witness s, values_to_witness) with (* in compile mode, we return empty vars *) | false, None -> Core_kernel.Array.init size_to_witness ~f:(fun _ -> - Run_state.alloc_var s () ) + Backend.Run_state.alloc_var s () ) (* in prover mode, we expect values to turn into vars *) | true, Some values_to_witness -> let store_value = (* If we're nested in a prover block, create constants instead of storing. *) if old_as_prover then Field.constant - else Run_state.store_field_elt s + else Backend.Run_state.store_field_elt s in Core_kernel.Array.map values_to_witness ~f:store_value (* the other cases are invalid *) @@ -1429,17 +1435,17 @@ module Run = struct Staged.stage finish_computation let request_manual (req : unit -> 'a Request.t) () : 'a = - Request.Handler.run (Run_state.handler !state) (req ()) + Request.Handler.run (Backend.Run_state.handler !state) (req ()) |> Option.value_exn ~message:"Unhandled request" module Async_generic (Promise : Base.Monad.S) = struct let run_prover ~(else_ : unit -> 'a) (f : unit -> 'a Promise.t) : 'a Promise.t = - if Run_state.has_witness !state then ( - let old = Run_state.as_prover !state in - Run_state.set_as_prover !state true ; + if Backend.Run_state.has_witness !state then ( + let old = Backend.Run_state.as_prover !state in + Backend.Run_state.set_as_prover !state true ; let%map.Promise result = f () in - Run_state.set_as_prover !state old ; + Backend.Run_state.set_as_prover !state old ; result ) else Promise.return (else_ ()) @@ -1459,10 +1465,10 @@ module Run = struct Perform.run_and_check_exn ~run:as_stateful (fun () -> mark_active ~f:(fun () -> let prover_block = x () in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; As_prover.run_prover prover_block ) ) in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; res ) let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t) : @@ -1472,10 +1478,10 @@ module Run = struct Perform.run_and_check ~run:as_stateful (fun () -> mark_active ~f:(fun () -> let prover_block = x () in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; As_prover.run_prover prover_block ) ) in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; res ) module Run_and_check_deferred (M : sig @@ -1513,10 +1519,10 @@ module Run = struct run_and_check_exn ~run:as_stateful (fun () -> mark_active ~f:(fun () -> map (x ()) ~f:(fun prover_block -> - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; As_prover.run_prover prover_block ) ) ) in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; res ) let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t M.t) : @@ -1527,10 +1533,10 @@ module Run = struct run_and_check ~run:as_stateful (fun () -> mark_active ~f:(fun () -> map (x ()) ~f:(fun prover_block -> - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; As_prover.run_prover prover_block ) ) ) in - Run_state.set_as_prover !state true ; + Backend.Run_state.set_as_prover !state true ; res ) end diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index caeda7505..4213be5f4 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -614,8 +614,6 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) ]} *) - type run_state = Field.t Run_state.t - include Monad_let.S module List : @@ -1222,10 +1220,7 @@ module type Run_basic = sig } end - and Internal_Basic : - (Basic - with type field = field - and type 'a Checked.t = ('a, field) Checked_runner.t) + and Internal_Basic : (Basic with type field = field) module Bitstring_checked : sig type t = Boolean.var list diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 55b31bf8b..5a713060b 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -24,6 +24,7 @@ module Pedersen = Pedersen module Request = Request module Restrict_monad = Restrict_monad module Run_state = Run_state +module Run_state_intf = Run_state_intf module Snark = Snark module Snark0 = Snark0 module Snark_intf = Snark_intf diff --git a/src/base/utils.ml b/src/base/utils.ml index 944edeb91..4c1bdf5e8 100644 --- a/src/base/utils.ml +++ b/src/base/utils.ml @@ -10,8 +10,9 @@ module Make with type field = Backend.Field.t and type field_var = Backend.Cvar.t) (Checked : Checked_intf.Extended + with module Types := Types with type field = Backend.Field.t - with module Types := Types) + and type run_state = Backend.Field.t Backend.Run_state.t) (As_prover : As_prover_intf.Basic with type field := Backend.Field.t with module Types := Types) @@ -27,7 +28,8 @@ module Make with type field := Backend.Field.t and type cvar := Backend.Cvar.t and type constr := Backend.Constraint.t option - and type r1cs := Backend.R1CS_constraint_system.t) = + and type r1cs := Backend.R1CS_constraint_system.t + and type run_state = Backend.Field.t Backend.Run_state.t) = struct open Backend diff --git a/src/base/utils.mli b/src/base/utils.mli index 0fa8633eb..05a47d7d3 100644 --- a/src/base/utils.mli +++ b/src/base/utils.mli @@ -9,8 +9,9 @@ module Make : functor with type field = Backend.Field.t and type field_var = Backend.Cvar.t) (Checked : Checked_intf.Extended + with module Types := Types with type field = Backend.Field.t - with module Types := Types) + and type run_state = Backend.Field.t Backend.Run_state.t) (As_prover : As_prover_intf.Basic with type field := Backend.Field.t with module Types := Types) @@ -26,7 +27,8 @@ module Make : functor with type field := Backend.Field.t and type cvar := Backend.Cvar.t and type constr := Backend.Constraint.t option - and type r1cs := Backend.R1CS_constraint_system.t) + and type r1cs := Backend.R1CS_constraint_system.t + and type run_state = Backend.Field.t Backend.Run_state.t) -> sig val equal : Checked.field Cvar0.t diff --git a/src/snarky.ml b/src/snarky.ml index 08d3fbdd2..fadd8c348 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -24,6 +24,7 @@ module Pedersen = Snarky_backendless.Pedersen module Request = Snarky_backendless.Request module Restrict_monad = Snarky_backendless.Restrict_monad module Run_state = Snarky_backendless.Run_state +module Run_state_intf = Snarky_backendless.Run_state_intf module Snark = Snark module Snark0 = Snarky_backendless.Snark0 module Snark_intf = Snarky_backendless.Snark_intf