From 1d84e3718832ad5e99586e49dd137c6c24381b96 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 29 Dec 2024 19:47:48 +0000 Subject: [PATCH 1/5] Hoist Run_state_intf.S --- src/base/dune | 1 + src/base/run_state.mli | 79 +-------------------------------- src/base/run_state_intf.mli | 80 ++++++++++++++++++++++++++++++++++ src/base/snarky_backendless.ml | 1 + src/snarky.ml | 1 + 5 files changed, 84 insertions(+), 78 deletions(-) create mode 100644 src/base/run_state_intf.mli diff --git a/src/base/dune b/src/base/dune index 99cfab1fba..7c4b4a6846 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.mli b/src/base/run_state.mli index 6fe4f85139..82c540bbc0 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 0000000000..0ec4d024ef --- /dev/null +++ b/src/base/run_state_intf.mli @@ -0,0 +1,80 @@ +module type S = sig + 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 +end diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 55b31bf8ba..5a713060b3 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/snarky.ml b/src/snarky.ml index 08d3fbdd24..fadd8c3487 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 From 4927af7f07bcb53b6df3025f53b6cddeeaf7c3bb Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 29 Dec 2024 19:53:26 +0000 Subject: [PATCH 2/5] Move Constraint_system_intf to Constraint_system.S --- src/base/backend_extended.ml | 3 +-- src/base/backend_intf.ml | 30 +----------------------------- src/base/constraint_system.ml | 35 ++++++++++++++++++++++++++++------- 3 files changed, 30 insertions(+), 38 deletions(-) diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index c3d77eac52..07cfd27ea8 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] diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml index bd80cb798b..5f744b28f7 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,5 @@ 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 end diff --git a/src/base/constraint_system.ml b/src/base/constraint_system.ml index 809c2d8372..e12bfd6e7e 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 From ffe5f5db6be512d83e101c4444b8f80d9eb4c05e Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 29 Dec 2024 20:50:17 +0000 Subject: [PATCH 3/5] Lift Checked.Simple.t implementation into functor --- src/base/checked_runner.ml | 77 +++++++++++++++----------------------- 1 file changed, 31 insertions(+), 46 deletions(-) diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 6e481edbc6..7a37e81eeb 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -21,39 +21,6 @@ module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct 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 = - 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 - - let return x : _ t = Pure x - - let map = - `Custom - (fun (x : _ t) ~f : _ t -> - match x with - | Pure a -> - Pure (f a) - | Function g -> - Function - (fun s -> - let s, a = g s in - (s, f a) ) ) - - let bind (x : _ t) ~f : _ t = - match x with - | Pure a -> - f a - | Function g -> - Function - (fun s -> - let s, a = g s in - eval (f a) s ) - end) -end - module Make_checked (Backend : Backend_extended.S) (Types : Types.Types @@ -75,16 +42,35 @@ struct type 'a t = 'a Types.Checked.t - let eval : 'a t -> run_state -> run_state * 'a = Simple.eval + 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.Make (struct - include Types.Checked + type nonrec 'a t = 'a t - let map = `Custom Simple.map + let return x : _ t = Pure x - let bind = Simple.bind + let map = + `Custom + (fun (x : _ t) ~f : _ t -> + match x with + | Pure a -> + Pure (f a) + | Function g -> + Function + (fun s -> + let s, a = g s in + (s, f a) ) ) - let return = Simple.return + let bind (x : _ t) ~f : _ t = + match x with + | Pure a -> + f a + | Function g -> + Function + (fun s -> + let s, a = g s in + eval (f a) s ) end) open Backend @@ -133,7 +119,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 +130,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 +201,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 +246,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 +256,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 +282,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 @@ -364,7 +349,7 @@ struct and type cvar := Backend.Cvar.t end ) - let run = Simple.eval + let run = Checked_runner.eval let dummy_vector = Run_state.Vector.null From 19176cce8185d834ce44de86200e3ac4684c3242 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 29 Dec 2024 22:09:07 +0000 Subject: [PATCH 4/5] Separate Vector.t type out from Run_state_intf.S --- src/base/run_state.ml | 2 +- src/base/run_state_intf.mli | 11 ++++++++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/base/run_state.ml b/src/base/run_state.ml index c0cc1e1a4b..cd148e418b 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_intf.mli b/src/base/run_state_intf.mli index 0ec4d024ef..a0959798fb 100644 --- a/src/base/run_state_intf.mli +++ b/src/base/run_state_intf.mli @@ -1,6 +1,15 @@ +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 = + 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 From c99cd4a38be9c5013f35d0e8bed6cbb29bf7b701 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 29 Dec 2024 23:13:16 +0000 Subject: [PATCH 5/5] Include Run_state in backend --- src/base/backend_extended.ml | 7 ++- src/base/backend_intf.ml | 2 + src/base/checked.ml | 5 +- src/base/checked_intf.ml | 10 ++-- src/base/checked_runner.ml | 34 ++++++++----- src/base/runners.ml | 10 ++-- src/base/snark0.ml | 94 +++++++++++++++++++----------------- src/base/snark_intf.ml | 7 +-- src/base/utils.ml | 6 ++- src/base/utils.mli | 6 ++- 10 files changed, 104 insertions(+), 77 deletions(-) diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index 07cfd27ea8..998a4dd365 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -81,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) : @@ -88,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 @@ -219,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 5f744b28f7..005b3a4649 100644 --- a/src/base/backend_intf.ml +++ b/src/base/backend_intf.ml @@ -6,4 +6,6 @@ module type S = sig val field_size : Bigint.t 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 d6aa33b2c8..631dd9ba3a 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 9d237f91bc..e719fde4cc 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 7a37e81eeb..dc4a08901d 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -7,16 +7,20 @@ 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) @@ -36,11 +40,15 @@ module Make_checked with type field := Backend.Field.t with module Types := Types) = struct - type run_state = Backend.Field.t Run_state.t + type run_state = Backend.Field.t Backend.Run_state.t type field = Backend.Field.t - type 'a t = 'a Types.Checked.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 @@ -291,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 @@ -341,12 +349,14 @@ 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 = Checked_runner.eval @@ -403,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 @@ -426,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/runners.ml b/src/base/runners.ml index 453e87e794..d7111c1552 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 bfd72e48e2..0a49ecf12b 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 caeda75058..4213be5f47 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/utils.ml b/src/base/utils.ml index 944edeb910..4c1bdf5e86 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 0fa8633ebe..05a47d7d36 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