From d3ea356ca1dbdb6cf1560e5dfbe873f850b87947 Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 22 Apr 2025 23:32:10 -0700 Subject: [PATCH 01/17] there is only one project function which is actually used, so remove the 'other one' --- src/base/backend_extended.ml | 35 +---------------------------------- src/base/snark_intf.ml | 3 --- src/intf/field.ml | 2 -- 3 files changed, 1 insertion(+), 39 deletions(-) diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index 38907d0ef..fb0eee865 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -96,7 +96,7 @@ module Make (Backend : Backend_intf.S) : let n = Bigint.of_field x in List.init size_in_bits ~f:(fun i -> Bigint.test_bit n i) - let project_reference = + let project = let rec go x acc = function | [] -> acc @@ -105,30 +105,6 @@ module Make (Backend : Backend_intf.S) : in fun bs -> go Field.one Field.zero bs - let _project bs = - (* todo: 32-bit and ARM support. basically this code needs to always match the loop in the C++ of_data implementation. *) - assert (Sys.word_size = 64 && not Sys.big_endian) ; - let chunks_of n xs = - List.groupi ~break:(fun i _ _ -> Int.equal (i mod n) 0) xs - in - let chunks64 = chunks_of 64 bs in - let z = Char.of_int_exn 0 in - let arr = - Bigstring.init (8 * Backend.Bigint.length_in_bytes) ~f:(fun _ -> z) - in - List.( - iteri ~f:(fun i elt -> - Bigstring.set_int64_t_le arr ~pos:(i * 8) - Int64.( - foldi ~init:zero - ~f:(fun i acc el -> - acc + if el then shift_left one i else zero ) - elt) )) - chunks64 ; - Backend.Bigint.(of_data arr ~bitcount:(List.length bs) |> to_field) - - let project = project_reference - let compare t1 t2 = Bigint.(compare (of_field t1) (of_field t2)) let hash_fold_t s x = @@ -144,15 +120,6 @@ module Make (Backend : Backend_intf.S) : let t_of_sexp = Fn.compose of_bignum_bigint Bignum_bigint.t_of_sexp - let%test_unit "project correctness" = - Quickcheck.test - Quickcheck.Generator.( - small_positive_int >>= fun x -> list_with_length x bool) - ~f:(fun bs -> - [%test_eq: string] - (project bs |> to_string) - (project_reference bs |> to_string) ) - let ( + ) = add let ( * ) = mul diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index ab212ba90..4b23e79f3 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -667,9 +667,6 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) *) val project : bool list -> t - (** [project], but slow. Exposed for benchmarks. *) - val project_reference : bool list -> t - (** Get the least significant bit of a field element. *) val parity : t -> bool diff --git a/src/intf/field.ml b/src/intf/field.ml index b162c46ba..ee0ae8b47 100644 --- a/src/intf/field.ml +++ b/src/intf/field.ml @@ -63,7 +63,5 @@ module type Full = sig val unpack : t -> bool list - val project_reference : bool list -> t - val project : bool list -> t end From 5f1f408a4f0d6eacb2a852ddd3338a6292181708 Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 22 Apr 2025 23:41:20 -0700 Subject: [PATCH 02/17] de-duplicate Constraint_intf module signature --- src/base/backend_extended.ml | 19 ++++------------- src/base/backend_intf.ml | 41 ++++++++++++++++++++++++------------ 2 files changed, 31 insertions(+), 29 deletions(-) diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index fb0eee865..1badf5623 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -25,21 +25,10 @@ module type S = sig with type field := Field.t and type t = Field.t Cvar.t - module Constraint : sig - type t [@@deriving sexp] - - val boolean : Cvar.t -> t - - val equal : Cvar.t -> Cvar.t -> t - - val r1cs : Cvar.t -> Cvar.t -> Cvar.t -> t - - val square : Cvar.t -> Cvar.t -> t - - val eval : t -> (Cvar.t -> Field.t) -> bool - - val log_constraint : t -> (Cvar.t -> Field.t) -> string - end + module Constraint : + Backend_intf.Constraint_intf + with type var := Cvar.t + and type field := Field.t module R1CS_constraint_system : Constraint_system.S diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml index 8dfcfccb3..4fd202177 100644 --- a/src/base/backend_intf.ml +++ b/src/base/backend_intf.ml @@ -38,30 +38,43 @@ module type Cvar_intf = sig val to_constant : t -> field option end -module type S = sig - module Field : Snarky_intf.Field.S +module type Constraint_intf = sig + type var - module Bigint : Snarky_intf.Bigint_intf.Extended with type field := Field.t + type field - val field_size : Bigint.t + type t [@@deriving sexp] - module Cvar : Cvar_intf with type field := Field.t and type t = Field.t Cvar.t + val boolean : var -> t - module Constraint : sig - type t [@@deriving sexp] + val equal : var -> var -> t - val boolean : Cvar.t -> t + val r1cs : var -> var -> var -> t - val equal : Cvar.t -> Cvar.t -> t + val square : var -> var -> t - val r1cs : Cvar.t -> Cvar.t -> Cvar.t -> t + val eval : t -> (var -> field) -> bool - val square : Cvar.t -> Cvar.t -> t + val log_constraint : t -> (var -> field) -> string - val eval : t -> (Cvar.t -> Field.t) -> bool +end - val log_constraint : t -> (Cvar.t -> Field.t) -> string - 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 Cvar : + Cvar_intf + with type field := Field.t + and type t = Field.t Cvar.t + + module Constraint : + Constraint_intf + with type var := Cvar.t + and type field := Field.t module R1CS_constraint_system : Constraint_system.S From 8ff4f74b47bf0d9ceabb919061ca831d4dbdf861 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 23 Apr 2025 11:24:54 -0700 Subject: [PATCH 03/17] remove unused functions from as_prover_0 --- src/base/as_prover0.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml index 553631d93..963de5125 100644 --- a/src/base/as_prover0.ml +++ b/src/base/as_prover0.ml @@ -14,6 +14,11 @@ end) and type field_var = Backend.Cvar.t and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) = struct + (** + `t` is a monad that has access to lookup table `tbl` with type `tbl : var -> field. In Haskell parlance, + `t` simply `Reader (var -> field)`. + *) + type 'a t = 'a Types.As_prover.t let map t ~f tbl = @@ -28,12 +33,6 @@ struct let run t tbl = t tbl - let get_state _tbl s = (s, s) - - let set_state s _tbl _ = (s, ()) - - let modify_state f _tbl s = (f s, ()) - let map2 x y ~f tbl = let x = x tbl in let y = y tbl in From 8e6b064dc6a1db3711a036426390af6078acc369 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 23 Apr 2025 12:50:31 -0700 Subject: [PATCH 04/17] remove unused As_prover module def --- src/base/types.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/base/types.ml b/src/base/types.ml index 37344c3ae..2132a44fb 100644 --- a/src/base/types.ml +++ b/src/base/types.ml @@ -1,7 +1,3 @@ -module As_prover = struct - type ('a, 'f) t = ('f Cvar.t -> 'f) -> 'a -end - module Provider = struct module T = struct (** The different ways to generate a value for the circuit witness. From 5b914f8e37d67a9760ba42668aa73adca34867cf Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 23 Apr 2025 13:04:51 -0700 Subject: [PATCH 05/17] remove unused Ref module in As_prover, remove unused make function in Snark0 --- src/base/snark0.ml | 8 +------- src/base/snark0.mli | 6 +----- 2 files changed, 2 insertions(+), 12 deletions(-) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 6f64ccb1c..75d9f728c 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -58,8 +58,6 @@ struct include As_prover type 'a as_prover = 'a t - - module Ref = Ref end module Handle = struct @@ -1569,8 +1567,4 @@ end type ('field, 'field_var) m = (module Snark_intf.Run with type field = 'field - and type field_var = 'field_var ) - -let make (type field) (module Backend : Backend_intf.S with type Field.t = field) - : (field, field Cvar.t) m = - (module Run.Make (Backend)) + and type field_var = 'field_var ) \ No newline at end of file diff --git a/src/base/snark0.mli b/src/base/snark0.mli index 0ab33b86e..83736f238 100644 --- a/src/base/snark0.mli +++ b/src/base/snark0.mli @@ -42,8 +42,4 @@ end type ('field, 'field_var) m = (module Snark_intf.Run with type field = 'field - and type field_var = 'field_var ) - -val make : - (module Backend_intf.S with type Field.t = 'field) - -> ('field, 'field Cvar.t) m + and type field_var = 'field_var ) \ No newline at end of file From 366cae4c7bb94294f0a6aa0d2ed8e0d4398b7242 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 23 Apr 2025 13:27:36 -0700 Subject: [PATCH 06/17] force dependency of as_prover on as_prover_intf --- src/base/as_prover0.ml | 3 ++- src/base/as_prover_intf.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml index 963de5125..f3618d669 100644 --- a/src/base/as_prover0.ml +++ b/src/base/as_prover0.ml @@ -12,8 +12,9 @@ end) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t - and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) = + and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) : As_prover_intf.Basic with module Types := Types = struct + module Types = Types (** `t` is a monad that has access to lookup table `tbl` with type `tbl : var -> field. In Haskell parlance, `t` simply `Reader (var -> field)`. diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml index b05a53fb7..eb5a2e0ee 100644 --- a/src/base/as_prover_intf.ml +++ b/src/base/as_prover_intf.ml @@ -14,7 +14,7 @@ module type Basic = sig val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t module Provider : sig - type 'a t + type 'a t := 'a Types.Provider.t val run : 'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option From 4873efb2409ae2d080947f1c2d00032d038b8ec6 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 23 Apr 2025 14:35:24 -0700 Subject: [PATCH 07/17] combine as_prover module and interface --- src/base/{as_prover0.ml => as_prover.ml} | 29 +++++++++++++++++++++++- src/base/as_prover_intf.ml | 26 --------------------- src/base/checked.ml | 2 +- src/base/checked_runner.ml | 6 ++--- src/base/runners.ml | 2 +- src/base/snark0.ml | 4 ++-- src/base/snarky_backendless.ml | 3 +-- src/base/utils.ml | 2 +- src/base/utils.mli | 2 +- src/snarky.ml | 3 +-- 10 files changed, 39 insertions(+), 40 deletions(-) rename src/base/{as_prover0.ml => as_prover.ml} (72%) delete mode 100644 src/base/as_prover_intf.ml diff --git a/src/base/as_prover0.ml b/src/base/as_prover.ml similarity index 72% rename from src/base/as_prover0.ml rename to src/base/as_prover.ml index f3618d669..8ae28d522 100644 --- a/src/base/as_prover0.ml +++ b/src/base/as_prover.ml @@ -1,5 +1,32 @@ open Core_kernel +module type Intf = sig + module Types : Types.Types + + type 'a t = 'a Types.As_prover.t + + include Monad_let.S with type 'a t := 'a t + + val run : 'a t -> (Types.field_var -> Types.field) -> 'a + + val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t + + val read_var : Types.field_var -> Types.field t + + val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t + + module Provider : sig + type 'a t := 'a Types.Provider.t + + val run : + 'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option + end + + module Handle : sig + val value : ('var, 'value) Handle.t -> 'value Types.As_prover.t + end +end + module Make (Backend : sig module Field : sig type t @@ -12,7 +39,7 @@ end) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t - and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) : As_prover_intf.Basic with module Types := Types = + and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) : Intf with module Types := Types = struct module Types = Types (** diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml deleted file mode 100644 index eb5a2e0ee..000000000 --- a/src/base/as_prover_intf.ml +++ /dev/null @@ -1,26 +0,0 @@ -module type Basic = sig - module Types : Types.Types - - type 'a t = 'a Types.As_prover.t - - include Monad_let.S with type 'a t := 'a t - - val run : 'a t -> (Types.field_var -> Types.field) -> 'a - - val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t - - val read_var : Types.field_var -> Types.field t - - val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t - - module Provider : sig - type 'a t := 'a Types.Provider.t - - val run : - 'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option - end - - module Handle : sig - val value : ('var, 'value) Handle.t -> 'value Types.As_prover.t - end -end diff --git a/src/base/checked.ml b/src/base/checked.ml index a0a15f929..f9b910411 100644 --- a/src/base/checked.ml +++ b/src/base/checked.ml @@ -6,7 +6,7 @@ module Make (Basic : Checked_intf.Basic with type constraint_ = Backend.Constraint.t with module Types := Types) - (As_prover : As_prover_intf.Basic with module Types := Types) : + (As_prover : As_prover.Intf with module Types := Types) : Checked_intf.S with module Types := Types with type run_state = Basic.run_state diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 1a9f27aac..8d43ae94c 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -33,7 +33,7 @@ module Make_checked ('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 module Types := Types) = + (As_prover : As_prover.Intf with module Types := Types) = struct type run_state = Backend.Run_state.t @@ -297,8 +297,8 @@ struct let clear_constraint_logger () = constraint_logger := None - module As_prover0 = As_prover0.Make (Backend) (Types) - module Checked_runner = Make_checked (Backend) (Types) (As_prover0) + module As_prover = As_prover.Make (Backend) (Types) + module Checked_runner = Make_checked (Backend) (Types) (As_prover) type run_state = Checked_runner.run_state diff --git a/src/base/runners.ml b/src/base/runners.ml index 010d39eba..d36593736 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -9,7 +9,7 @@ module Make with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover_intf.Basic with module Types := Types) + (As_prover : As_prover.Intf with module Types := Types) (Runner : Checked_runner.S with module Types := Types with type constr := Backend.Constraint.t option diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 75d9f728c..05ce6672b 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -16,7 +16,7 @@ module Make_basic with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover_intf.Basic with module Types := Types) + (As_prover : As_prover.Intf with module Types := Types) (Runner : Runner.S with module Types := Types with type constr := Backend.Constraint.t option @@ -648,7 +648,7 @@ module Make (Backend : Backend_intf.S) = struct module Types = Runner.Simple_types (Backend_extended) module Runner0 = Runner.Make (Backend_extended) (Types) module Checked_runner = Runner0.Checked_runner - module As_prover1 = As_prover0.Make (Backend_extended) (Types) + module As_prover1 = As_prover.Make (Backend_extended) (Types) module Checked1 = Checked.Make (Backend_extended) (Types) (Checked_runner) (As_prover1) diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 5a713060b..8f39a0f2a 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -1,5 +1,4 @@ -module As_prover0 = As_prover0 -module As_prover_intf = As_prover_intf +module As_prover = As_prover module Backend_extended = Backend_extended module Backend_intf = Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf diff --git a/src/base/utils.ml b/src/base/utils.ml index 08ccb879a..cb16658c6 100644 --- a/src/base/utils.ml +++ b/src/base/utils.ml @@ -12,7 +12,7 @@ module Make with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover_intf.Basic with module Types := Types) + (As_prover : As_prover.Intf with module Types := Types) (Typ : Snark_intf.Typ_intf with type field := Backend.Field.t and type field_var := Backend.Cvar.t diff --git a/src/base/utils.mli b/src/base/utils.mli index 8707683e8..810bb464e 100644 --- a/src/base/utils.mli +++ b/src/base/utils.mli @@ -11,7 +11,7 @@ module Make : functor with module Types := Types with type run_state = Backend.Run_state.t with type constraint_ = Backend.Constraint.t) - (As_prover : As_prover_intf.Basic with module Types := Types) + (As_prover : As_prover.Intf with module Types := Types) (Typ : Snark_intf.Typ_intf with type field := Backend.Field.t and type field_var := Backend.Cvar.t diff --git a/src/snarky.ml b/src/snarky.ml index fadd8c348..76674710a 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -1,5 +1,4 @@ -module As_prover0 = Snarky_backendless.As_prover0 -module As_prover_intf = Snarky_backendless.As_prover_intf +module As_prover = Snarky_backendless.As_prover module Backend_extended = Snarky_backendless.Backend_extended module Backend_intf = Snarky_backendless.Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf From 452623403c08b3b7cc129a4f0211944a92916c30 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 13:27:44 -0700 Subject: [PATCH 08/17] add cvar.mli and enforce interface --- src/base/backend_extended.ml | 32 +++++++++++++++- src/base/backend_intf.ml | 42 +------------------- src/base/cvar.ml | 74 ++++++++++++++++++++++++------------ src/base/cvar.mli | 62 ++++++++++++++++++++++++++++++ src/base/snark0.ml | 2 - src/base/snark_intf.ml | 3 -- 6 files changed, 144 insertions(+), 71 deletions(-) create mode 100644 src/base/cvar.mli diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index 1badf5623..bd752fd75 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -9,6 +9,36 @@ type 'a json = as 'a + +module type Input_intf = 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 Cvar : + Cvar.Intf + with type field := Field.t + and type t = Field.t Cvar.t + + module Constraint : + Backend_intf.Constraint_intf + with type var := Cvar.t + and type field := Field.t + + 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 type S = sig module Field : Snarky_intf.Field.Full @@ -21,7 +51,7 @@ module type S = sig end module Cvar : - Backend_intf.Cvar_intf + Cvar.Intf with type field := Field.t and type t = Field.t Cvar.t diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml index 4fd202177..be659f4e7 100644 --- a/src/base/backend_intf.ml +++ b/src/base/backend_intf.ml @@ -1,43 +1,3 @@ -module type Cvar_intf = sig - type field - - type t [@@deriving sexp] - - val length : t -> int - - module Unsafe : sig - val of_index : int -> t - end - - val eval : [ `Return_values_will_be_mutated of int -> field ] -> t -> field - - val constant : field -> t - - val to_constant_and_terms : t -> field option * (field * int) list - - val add : t -> t -> t - - val negate : t -> t - - val scale : t -> field -> t - - val sub : t -> t -> t - - val linear_combination : (field * t) list -> t - - val sum : t list -> t - - val ( + ) : t -> t -> t - - val ( - ) : t -> t -> t - - val ( * ) : field -> t -> t - - val var_indices : t -> int list - - val to_constant : t -> field option -end - module type Constraint_intf = sig type var @@ -67,7 +27,7 @@ module type S = sig val field_size : Bigint.t module Cvar : - Cvar_intf + Cvar.Intf with type field := Field.t and type t = Field.t Cvar.t diff --git a/src/base/cvar.ml b/src/base/cvar.ml index 08c7a400c..2508ae1bd 100644 --- a/src/base/cvar.ml +++ b/src/base/cvar.ml @@ -9,6 +9,49 @@ type 'f t = type 'f cvar = 'f t [@@deriving sexp] +module type Intf = sig + type field + + type t = field cvar [@@deriving sexp] + + module Unsafe : sig + val of_index : int -> t + end + + val eval : [ `Return_values_will_be_mutated of int -> field ] -> t -> field + + val constant : field -> t + + val to_constant_and_terms : t -> field option * (field * int) list + + val add : t -> t -> t + + val negate : t -> t + + val scale : t -> field -> t + + val sub : t -> t -> t + + val linear_combination : (field * t) list -> t + + val sum : t list -> t + + val ( + ) : t -> t -> t + + val ( - ) : t -> t -> t + + val ( * ) : field -> t -> t + + val var_indices : t -> int list + + val to_constant : t -> field option +end + + +module Unsafe = struct + let of_index v = Var v +end + let to_constant_and_terms ~equal ~add ~mul ~zero ~one = let rec go scale constant terms = function | Constant c -> @@ -26,18 +69,12 @@ let to_constant_and_terms ~equal ~add ~mul ~zero ~one = let c = if equal c zero then None else Some c in (c, ts) -module Unsafe = struct - let of_index v = Var v -end +module Make (Field : Snarky_intf.Field.Extended) : Intf with type field := Field.t = struct -module Make (Field : Snarky_intf.Field.Extended) = struct type t = Field.t cvar [@@deriving sexp] - let length _ = failwith "TODO" - module Unsafe = Unsafe - let scratch = Field.of_int 0 let eval (`Return_values_will_be_mutated context) t0 = let open Field in @@ -63,23 +100,6 @@ module Make (Field : Snarky_intf.Field.Extended) = struct let constant c = Constant c - let to_constant_and_terms = - let rec go scale constant terms = function - | Constant c -> - (Field.add constant (Field.mul scale c), terms) - | Var v -> - (constant, (scale, v) :: terms) - | Scale (s, t) -> - go (Field.mul s scale) constant terms t - | Add (x1, x2) -> - let c1, terms1 = go scale constant terms x1 in - go scale c1 terms1 x2 - in - fun t -> - let c, ts = go Field.one Field.zero [] t in - let c = if Field.equal c Field.zero then None else Some c in - (c, ts) - let add x y = match (x, y) with | Constant x, _ when Field.(equal x zero) -> @@ -126,6 +146,11 @@ module Make (Field : Snarky_intf.Field.Extended) = struct let negate x = scale x neg_one + let to_constant_and_terms = to_constant_and_terms ~equal:Field.equal ~add:Field.add + ~mul:Field.mul ~zero:Field.zero ~one:Field.one + + + (* let to_json x = let singleton = Map.singleton (module Int) in let join = Map.merge_skewed ~combine:(fun ~key:_ -> Field.add) in @@ -144,6 +169,7 @@ module Make (Field : Snarky_intf.Field.Extended) = struct (List.filter_map (Map.to_alist map) ~f:(fun (i, f) -> if Field.(equal f zero) then None else Some (Int.to_string i, `String (Field.to_string f)) ) ) + *) let var_indices t = let _, terms = to_constant_and_terms t in diff --git a/src/base/cvar.mli b/src/base/cvar.mli new file mode 100644 index 000000000..7d8be58c8 --- /dev/null +++ b/src/base/cvar.mli @@ -0,0 +1,62 @@ +type 'f t = + | Constant of 'f + | Var of int + | Add of 'f t * 'f t + | Scale of 'f * 'f t +[@@deriving sexp] + +type 'f cvar = 'f t [@@deriving sexp] + +val to_constant_and_terms: + equal:('a -> 'a -> bool) -> + add:('a -> 'b -> 'a) -> + mul:('b -> 'b -> 'b) -> + zero:'a -> + one:'b -> + 'b t -> + 'a option * ('b * int) list + +module type Intf = sig + type field + + type t = field cvar [@@deriving sexp] + + module Unsafe : sig + val of_index : int -> t + end + + val eval : [ `Return_values_will_be_mutated of int -> field ] -> t -> field + + val constant : field -> t + + val to_constant_and_terms : t -> field option * (field * int) list + + val add : t -> t -> t + + val negate : t -> t + + val scale : t -> field -> t + + val sub : t -> t -> t + + val linear_combination : (field * t) list -> t + + val sum : t list -> t + + val ( + ) : t -> t -> t + + val ( - ) : t -> t -> t + + val ( * ) : field -> t -> t + + val var_indices : t -> int list + + val to_constant : t -> field option + +end + +module Unsafe : sig + val of_index : int -> 'field t +end + +module Make (Field : Snarky_intf.Field.Extended) : Intf with type field := Field.t \ No newline at end of file diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 05ce6672b..0edd3c387 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -984,8 +984,6 @@ module Run = struct type nonrec t = t - let length = length - let var_indices = var_indices let to_constant_and_terms = to_constant_and_terms diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 4b23e79f3..d9cea8410 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -303,9 +303,6 @@ module type Field_var_intf = sig type t - (** For debug purposes *) - val length : t -> int - val var_indices : t -> int list (** Convert a {!type:t} value to its constituent constant and a list of From 0fa37e22d7235a2f37f4e2afe2e47030282a3d55 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 13:47:17 -0700 Subject: [PATCH 09/17] remove backend_intf file and use the Backend_extended.Input_intf instead. This is what the codebase was already using anyway --- src/base/backend_extended.ml | 26 +++++++++++++++--- src/base/backend_intf.ml | 48 ---------------------------------- src/base/constraint.ml | 23 ++++++++++++++++ src/base/snark.ml | 3 +-- src/base/snark0.ml | 6 ++--- src/base/snark0.mli | 4 +-- src/base/snarky_backendless.ml | 1 - src/snark.ml | 1 - src/snarky.ml | 1 - 9 files changed, 52 insertions(+), 61 deletions(-) delete mode 100644 src/base/backend_intf.ml diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index bd752fd75..870e38af5 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -9,6 +9,26 @@ type 'a json = as 'a +module type Constraint_intf = sig + type var + + type field + + type t [@@deriving sexp] + + val boolean : var -> t + + val equal : var -> var -> t + + val r1cs : var -> var -> var -> t + + val square : var -> var -> t + + val eval : t -> (var -> field) -> bool + + val log_constraint : t -> (var -> field) -> string + +end module type Input_intf = sig module Field : Snarky_intf.Field.S @@ -23,7 +43,7 @@ module type Input_intf = sig and type t = Field.t Cvar.t module Constraint : - Backend_intf.Constraint_intf + Constraint_intf with type var := Cvar.t and type field := Field.t @@ -56,7 +76,7 @@ module type S = sig and type t = Field.t Cvar.t module Constraint : - Backend_intf.Constraint_intf + Constraint_intf with type var := Cvar.t and type field := Field.t @@ -71,7 +91,7 @@ module type S = sig and type constraint_ := Constraint.t end -module Make (Backend : Backend_intf.S) : +module Make (Backend : Input_intf) : S with type Field.t = Backend.Field.t and type Field.Vector.t = Backend.Field.Vector.t diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml deleted file mode 100644 index be659f4e7..000000000 --- a/src/base/backend_intf.ml +++ /dev/null @@ -1,48 +0,0 @@ -module type Constraint_intf = sig - type var - - type field - - type t [@@deriving sexp] - - val boolean : var -> t - - val equal : var -> var -> t - - val r1cs : var -> var -> var -> t - - val square : var -> var -> t - - val eval : t -> (var -> field) -> bool - - val log_constraint : t -> (var -> field) -> string - -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 Cvar : - Cvar.Intf - with type field := Field.t - and type t = Field.t Cvar.t - - module Constraint : - Constraint_intf - with type var := Cvar.t - and type field := Field.t - - 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 diff --git a/src/base/constraint.ml b/src/base/constraint.ml index bf258703c..951f089ea 100644 --- a/src/base/constraint.ml +++ b/src/base/constraint.ml @@ -1,5 +1,6 @@ open Base + type ('var, 'field) basic = .. module Conv (F : sig @@ -174,3 +175,25 @@ module T = struct end include T + + +module type Intf = sig + type var + + type field + + type t [@@deriving sexp] + + val boolean : var -> t + + val equal : var -> var -> t + + val r1cs : var -> var -> var -> t + + val square : var -> var -> t + + val eval : t -> (var -> field) -> bool + + val log_constraint : t -> (var -> field) -> string + +end \ No newline at end of file diff --git a/src/base/snark.ml b/src/base/snark.ml index b1d73e36b..58eaaf2ed 100644 --- a/src/base/snark.ml +++ b/src/base/snark.ml @@ -1,3 +1,2 @@ include Snark0 -module Backend_intf = Backend_intf -module Merkle_tree = Merkle_tree +module Merkle_tree = Merkle_tree \ No newline at end of file diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 0edd3c387..5b1dab23b 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -643,7 +643,7 @@ end (** The main functor for the monadic interface. See [Run.Make] for the same thing but for the imperative interface. *) -module Make (Backend : Backend_intf.S) = struct +module Make (Backend : Backend_extended.Input_intf) = struct module Backend_extended = Backend_extended.Make (Backend) module Types = Runner.Simple_types (Backend_extended) module Runner0 = Runner.Make (Backend_extended) (Types) @@ -692,7 +692,7 @@ module Run = struct let active_functor_id () = List.hd_exn !active_counters - module Make_basic (Backend : Backend_intf.S) = struct + module Make_basic (Backend : Backend_extended.Input_intf) = struct module Snark = Make (Backend) open Backend.Run_state open Snark @@ -1554,7 +1554,7 @@ module Run = struct let run_checked = run end - module Make (Backend : Backend_intf.S) = struct + module Make (Backend : Backend_extended.Input_intf) = struct module Basic = Make_basic (Backend) include Basic module Number = Number.Run.Make (Basic) diff --git a/src/base/snark0.mli b/src/base/snark0.mli index 83736f238..1ee1cd265 100644 --- a/src/base/snark0.mli +++ b/src/base/snark0.mli @@ -19,7 +19,7 @@ val set_eval_constraints : bool -> unit *) exception Runtime_error of string list * exn * string -module Make (Backend : Backend_intf.S) : +module Make (Backend : Backend_extended.Input_intf) : Snark_intf.S with type field = Backend.Field.t and type field_var = Backend.Cvar.t @@ -29,7 +29,7 @@ module Make (Backend : Backend_intf.S) : and type Constraint.t = Backend.Constraint.t module Run : sig - module Make (Backend : Backend_intf.S) : + module Make (Backend : Backend_extended.Input_intf) : Snark_intf.Run with type field = Backend.Field.t and type field_var = Backend.Cvar.t diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 8f39a0f2a..3a022aaf4 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -1,6 +1,5 @@ module As_prover = As_prover module Backend_extended = Backend_extended -module Backend_intf = Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf module Bin_prot_io = Bin_prot_io module Boolean = Boolean diff --git a/src/snark.ml b/src/snark.ml index d012aba75..72199a35f 100644 --- a/src/snark.ml +++ b/src/snark.ml @@ -1,4 +1,3 @@ open Snarky_backendless include Snark0 -module Backend_intf = Backend_intf module Merkle_tree = Merkle_tree diff --git a/src/snarky.ml b/src/snarky.ml index 76674710a..08ec923ba 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -1,6 +1,5 @@ module As_prover = Snarky_backendless.As_prover module Backend_extended = Snarky_backendless.Backend_extended -module Backend_intf = Snarky_backendless.Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf module Bin_prot_io = Snarky_backendless.Bin_prot_io module Boolean = Snarky_backendless.Boolean From e64e7c3d74b6e231b68c3c79a87478ec7fe93695 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 13:53:02 -0700 Subject: [PATCH 10/17] added backend_extended.mli file --- src/base/backend_extended.ml | 8 --- src/base/backend_extended.mli | 92 +++++++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+), 8 deletions(-) create mode 100644 src/base/backend_extended.mli diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml index 870e38af5..4af4a2bfb 100644 --- a/src/base/backend_extended.ml +++ b/src/base/backend_extended.ml @@ -1,14 +1,6 @@ open Core_kernel module Bignum_bigint = Bigint -(** Yojson-compatible JSON type. *) -type 'a json = - [> `String of string - | `Assoc of (string * 'a json) list - | `List of 'a json list ] - as - 'a - module type Constraint_intf = sig type var diff --git a/src/base/backend_extended.mli b/src/base/backend_extended.mli new file mode 100644 index 000000000..136fb2f12 --- /dev/null +++ b/src/base/backend_extended.mli @@ -0,0 +1,92 @@ +module Bignum_bigint = Bigint + +module type Constraint_intf = sig + type var + + type field + + type t [@@deriving sexp] + + val boolean : var -> t + + val equal : var -> var -> t + + val r1cs : var -> var -> var -> t + + val square : var -> var -> t + + val eval : t -> (var -> field) -> bool + + val log_constraint : t -> (var -> field) -> string +end + +module type Input_intf = 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 Cvar : + Cvar.Intf + with type field := Field.t + and type t = Field.t Cvar.t + + module Constraint : + Constraint_intf + with type var := Cvar.t + and type field := Field.t + + 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 type S = sig + module Field : Snarky_intf.Field.Full + + module Bigint : sig + include Snarky_intf.Bigint_intf.Extended with type field := Field.t + + val of_bignum_bigint : Bignum_bigint.t -> t + + val to_bignum_bigint : t -> Bignum_bigint.t + end + + module Cvar : + Cvar.Intf + with type field := Field.t + and type t = Field.t Cvar.t + + module Constraint : + Constraint_intf + with type var := Cvar.t + and type field := Field.t + + 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 : functor + (Backend : Input_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 Cvar.t = Backend.Cvar.t + 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 \ No newline at end of file From 8ac635b837826614a9605f408ef156f9b33c0b51 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 14:25:08 -0700 Subject: [PATCH 11/17] move monad lib out of main snarky lib --- monad_lib/dune | 9 +++++++++ {src/base => monad_lib}/monad_let.ml | 0 monad_lib/monad_lib.ml | 3 +++ {src/base => monad_lib}/monad_sequence.ml | 0 {src/base => monad_lib}/restrict_monad.ml | 0 src/base/as_prover.ml | 4 ++-- src/base/checked_intf.ml | 4 ++-- src/base/checked_runner.ml | 2 +- src/base/dune | 2 +- src/base/snark0.ml | 4 ++-- src/base/snark_intf.ml | 10 +++++----- src/base/snarky_backendless.ml | 3 --- src/base/typ.ml | 2 +- src/snarky.ml | 3 --- 14 files changed, 26 insertions(+), 20 deletions(-) create mode 100644 monad_lib/dune rename {src/base => monad_lib}/monad_let.ml (100%) create mode 100644 monad_lib/monad_lib.ml rename {src/base => monad_lib}/monad_sequence.ml (100%) rename {src/base => monad_lib}/restrict_monad.ml (100%) diff --git a/monad_lib/dune b/monad_lib/dune new file mode 100644 index 000000000..bf8e49682 --- /dev/null +++ b/monad_lib/dune @@ -0,0 +1,9 @@ +(library + (name monad_lib) + (public_name snarky.monad_lib) + (library_flags -linkall) + (inline_tests) + (libraries core_kernel) + (preprocess + (pps ppx_jane ppx_deriving.eq bisect_ppx -- --conditional)) + (synopsis "internal monad types for snarky")) diff --git a/src/base/monad_let.ml b/monad_lib/monad_let.ml similarity index 100% rename from src/base/monad_let.ml rename to monad_lib/monad_let.ml diff --git a/monad_lib/monad_lib.ml b/monad_lib/monad_lib.ml new file mode 100644 index 000000000..3a5eb587c --- /dev/null +++ b/monad_lib/monad_lib.ml @@ -0,0 +1,3 @@ +module Monad_let = Monad_let +module Monad_sequence = Monad_sequence +module Restrict_monad = Restrict_monad \ No newline at end of file diff --git a/src/base/monad_sequence.ml b/monad_lib/monad_sequence.ml similarity index 100% rename from src/base/monad_sequence.ml rename to monad_lib/monad_sequence.ml diff --git a/src/base/restrict_monad.ml b/monad_lib/restrict_monad.ml similarity index 100% rename from src/base/restrict_monad.ml rename to monad_lib/restrict_monad.ml diff --git a/src/base/as_prover.ml b/src/base/as_prover.ml index 8ae28d522..b055d3b2e 100644 --- a/src/base/as_prover.ml +++ b/src/base/as_prover.ml @@ -5,7 +5,7 @@ module type Intf = sig type 'a t = 'a Types.As_prover.t - include Monad_let.S with type 'a t := 'a t + include Monad_lib.Monad_let.S with type 'a t := 'a t val run : 'a t -> (Types.field_var -> Types.field) -> 'a @@ -76,7 +76,7 @@ struct let fields = Array.map ~f:tbl field_vars in value_of_fields (fields, aux) - include Monad_let.Make (struct + include Monad_lib.Monad_let.Make (struct type nonrec 'a t = 'a t let map = `Custom map diff --git a/src/base/checked_intf.ml b/src/base/checked_intf.ml index e7a79d8d7..3497dc1be 100644 --- a/src/base/checked_intf.ml +++ b/src/base/checked_intf.ml @@ -7,7 +7,7 @@ module type Basic = sig type run_state - include Monad_let.S with type 'a t := 'a t + include Monad_lib.Monad_let.S with type 'a t := 'a t val add_constraint : constraint_ -> unit t @@ -44,7 +44,7 @@ module type S = sig type 'a t = 'a Types.Checked.t - include Monad_let.S with type 'a t := 'a t + include Monad_lib.Monad_let.S with type 'a t := 'a t val as_prover : unit Types.As_prover.t -> unit t diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 8d43ae94c..b06bde9fa 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -48,7 +48,7 @@ struct 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 Monad_lib.Monad_let.Make (struct type nonrec 'a t = 'a t let return x : _ t = Pure x diff --git a/src/base/dune b/src/base/dune index 7c4b4a684..78725ea34 100644 --- a/src/base/dune +++ b/src/base/dune @@ -2,7 +2,7 @@ (name snarky_backendless) (public_name snarky.backendless) (inline_tests) - (libraries bitstring_lib core_kernel h_list interval_union snarky_intf + (libraries bitstring_lib core_kernel h_list interval_union monad_lib snarky_intf bignum.bigint) (modules_without_implementation run_state_intf) (preprocess diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 5b1dab23b..ae30e8daa 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -122,7 +122,7 @@ struct (bits, `Success success) module List = - Monad_sequence.List + Monad_lib.Monad_sequence.List (Checked) (struct type t = Boolean.var @@ -131,7 +131,7 @@ struct end) module Array = - Monad_sequence.Array + Monad_lib.Monad_sequence.Array (Checked) (struct type t = Boolean.var diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index d9cea8410..4354bb55a 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -609,16 +609,16 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) ]} *) - include Monad_let.S + include Monad_lib.Monad_let.S module List : - Monad_sequence.S + Monad_lib.Monad_sequence.S with type 'a monad := 'a t and type 'a t = 'a list and type boolean := Boolean.var module Array : - Monad_sequence.S + Monad_lib.Monad_sequence.S with type 'a monad := 'a t and type 'a t = 'a array and type boolean := Boolean.var @@ -699,7 +699,7 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) type 'a as_prover = 'a t - include Monad_let.S with type 'a t := 'a t + include Monad_lib.Monad_let.S with type 'a t := 'a t (** Combine 2 {!type:As_prover.t} blocks using another function. *) val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t @@ -721,7 +721,7 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) { public_inputs : Field.Vector.t; auxiliary_inputs : Field.Vector.t } end - module Let_syntax : Monad_let.Syntax2 with type ('a, 's) t := 'a Checked.t + module Let_syntax : Monad_lib.Monad_let.Syntax2 with type ('a, 's) t := 'a Checked.t (** Utility functions for dealing with lists of bits in the R1CS. *) module Bitstring_checked : sig diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 3a022aaf4..824f0a676 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -14,13 +14,10 @@ module Field_intf = Snarky_intf.Field module H_list = H_list module Handle = Handle module Merkle_tree = Merkle_tree -module Monad_let = Monad_let -module Monad_sequence = Monad_sequence module Number = Number module Number_intf = Number_intf 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 diff --git a/src/base/typ.ml b/src/base/typ.ml index b5228c380..836420cc4 100644 --- a/src/base/typ.ml +++ b/src/base/typ.ml @@ -37,7 +37,7 @@ module type Checked_monad = sig type 'a t = 'a Types.Checked.t - include Monad_let.S with type 'a t := 'a t + include Monad_lib.Monad_let.S with type 'a t := 'a t end module Make diff --git a/src/snarky.ml b/src/snarky.ml index 08ec923ba..ef8540365 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -14,13 +14,10 @@ module Field_intf = Snarky_intf.Field module H_list = H_list module Handle = Snarky_backendless.Handle module Merkle_tree = Snarky_backendless.Merkle_tree -module Monad_let = Snarky_backendless.Monad_let -module Monad_sequence = Snarky_backendless.Monad_sequence module Number = Snarky_backendless.Number module Number_intf = Snarky_backendless.Number_intf 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 From 1dc130cbea85137fa320a000453b2698c1df796b Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 15:02:04 -0700 Subject: [PATCH 12/17] remove unused bin_prot_io module --- src/base/bin_prot_io.ml | 14 -------------- src/base/snarky_backendless.ml | 1 - src/snarky.ml | 1 - 3 files changed, 16 deletions(-) delete mode 100644 src/base/bin_prot_io.ml diff --git a/src/base/bin_prot_io.ml b/src/base/bin_prot_io.ml deleted file mode 100644 index 47d55da82..000000000 --- a/src/base/bin_prot_io.ml +++ /dev/null @@ -1,14 +0,0 @@ -open Core_kernel - -let read m filename = - let buffer = - In_channel.with_file filename ~binary:true ~f:In_channel.input_all - in - Binable.of_string m buffer - -let write m filename ~data = - Out_channel.with_file filename ~binary:true ~f:(fun channel -> - let buffer = - Binable.to_string m data |> Bytes.unsafe_of_string_promise_no_mutation - in - Out_channel.output channel ~buf:buffer ~pos:0 ~len:(Bytes.length buffer) ) diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 824f0a676..49beda60e 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -1,7 +1,6 @@ module As_prover = As_prover module Backend_extended = Backend_extended module Bigint_intf = Snarky_intf.Bigint_intf -module Bin_prot_io = Bin_prot_io module Boolean = Boolean module Checked_intf = Checked_intf module Checked_runner = Checked_runner diff --git a/src/snarky.ml b/src/snarky.ml index ef8540365..35b46c8c3 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -1,7 +1,6 @@ module As_prover = Snarky_backendless.As_prover module Backend_extended = Snarky_backendless.Backend_extended module Bigint_intf = Snarky_intf.Bigint_intf -module Bin_prot_io = Snarky_backendless.Bin_prot_io module Boolean = Snarky_backendless.Boolean module Checked_intf = Snarky_backendless.Checked_intf module Checked_runner = Snarky_backendless.Checked_runner From 6ce97009adbe73f23a21cbbeead907fb9cb74cd5 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 15:07:02 -0700 Subject: [PATCH 13/17] rename backend_extended to backend_intf --- .../{backend_extended.ml => backend_intf.ml} | 0 ...{backend_extended.mli => backend_intf.mli} | 0 src/base/checked.ml | 2 +- src/base/checked_runner.ml | 8 +++---- src/base/runners.ml | 2 +- src/base/snark0.ml | 22 +++++++++---------- src/base/snark0.mli | 4 ++-- src/base/snarky_backendless.ml | 2 +- src/base/utils.ml | 2 +- src/base/utils.mli | 2 +- src/snarky.ml | 2 +- 11 files changed, 23 insertions(+), 23 deletions(-) rename src/base/{backend_extended.ml => backend_intf.ml} (100%) rename src/base/{backend_extended.mli => backend_intf.mli} (100%) diff --git a/src/base/backend_extended.ml b/src/base/backend_intf.ml similarity index 100% rename from src/base/backend_extended.ml rename to src/base/backend_intf.ml diff --git a/src/base/backend_extended.mli b/src/base/backend_intf.mli similarity index 100% rename from src/base/backend_extended.mli rename to src/base/backend_intf.mli diff --git a/src/base/checked.ml b/src/base/checked.ml index f9b910411..dbf42f8c8 100644 --- a/src/base/checked.ml +++ b/src/base/checked.ml @@ -1,7 +1,7 @@ open Core_kernel module Make - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field_var = Backend.Cvar.t) (Basic : Checked_intf.Basic with type constraint_ = Backend.Constraint.t diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index b06bde9fa..502003e8b 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -6,13 +6,13 @@ let eval_constraints = ref true let eval_constraints_ref = eval_constraints -module T (Backend : Backend_extended.S) = struct +module T (Backend : Backend_intf.S) = struct type 'a t = | Pure of 'a | Function of (Backend.Run_state.t -> Backend.Run_state.t * 'a) end -module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct +module Simple_types (Backend : Backend_intf.S) = Types.Make_types (struct type field = Backend.Field.t type field_var = Backend.Cvar.t @@ -23,7 +23,7 @@ module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct end) module Make_checked - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t @@ -274,7 +274,7 @@ module type Run_extras = sig end module Make - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t diff --git a/src/base/runners.ml b/src/base/runners.ml index d36593736..902bd426b 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -1,7 +1,7 @@ open Core_kernel module Make - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index ae30e8daa..ae3b4fd1b 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -8,7 +8,7 @@ module Runner = Checked_runner let set_eval_constraints b = Runner.eval_constraints := b module Make_basic - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t) @@ -643,14 +643,14 @@ end (** The main functor for the monadic interface. See [Run.Make] for the same thing but for the imperative interface. *) -module Make (Backend : Backend_extended.Input_intf) = struct - module Backend_extended = Backend_extended.Make (Backend) - module Types = Runner.Simple_types (Backend_extended) - module Runner0 = Runner.Make (Backend_extended) (Types) +module Make (Backend : Backend_intf.Input_intf) = struct + module Backend_intf = Backend_intf.Make (Backend) + module Types = Runner.Simple_types (Backend_intf) + module Runner0 = Runner.Make (Backend_intf) (Types) module Checked_runner = Runner0.Checked_runner - module As_prover1 = As_prover.Make (Backend_extended) (Types) + module As_prover1 = As_prover.Make (Backend_intf) (Types) module Checked1 = - Checked.Make (Backend_extended) (Types) (Checked_runner) (As_prover1) + Checked.Make (Backend_intf) (Types) (Checked_runner) (As_prover1) module Checked_for_basic = struct include ( @@ -659,7 +659,7 @@ module Make (Backend : Backend_extended.Input_intf) = struct with module Types := Types with type 'a t := 'a Checked1.t and type run_state = Backend.Run_state.t - and type constraint_ = Backend_extended.Constraint.t ) + and type constraint_ = Backend_intf.Constraint.t ) type 'a t = 'a Types.Checked.t @@ -667,7 +667,7 @@ module Make (Backend : Backend_extended.Input_intf) = struct end module Basic = - Make_basic (Backend_extended) (Types) (Checked_for_basic) (As_prover1) + Make_basic (Backend_intf) (Types) (Checked_for_basic) (As_prover1) (Runner0) include Basic module Number = Number.Make (Basic) @@ -692,7 +692,7 @@ module Run = struct let active_functor_id () = List.hd_exn !active_counters - module Make_basic (Backend : Backend_extended.Input_intf) = struct + module Make_basic (Backend : Backend_intf.Input_intf) = struct module Snark = Make (Backend) open Backend.Run_state open Snark @@ -1554,7 +1554,7 @@ module Run = struct let run_checked = run end - module Make (Backend : Backend_extended.Input_intf) = struct + module Make (Backend : Backend_intf.Input_intf) = struct module Basic = Make_basic (Backend) include Basic module Number = Number.Run.Make (Basic) diff --git a/src/base/snark0.mli b/src/base/snark0.mli index 1ee1cd265..a3ba48000 100644 --- a/src/base/snark0.mli +++ b/src/base/snark0.mli @@ -19,7 +19,7 @@ val set_eval_constraints : bool -> unit *) exception Runtime_error of string list * exn * string -module Make (Backend : Backend_extended.Input_intf) : +module Make (Backend : Backend_intf.Input_intf) : Snark_intf.S with type field = Backend.Field.t and type field_var = Backend.Cvar.t @@ -29,7 +29,7 @@ module Make (Backend : Backend_extended.Input_intf) : and type Constraint.t = Backend.Constraint.t module Run : sig - module Make (Backend : Backend_extended.Input_intf) : + module Make (Backend : Backend_intf.Input_intf) : Snark_intf.Run with type field = Backend.Field.t and type field_var = Backend.Cvar.t diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 49beda60e..402eae73b 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -1,5 +1,5 @@ module As_prover = As_prover -module Backend_extended = Backend_extended +module Backend_intf = Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf module Boolean = Boolean module Checked_intf = Checked_intf diff --git a/src/base/utils.ml b/src/base/utils.ml index cb16658c6..b5c0cd902 100644 --- a/src/base/utils.ml +++ b/src/base/utils.ml @@ -4,7 +4,7 @@ module Runner = Checked_runner let set_eval_constraints b = Runner.eval_constraints := b module Make - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t) diff --git a/src/base/utils.mli b/src/base/utils.mli index 810bb464e..e1cd093cc 100644 --- a/src/base/utils.mli +++ b/src/base/utils.mli @@ -3,7 +3,7 @@ module Runner = Checked_runner val set_eval_constraints : bool -> unit module Make : functor - (Backend : Backend_extended.S) + (Backend : Backend_intf.S) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t) diff --git a/src/snarky.ml b/src/snarky.ml index 35b46c8c3..51e0436ac 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -1,5 +1,5 @@ module As_prover = Snarky_backendless.As_prover -module Backend_extended = Snarky_backendless.Backend_extended +module Backend_intf = Snarky_backendless.Backend_intf module Bigint_intf = Snarky_intf.Bigint_intf module Boolean = Snarky_backendless.Boolean module Checked_intf = Snarky_backendless.Checked_intf From f7445b266eadcceb43d67202fe2d3a216dbc73d9 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 15:33:41 -0700 Subject: [PATCH 14/17] add back as_prover_intf --- src/base/as_prover.ml | 29 +---------------------------- src/base/as_prover_intf.ml | 26 ++++++++++++++++++++++++++ src/base/checked.ml | 2 +- src/base/checked_runner.ml | 2 +- src/base/runners.ml | 2 +- src/base/snark0.ml | 2 +- src/base/utils.ml | 2 +- src/base/utils.mli | 2 +- 8 files changed, 33 insertions(+), 34 deletions(-) create mode 100644 src/base/as_prover_intf.ml diff --git a/src/base/as_prover.ml b/src/base/as_prover.ml index b055d3b2e..40464b0bd 100644 --- a/src/base/as_prover.ml +++ b/src/base/as_prover.ml @@ -1,32 +1,5 @@ open Core_kernel -module type Intf = sig - module Types : Types.Types - - type 'a t = 'a Types.As_prover.t - - include Monad_lib.Monad_let.S with type 'a t := 'a t - - val run : 'a t -> (Types.field_var -> Types.field) -> 'a - - val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t - - val read_var : Types.field_var -> Types.field t - - val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t - - module Provider : sig - type 'a t := 'a Types.Provider.t - - val run : - 'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option - end - - module Handle : sig - val value : ('var, 'value) Handle.t -> 'value Types.As_prover.t - end -end - module Make (Backend : sig module Field : sig type t @@ -39,7 +12,7 @@ end) (Types : Types.Types with type field = Backend.Field.t and type field_var = Backend.Cvar.t - and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) : Intf with module Types := Types = + and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) : As_prover_intf.S with module Types := Types = struct module Types = Types (** diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml new file mode 100644 index 000000000..66ea678cf --- /dev/null +++ b/src/base/as_prover_intf.ml @@ -0,0 +1,26 @@ +module type S = sig + module Types : Types.Types + + type 'a t = 'a Types.As_prover.t + + include Monad_lib.Monad_let.S with type 'a t := 'a t + + val run : 'a t -> (Types.field_var -> Types.field) -> 'a + + val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t + + val read_var : Types.field_var -> Types.field t + + val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t + + module Provider : sig + type 'a t := 'a Types.Provider.t + + val run : + 'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option + end + + module Handle : sig + val value : ('var, 'value) Handle.t -> 'value Types.As_prover.t + end +end diff --git a/src/base/checked.ml b/src/base/checked.ml index dbf42f8c8..c72ff7dc5 100644 --- a/src/base/checked.ml +++ b/src/base/checked.ml @@ -6,7 +6,7 @@ module Make (Basic : Checked_intf.Basic with type constraint_ = Backend.Constraint.t with module Types := Types) - (As_prover : As_prover.Intf with module Types := Types) : + (As_prover : As_prover_intf.S with module Types := Types) : Checked_intf.S with module Types := Types with type run_state = Basic.run_state diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 502003e8b..dd445aa4d 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -33,7 +33,7 @@ module Make_checked ('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 with module Types := Types) = + (As_prover : As_prover_intf.S with module Types := Types) = struct type run_state = Backend.Run_state.t diff --git a/src/base/runners.ml b/src/base/runners.ml index 902bd426b..4d4a99bb4 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -9,7 +9,7 @@ module Make with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover.Intf with module Types := Types) + (As_prover : As_prover_intf.S with module Types := Types) (Runner : Checked_runner.S with module Types := Types with type constr := Backend.Constraint.t option diff --git a/src/base/snark0.ml b/src/base/snark0.ml index ae3b4fd1b..a2137d49e 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -16,7 +16,7 @@ module Make_basic with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover.Intf with module Types := Types) + (As_prover : As_prover_intf.S with module Types := Types) (Runner : Runner.S with module Types := Types with type constr := Backend.Constraint.t option diff --git a/src/base/utils.ml b/src/base/utils.ml index b5c0cd902..abff98cc8 100644 --- a/src/base/utils.ml +++ b/src/base/utils.ml @@ -12,7 +12,7 @@ module Make with module Types := Types with type run_state = Backend.Run_state.t and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover.Intf with module Types := Types) + (As_prover : As_prover_intf.S with module Types := Types) (Typ : Snark_intf.Typ_intf with type field := Backend.Field.t and type field_var := Backend.Cvar.t diff --git a/src/base/utils.mli b/src/base/utils.mli index e1cd093cc..2f8a5baa3 100644 --- a/src/base/utils.mli +++ b/src/base/utils.mli @@ -11,7 +11,7 @@ module Make : functor with module Types := Types with type run_state = Backend.Run_state.t with type constraint_ = Backend.Constraint.t) - (As_prover : As_prover.Intf with module Types := Types) + (As_prover : As_prover_intf.S with module Types := Types) (Typ : Snark_intf.Typ_intf with type field := Backend.Field.t and type field_var := Backend.Cvar.t From 76af7fff8765beb988e3b7dccc1f4fa92edb887d Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 15:40:21 -0700 Subject: [PATCH 15/17] use as_prover_intf at the right level --- src/base/checked_runner.ml | 4 ++-- src/base/snark0.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index dd445aa4d..2944bb123 100644 --- a/src/base/checked_runner.ml +++ b/src/base/checked_runner.ml @@ -285,7 +285,8 @@ module Make and type ('var, 'value) Typ.typ = ('var, 'value) Simple_types(Backend).Typ.typ and type ('request, 'compute) Provider.provider = - ('request, 'compute) Simple_types(Backend).Provider.provider) = + ('request, 'compute) Simple_types(Backend).Provider.provider) + (As_prover : As_prover_intf.S with module Types := Types) = struct open Backend @@ -297,7 +298,6 @@ struct let clear_constraint_logger () = constraint_logger := None - module As_prover = As_prover.Make (Backend) (Types) module Checked_runner = Make_checked (Backend) (Types) (As_prover) type run_state = Checked_runner.run_state diff --git a/src/base/snark0.ml b/src/base/snark0.ml index a2137d49e..a53172d7d 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -646,9 +646,9 @@ end module Make (Backend : Backend_intf.Input_intf) = struct module Backend_intf = Backend_intf.Make (Backend) module Types = Runner.Simple_types (Backend_intf) - module Runner0 = Runner.Make (Backend_intf) (Types) - module Checked_runner = Runner0.Checked_runner module As_prover1 = As_prover.Make (Backend_intf) (Types) + module Runner0 = Runner.Make (Backend_intf) (Types) (As_prover1) + module Checked_runner = Runner0.Checked_runner module Checked1 = Checked.Make (Backend_intf) (Types) (Checked_runner) (As_prover1) From 917c16dea920c562d5a2d43759693493cac4aec7 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 15:48:27 -0700 Subject: [PATCH 16/17] created checked.mli --- src/base/checked.ml | 6 +----- src/base/checked.mli | 12 ++++++++++++ 2 files changed, 13 insertions(+), 5 deletions(-) create mode 100644 src/base/checked.mli diff --git a/src/base/checked.ml b/src/base/checked.ml index c72ff7dc5..d86f6c3df 100644 --- a/src/base/checked.ml +++ b/src/base/checked.ml @@ -6,11 +6,7 @@ module Make (Basic : Checked_intf.Basic with type constraint_ = Backend.Constraint.t with module Types := Types) - (As_prover : As_prover_intf.S with module Types := Types) : - Checked_intf.S - with module Types := Types - with type run_state = Basic.run_state - and type constraint_ = Basic.constraint_ = struct + (As_prover : As_prover_intf.S with module Types := Types) = struct include Basic let request_witness (typ : ('var, 'value) Types.Typ.t) diff --git a/src/base/checked.mli b/src/base/checked.mli new file mode 100644 index 000000000..b4369e5b0 --- /dev/null +++ b/src/base/checked.mli @@ -0,0 +1,12 @@ + +module Make + (Backend : Backend_intf.S) + (Types : Types.Types with type field_var = Backend.Cvar.t) + (Basic : Checked_intf.Basic + with type constraint_ = Backend.Constraint.t + with module Types := Types) + (As_prover : As_prover_intf.S with module Types := Types) : + Checked_intf.S + with module Types := Types + with type run_state = Basic.run_state + and type constraint_ = Basic.constraint_ \ No newline at end of file From 4b8e5e04c492b03f2eadea1b3a8776a19d8e55c6 Mon Sep 17 00:00:00 2001 From: martyall Date: Thu, 24 Apr 2025 16:09:26 -0700 Subject: [PATCH 17/17] re-export modules in only one place --- src/base/snark.ml | 1570 +++++++++++++++++++++++++++- src/base/{snark0.mli => snark.mli} | 0 src/base/snark0.ml | 1568 --------------------------- src/base/snarky_backendless.ml | 1 - src/snark.ml | 3 - src/snarky.ml | 3 +- 6 files changed, 1569 insertions(+), 1576 deletions(-) rename src/base/{snark0.mli => snark.mli} (100%) delete mode 100644 src/base/snark0.ml delete mode 100644 src/snark.ml diff --git a/src/base/snark.ml b/src/base/snark.ml index 58eaaf2ed..a53172d7d 100644 --- a/src/base/snark.ml +++ b/src/base/snark.ml @@ -1,2 +1,1568 @@ -include Snark0 -module Merkle_tree = Merkle_tree \ No newline at end of file +open Core_kernel +module Bignum_bigint = Bigint + +exception Runtime_error of string list * exn * string + +module Runner = Checked_runner + +let set_eval_constraints b = Runner.eval_constraints := b + +module Make_basic + (Backend : Backend_intf.S) + (Types : Types.Types + with type field = Backend.Field.t + and type field_var = Backend.Cvar.t) + (Checked : Checked_intf.Extended + with module Types := Types + with type run_state = Backend.Run_state.t + and type constraint_ = Backend.Constraint.t) + (As_prover : As_prover_intf.S with module Types := Types) + (Runner : Runner.S + with module Types := Types + with type constr := Backend.Constraint.t option + and type r1cs := Backend.R1CS_constraint_system.t + and type run_state = Backend.Run_state.t) = +struct + open Backend + + type field_var = Cvar.t + + module Typ = struct + include Types.Typ + module T = Typ.Make (Types) (Checked) + include T.T + + type ('var, 'value) t = ('var, 'value) T.t + + let unit : (unit, unit) t = unit () + + let field : (Cvar.t, Field.t) t = field () + end + + include Runners.Make (Backend) (Types) (Checked) (As_prover) (Runner) + module Bigint = Bigint + module Field0 = Field + module Cvar = Cvar + module Constraint = Constraint + + module Handler = struct + type t = Request.request -> Request.response + end + + let constant (Typ typ : _ Typ.t) x = + let fields, aux = typ.value_to_fields x in + let field_vars = Array.map fields ~f:(fun x -> Cvar.constant x) in + typ.var_of_fields (field_vars, aux) + + module As_prover = struct + include As_prover + + type 'a as_prover = 'a t + end + + module Handle = struct + include Handle + + let value = As_prover.Handle.value + end + + module Checked = struct + include ( + Checked : + Checked_intf.Extended + with module Types := Types + with type run_state = Backend.Run_state.t + and type constraint_ = Backend.Constraint.t ) + + let perform req = request_witness Typ.unit req + + module Runner = Runner + include Utils.Make (Backend) (Types) (Checked) (As_prover) (Typ) (Runner) + + module Control = struct end + + let two_to_the n = + let rec go acc i = + if i = 0 then acc else go (Field0.add acc acc) (i - 1) + in + go Field0.one n + + type _ Request.t += Choose_preimage : Field.t * int -> bool list Request.t + + let choose_preimage_unchecked v ~length = + exists + (Typ.list Boolean.typ ~length) + ~request: + As_prover.(map (read_var v) ~f:(fun x -> Choose_preimage (x, length))) + ~compute: + (let open As_prover.Let_syntax in + let%map x = As_prover.read_var v in + let x = Bigint.of_field x in + List.init length ~f:(fun i -> Bigint.test_bit x i)) + + let packing_sum (bits : Boolean.var list) = + let ts, _ = + List.fold_left bits ~init:([], Field.one) ~f:(fun (acc, c) v -> + ((c, (v :> Cvar.t)) :: acc, Field.add c c) ) + in + Cvar.linear_combination ts + + let choose_preimage (v : Cvar.t) ~length : Boolean.var list t = + let open Let_syntax in + let%bind bits = choose_preimage_unchecked v ~length in + let lc = packing_sum bits in + let%map () = assert_r1cs lc (Cvar.constant Field.one) v in + bits + + let choose_preimage_flagged (v : Cvar.t) ~length = + let open Let_syntax in + let%bind bits = choose_preimage_unchecked v ~length in + let lc = packing_sum bits in + let%map success = equal lc v in + (bits, `Success success) + + module List = + Monad_lib.Monad_sequence.List + (Checked) + (struct + type t = Boolean.var + + include Boolean + end) + + module Array = + Monad_lib.Monad_sequence.Array + (Checked) + (struct + type t = Boolean.var + + let any = Boolean.Array.any + + let all = Boolean.Array.all + end) + end + + module Cvar1 = struct + include Cvar + + let project = + let two = Field.of_int 2 in + fun (vars : Checked.Boolean.var list) -> + let rec go res = function + | [] -> + res + | v :: vs -> + go Cvar.(add v (Cvar.scale res two)) vs + in + match List.rev (vars :> Cvar.t list) with + | [] -> + Cvar.constant Field.zero + | v :: vs -> + go v vs + + let pack vars = + assert (List.length vars < Field.size_in_bits) ; + project vars + + let unpack v ~length = + assert (length < Field.size_in_bits) ; + Checked.choose_preimage v ~length + + let unpack_flagged v ~length = + assert (length < Field.size_in_bits) ; + Checked.choose_preimage_flagged v ~length + end + + module Field = struct + include Field0 + + let gen = + Quickcheck.Generator.map + Bignum_bigint.(gen_incl zero (size - one)) + ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) + + let gen_incl lo hi = + let lo_bigint = Bigint.(to_bignum_bigint @@ of_field lo) in + let hi_bigint = Bigint.(to_bignum_bigint @@ of_field hi) in + Quickcheck.Generator.map + Bignum_bigint.(gen_incl lo_bigint hi_bigint) + ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) + + let gen_uniform = + Quickcheck.Generator.map + Bignum_bigint.(gen_uniform_incl zero (size - one)) + ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) + + let gen_uniform_incl lo hi = + let lo_bigint = Bigint.(to_bignum_bigint @@ of_field lo) in + let hi_bigint = Bigint.(to_bignum_bigint @@ of_field hi) in + Quickcheck.Generator.map + Bignum_bigint.(gen_uniform_incl lo_bigint hi_bigint) + ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) + + let typ = Typ.field + + module Var = Cvar1 + + let parity x = Bigint.(test_bit (of_field x) 0) + + module Checked = struct + include Cvar1 + + let equal = Checked.equal + + let mul x y = Checked.mul ~label:"Field.Checked.mul" x y + + let square x = Checked.square ~label:"Field.Checked.square" x + + let div x y = Checked.div ~label:"Field.Checked.div" x y + + let inv x = Checked.inv ~label:"Field.Checked.inv" x + + let sqrt (x : Cvar.t) : Cvar.t Checked.t = + match Cvar.to_constant x with + | Some x -> + Checked.return (Cvar.constant (Field.sqrt x)) + | _ -> + let open Checked in + let open Let_syntax in + let%bind y = + exists ~compute:As_prover.(map (read_var x) ~f:Field.sqrt) typ + in + let%map () = assert_square y x in + y + + let quadratic_nonresidue = + lazy + (let rec go i = + let x = Field.of_int i in + if not (Field.is_square x) then x else go Int.(i + 1) + in + go 2 ) + + (* The trick here is the following. + + Let beta be a known non-square. + + x is not a square iff beta*x is a square + + So we guess the result [is_square] and y a sqrt of one of {x, beta*x} and assert + + y * y = is_square * x + (1 - is_square) * (beta * x) + + which, letting B = beta*x holds iff + + y * y + = is_square * x + B - is_square * B + = is_square * (x - B) + B + *) + let sqrt_check x = + let open Checked in + let open Let_syntax in + let%bind is_square = + exists + ~compute:As_prover.(map (read_var x) ~f:Field.is_square) + Boolean.typ + in + let%bind y = + exists typ + ~compute: + As_prover.( + Let_syntax.( + let%map is_square = read Boolean.typ is_square + and x = read_var x in + if is_square then Field.sqrt x + else Field.(sqrt (Lazy.force quadratic_nonresidue * x)))) + in + let b = scale x (Lazy.force quadratic_nonresidue) in + let%bind t = mul (is_square :> Var.t) (x - b) in + let%map () = assert_square y (t + b) in + (y, is_square) + + let is_square x = + let open Checked.Let_syntax in + let%map _, b = sqrt_check x in + b + + let%test_unit "is_square" = + let x = Field.random () in + let typf = Typ.field in + let x2 = Field.square x in + assert (Field.(equal (x * x) x2)) ; + let run elt = + let answer = + run_and_check + (Checked.map + ~f:(As_prover.read Checked.Boolean.typ) + Checked.( + Let_syntax.( + let%bind x = exists typf ~compute:(As_prover.return elt) in + is_square x)) ) + |> Or_error.ok_exn + in + answer + in + assert (run x2) ; + assert (not (run (Field.mul (Lazy.force quadratic_nonresidue) x2))) + + let choose_preimage_var = Checked.choose_preimage + + type comparison_result = + { less : Checked.Boolean.var; less_or_equal : Checked.Boolean.var } + + let if_ = Checked.if_ + + let compare ~bit_length a b = + (* Overview of the logic: + let n = bit_length + We have 0 <= a < 2^n, 0 <= b < 2^n, and so + -2^n < b - a < 2^n + If (b - a) >= 0, then + 2^n <= 2^n + b - a < 2^{n+1}, + and so the n-th bit must be set. + If (b - a) < 0 then + 0 < 2^n + b - a < 2^n + and so the n-th bit must not be set. + Thus, we can use the n-th bit of 2^n + b - a to determine whether + (b - a) >= 0 <-> a <= b. + + We also need that the maximum value + 2^n + (2^n - 1) - 0 = 2^{n+1} - 1 + fits inside the field, so for the max field element f, + 2^{n+1} - 1 <= f -> n+1 <= log2(f) = size_in_bits - 1 + *) + assert (Int.(bit_length <= size_in_bits - 2)) ; + let open Checked in + let open Let_syntax in + [%with_label_ "compare"] (fun () -> + let alpha_packed = + Cvar.(constant (two_to_the bit_length) + b - a) + in + let%bind alpha = unpack alpha_packed ~length:Int.(bit_length + 1) in + let prefix, less_or_equal = + match Core_kernel.List.split_n alpha bit_length with + | p, [ l ] -> + (p, l) + | _ -> + failwith "compare: Invalid alpha" + in + let%bind not_all_zeros = Boolean.any prefix in + let%map less = Boolean.(less_or_equal && not_all_zeros) in + { less; less_or_equal } ) + + module Assert = struct + let lt ~bit_length (x : Cvar.t) (y : Cvar.t) = + match (Cvar.to_constant x, Cvar.to_constant y) with + | Some x, Some y -> + assert (Field.compare x y < 0) ; + Checked.return () + | _ -> + let open Checked in + let open Let_syntax in + let%bind { less; _ } = compare ~bit_length x y in + Boolean.Assert.is_true less + + let lte ~bit_length (x : Cvar.t) (y : Cvar.t) = + match (Cvar.to_constant x, Cvar.to_constant y) with + | Some x, Some y -> + assert (Field.compare x y <= 0) ; + Checked.return () + | _ -> + let open Checked in + let open Let_syntax in + let%bind { less_or_equal; _ } = compare ~bit_length x y in + Boolean.Assert.is_true less_or_equal + + let gt ~bit_length x y = lt ~bit_length y x + + let gte ~bit_length x y = lte ~bit_length y x + + let non_zero (v : Cvar.t) = + match Cvar.to_constant v with + | Some v -> + if Field.(equal zero v) then + failwithf "assert_non_zero: failed on constant %s" + (Field.to_string v) () ; + Checked.return () + | _ -> + Checked.assert_non_zero v + + let equal x y = Checked.assert_equal x y + + let not_equal (x : t) (y : t) = + match (Cvar.to_constant x, Cvar.to_constant y) with + | Some x, Some y -> + if Field.(equal x y) then + failwithf "not_equal: failed on constants %s and %s" + (Field.to_string x) (Field.to_string y) () ; + Checked.return () + | _, _ -> + Checked.with_label "Checked.Assert.not_equal" (fun () -> + non_zero (sub x y) ) + end + + let lt_bitstring_value = + let module Boolean = Checked.Boolean in + let module Expr = struct + module Binary = struct + type 'a t = Lit of 'a | And of 'a * 'a t | Or of 'a * 'a t + end + + module Nary = struct + type 'a t = Lit of 'a | And of 'a t list | Or of 'a t list + + let rec of_binary : 'a Binary.t -> 'a t = function + | Lit x -> + Lit x + | And (x, And (y, t)) -> + And [ Lit x; Lit y; of_binary t ] + | Or (x, Or (y, t)) -> + Or [ Lit x; Lit y; of_binary t ] + | And (x, t) -> + And [ Lit x; of_binary t ] + | Or (x, t) -> + Or [ Lit x; of_binary t ] + + let rec eval = + let open Checked.Let_syntax in + function + | Lit x -> + return x + | And xs -> + Checked.List.map xs ~f:eval >>= Boolean.all + | Or xs -> + Checked.List.map xs ~f:eval >>= Boolean.any + end + end in + let rec lt_binary xs ys : Boolean.var Expr.Binary.t = + match (xs, ys) with + | [], [] -> + Lit Boolean.false_ + | [ _x ], [ false ] -> + Lit Boolean.false_ + | [ x ], [ true ] -> + Lit (Boolean.not x) + | [ x1; _x2 ], [ true; false ] -> + Lit (Boolean.not x1) + | [ _x1; _x2 ], [ false; false ] -> + Lit Boolean.false_ + | x :: xs, false :: ys -> + And (Boolean.not x, lt_binary xs ys) + | x :: xs, true :: ys -> + Or (Boolean.not x, lt_binary xs ys) + | _ :: _, [] | [], _ :: _ -> + failwith "lt_bitstring_value: Got unequal length strings" + in + fun (xs : Boolean.var Bitstring_lib.Bitstring.Msb_first.t) + (ys : bool Bitstring_lib.Bitstring.Msb_first.t) -> + let open Expr.Nary in + eval + (of_binary (lt_binary (xs :> Boolean.var list) (ys :> bool list))) + + let field_size_bits = + lazy + ( List.init Field.size_in_bits ~f:(fun i -> + Z.testbit + (Bignum_bigint.to_zarith_bigint Field.size) + Stdlib.(Field.size_in_bits - 1 - i) ) + |> Bitstring_lib.Bitstring.Msb_first.of_list ) + + let unpack_full x = + let module Bitstring = Bitstring_lib.Bitstring in + let open Checked.Let_syntax in + let%bind res = + choose_preimage_var x ~length:Field.size_in_bits + >>| Bitstring.Lsb_first.of_list + in + let%map () = + lt_bitstring_value + (Bitstring.Msb_first.of_lsb_first res) + (Lazy.force field_size_bits) + >>= Checked.Boolean.Assert.is_true + in + res + + let parity ?length x = + let open Checked in + let unpack = + let unpack_full x = + unpack_full x >>| Bitstring_lib.Bitstring.Lsb_first.to_list + in + match length with + | None -> + unpack_full + | Some length -> + let length = Int.min length Field.size_in_bits in + if Int.equal length Field.size_in_bits then unpack_full + else choose_preimage_var ~length + in + unpack x >>| Base.List.hd_exn + end + end + + module Bitstring_checked = struct + type t = Checked.Boolean.var list + + let lt_value = Field.Checked.lt_bitstring_value + + let chunk_for_equality (t1 : t) (t2 : t) = + let chunk_size = Field.size_in_bits - 1 in + let rec go acc t1 t2 = + match (t1, t2) with + | [], [] -> + acc + | _, _ -> + let t1_a, t1_b = List.split_n t1 chunk_size in + let t2_a, t2_b = List.split_n t2 chunk_size in + go ((t1_a, t2_a) :: acc) t1_b t2_b + in + go [] t1 t2 + + let equal t1 t2 = + let open Checked in + all + (Base.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> + equal (Cvar1.pack x1) (Cvar1.pack x2) ) ) + >>= Boolean.all + + let equal_expect_true t1 t2 = + let open Checked in + all + (Core_kernel.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> + (* Inlined [Field.equal], but skip creating the field element for + this chunk if possible. + *) + let z = Cvar1.(pack x1 - pack x2) in + let%bind r, inv = + exists + Typ.(field * field) + ~compute: + As_prover.( + match + Core_kernel.List.map2 x1 x2 ~f:(fun x1 x2 -> + let%map x1 = read_var (x1 :> Cvar.t) + and x2 = read_var (x2 :> Cvar.t) in + Field.equal x1 x2 ) + with + | Ok res -> + let%bind res = all res in + if Core_kernel.List.for_all ~f:Fn.id res then + return (Field.one, Field.zero) + else equal_vars z + | _ -> + equal_vars z) + in + let%map () = equal_constraints z inv r in + Boolean.Unsafe.of_cvar r ) ) + >>= Boolean.all + + module Assert = struct + let equal t1 t2 = + let open Checked in + Base.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> + Backend.Constraint.equal (Cvar1.pack x1) (Cvar1.pack x2) ) + |> assert_all + end + end + + let%test_unit "lt_bitstring_value" = + let gen = + let open Quickcheck.Generator in + let open Let_syntax in + let%bind length = small_positive_int in + let%map x = list_with_length length bool + and y = list_with_length length bool in + (x, y) + in + Quickcheck.test gen ~f:(fun (x, y) -> + let correct_answer = [%compare: bool list] x y < 0 in + let lt = + run_and_check + (Checked.map + ~f:(As_prover.read Checked.Boolean.typ) + (Field.Checked.lt_bitstring_value + (Bitstring_lib.Bitstring.Msb_first.of_list + (List.map ~f:Checked.(constant Boolean.typ) x) ) + (Bitstring_lib.Bitstring.Msb_first.of_list y) ) ) + |> Or_error.ok_exn + in + assert (Bool.equal lt correct_answer) ) + + include Checked + + let%snarkydef_ if_ (b : Boolean.var) ~typ:(Typ typ : ('var, _) Typ.t) + ~(then_ : 'var) ~(else_ : 'var) = + let then_, then_aux = typ.var_to_fields then_ in + let else_, else_aux = typ.var_to_fields else_ in + let%bind res = + Array.all + (Core_kernel.Array.map2_exn then_ else_ ~f:(fun then_ else_ -> + if_ b ~then_ ~else_ ) ) + in + let%map res_aux = + (* Abstraction leak.. *) + let res_aux = ref None in + let%map () = + as_prover + As_prover.( + if%map read Boolean.typ b then res_aux := Some then_aux + else res_aux := Some else_aux) + in + match !res_aux with + | Some res_aux -> + res_aux + | None -> + typ.constraint_system_auxiliary () + in + typ.var_of_fields (res, res_aux) + + module Test = struct + let checked_to_unchecked typ1 typ2 checked input = + let checked_result = + run_and_check + (let open Let_syntax in + let%bind input = exists typ1 ~compute:(As_prover.return input) in + let%map result = checked input in + As_prover.read typ2 result) + |> Or_error.ok_exn + in + checked_result + + let test_equal (type a) ?(sexp_of_t = sexp_of_opaque) ?(equal = Caml.( = )) + typ1 typ2 checked unchecked input = + let checked_result = checked_to_unchecked typ1 typ2 checked input in + let sexp_of_a = sexp_of_t in + let compare_a x y = if equal x y then 0 else 1 in + [%test_eq: a] checked_result (unchecked input) + end + + module R1CS_constraint_system = struct + include R1CS_constraint_system + end +end + +(** The main functor for the monadic interface. + See [Run.Make] for the same thing but for the imperative interface. *) +module Make (Backend : Backend_intf.Input_intf) = struct + module Backend_intf = Backend_intf.Make (Backend) + module Types = Runner.Simple_types (Backend_intf) + module As_prover1 = As_prover.Make (Backend_intf) (Types) + module Runner0 = Runner.Make (Backend_intf) (Types) (As_prover1) + module Checked_runner = Runner0.Checked_runner + module Checked1 = + Checked.Make (Backend_intf) (Types) (Checked_runner) (As_prover1) + + module Checked_for_basic = struct + include ( + Checked1 : + Checked_intf.S + with module Types := Types + with type 'a t := 'a Checked1.t + and type run_state = Backend.Run_state.t + and type constraint_ = Backend_intf.Constraint.t ) + + type 'a t = 'a Types.Checked.t + + let run = Runner0.run + end + + module Basic = + Make_basic (Backend_intf) (Types) (Checked_for_basic) (As_prover1) + (Runner0) + include Basic + module Number = Number.Make (Basic) + module Enumerable = Enumerable.Make (Basic) +end + +module Typ0 = Typ + +module Run = struct + let functor_counter = ref 0 + + let active_counters = ref [] + + let is_active_functor_id num = + match !active_counters with + | [] -> + (* Show the usual error, the functor isn't wrong as far as we can tell. + *) + true + | active :: _ -> + Int.equal active num + + let active_functor_id () = List.hd_exn !active_counters + + module Make_basic (Backend : Backend_intf.Input_intf) = struct + module Snark = Make (Backend) + open Backend.Run_state + open Snark + + let set_constraint_logger = set_constraint_logger + + let clear_constraint_logger = clear_constraint_logger + + let this_functor_id = incr functor_counter ; !functor_counter + + let state = + ref + (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 () = Backend.Run_state.dump !state + + let in_prover () : bool = Backend.Run_state.has_witness !state + + let in_checked_computation () : bool = + is_active_functor_id this_functor_id + && Backend.Run_state.is_running !state + + let run (checked : _ Checked.t) = + match checked with + | Pure a -> + a + | _ -> + if not (is_active_functor_id this_functor_id) then + failwithf + "Could not run this function.\n\n\ + Hint: The module used to create this function had internal ID \ + %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 (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 + state := state' ; + x + + let as_stateful x state' = + state := state' ; + let a = x () in + (!state, a) + + let make_checked (type a) (f : unit -> a) : _ Checked.t = + let g : run_state -> run_state * a = as_stateful f in + Function g + + module R1CS_constraint_system = Snark.R1CS_constraint_system + + type field = Snark.field + + type field_var = Snark.field_var + + module Bigint = Snark.Bigint + module Constraint = Snark.Constraint + + module Typ = struct + include Types.Typ + open Snark.Typ + module Data_spec = Typ.Data_spec + + type nonrec ('var, 'value) t = ('var, 'value) t + + let unit = unit + + let field = field + + let tuple2 = tuple2 + + let ( * ) = ( * ) + + let tuple3 = tuple3 + + let list = list + + let array = array + + let hlist = hlist + + let transport = transport + + let transport_var = transport_var + + let of_hlistable = of_hlistable + + type nonrec 'a prover_value = 'a prover_value + + let prover_value = prover_value + end + + let constant (Typ typ : _ Typ.t) x = + let fields, aux = typ.value_to_fields x in + let field_vars = Core_kernel.Array.map ~f:Cvar.constant fields in + typ.var_of_fields (field_vars, aux) + + module Boolean = struct + open Snark.Boolean + + type nonrec var = var + + type value = bool + + let true_ = true_ + + let false_ = false_ + + let if_ b ~then_ ~else_ = run (if_ b ~then_ ~else_) + + let not = not + + let ( && ) x y = run (x && y) + + let ( &&& ) = ( && ) + + let ( || ) x y = run (x || y) + + let ( ||| ) = ( || ) + + let ( lxor ) x y = run (x lxor y) + + let any l = run (any l) + + let all l = run (all l) + + let of_field x = run (of_field x) + + let var_of_value = var_of_value + + let typ = typ + + let typ_unchecked = typ_unchecked + + let equal x y = run (equal x y) + + module Expr = struct + open Snark.Boolean.Expr + + type nonrec t = t + + let ( ! ) = ( ! ) + + let ( && ) = ( && ) + + let ( &&& ) = ( && ) + + let ( || ) = ( || ) + + let ( ||| ) = ( ||| ) + + let any = any + + let all = all + + let not = not + + let eval x = run (eval x) + + let assert_ x = run (assert_ x) + end + + module Unsafe = Unsafe + + module Assert = struct + open Snark.Boolean.Assert + + let ( = ) x y = run (x = y) + + let is_true x = run (is_true x) + + let any l = run (any l) + + let all l = run (all l) + + let exactly_one l = run (exactly_one l) + end + + module Array = struct + open Snark.Boolean.Array + + let any x = run (any x) + + let all x = run (all x) + + module Assert = struct + let any x = run (Assert.any x) + + let all x = run (Assert.all x) + end + end + end + + module Field = struct + open Snark.Field + + let size_in_bits = size_in_bits + + let size = size + + module Constant = struct + type t = Snark.Field.t [@@deriving bin_io, sexp, hash, compare, eq] + + let gen = gen + + let gen_uniform = gen_uniform + + module T = struct + let bin_shape_t = bin_shape_t + + let bin_writer_t = bin_writer_t + + let bin_write_t = bin_write_t + + let bin_size_t = bin_size_t + + let bin_reader_t = bin_reader_t + + let __bin_read_t__ = __bin_read_t__ + + let bin_read_t = bin_read_t + + let bin_t = bin_t + + let sexp_of_t = sexp_of_t + + let t_of_sexp = t_of_sexp + + let of_int = of_int + + let one = one + + let zero = zero + + let add = add + + let sub = sub + + let mul = mul + + let inv = inv + + let square = square + + let sqrt = sqrt + + let is_square = is_square + + let equal = equal + + let size_in_bits = size_in_bits + + let print = print + + let to_string = to_string + + let random = random + + module Vector = Vector + + let negate = negate + + let ( + ) = ( + ) + + let ( - ) = ( - ) + + let ( * ) = ( * ) + + let ( / ) = ( / ) + + let of_string = of_string + + let to_string = to_string + + let unpack = unpack + + let project = project + + let parity = parity + end + + include T + end + + open Snark.Field.Var + + type nonrec t = t + + let var_indices = var_indices + + let to_constant_and_terms = to_constant_and_terms + + let constant = constant + + let to_constant = to_constant + + let linear_combination = linear_combination + + let sum = sum + + let add = add + + let negate = negate + + let sub = sub + + let scale = scale + + let project = project + + let pack = pack + + (* New definitions *) + + let of_int i = constant (Constant.of_int i) + + let one = constant Constant.one + + let zero = constant Constant.zero + + open Snark.Field.Checked + + let mul x y = run (mul x y) + + let square x = run (square x) + + let div x y = run (div x y) + + let inv x = run (inv x) + + let is_square x = run (is_square x) + + let sqrt x = run (sqrt x) + + let sqrt_check x = run (sqrt_check x) + + let equal x y = run (equal x y) + + let unpack x ~length = run (unpack x ~length) + + let unpack_flagged x ~length = run (unpack_flagged x ~length) + + let unpack_full x = run (unpack_full x) + + let parity ?length x = run (parity ?length x) + + let choose_preimage_var x ~length = run (choose_preimage_var x ~length) + + type nonrec comparison_result = comparison_result = + { less : Boolean.var; less_or_equal : Boolean.var } + + let compare ~bit_length x y = run (compare ~bit_length x y) + + let if_ b ~then_ ~else_ = run (if_ b ~then_ ~else_) + + let ( + ) = add + + let ( - ) = sub + + let ( * ) = mul + + let ( / ) = div + + module Unsafe = Unsafe + + module Assert = struct + open Snark.Field.Checked.Assert + + let lte ~bit_length x y = run (lte ~bit_length x y) + + let gte ~bit_length x y = run (gte ~bit_length x y) + + let lt ~bit_length x y = run (lt ~bit_length x y) + + let gt ~bit_length x y = run (gt ~bit_length x y) + + let not_equal x y = run (not_equal x y) + + let equal x y = run (equal x y) + + let non_zero x = run (non_zero x) + end + + let typ = typ + end + + module Proof_inputs = Proof_inputs + + module Bitstring_checked = struct + open Snark.Bitstring_checked + + type nonrec t = t + + let equal x y = run (equal x y) + + let equal_expect_true x y = run (equal_expect_true x y) + + let lt_value x y = run (lt_value x y) + + module Assert = struct + open Snark.Bitstring_checked.Assert + + let equal x y = run (equal x y) + end + end + + module As_prover = struct + type 'a t = 'a + + type 'a as_prover = 'a t + + let eval_as_prover f = + 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 () = Backend.Run_state.as_prover !state + + let read_var var = eval_as_prover (As_prover.read_var var) + + let read typ var = eval_as_prover (As_prover.read typ var) + + include Field.Constant.T + + let run_prover f _tbl = + (* Allow for nesting of prover blocks, by caching the current value and + restoring it once we're done. + *) + let old = Backend.Run_state.as_prover !state in + Backend.Run_state.set_as_prover !state true ; + let a = f () in + Backend.Run_state.set_as_prover !state old ; + a + end + + module Handle = struct + type ('var, 'value) t = ('var, 'value) Handle.t + + let value handle () = As_prover.eval_as_prover (Handle.value handle) + + let var = Handle.var + end + + let mark_active ~f = + let counters = !active_counters in + active_counters := this_functor_id :: counters ; + try + let ret = f () in + active_counters := counters ; + ret + with exn -> + active_counters := counters ; + raise exn + + let mark_active_deferred (type a ma) ~(map : ma -> f:(a -> a) -> ma) ~f = + let counters = !active_counters in + active_counters := this_functor_id :: counters ; + try + map (f ()) ~f:(fun (ret : a) -> + active_counters := counters ; + ret ) + with exn -> + active_counters := counters ; + raise exn + + let assert_ c = run (assert_ c) + + let assert_all c = run (assert_all c) + + let assert_r1cs a b c = run (assert_r1cs a b c) + + let assert_square x y = run (assert_square x y) + + let as_prover p = run (as_prover (As_prover.run_prover p)) + + let next_auxiliary () = run (next_auxiliary ()) + + let request_witness typ p = + run (request_witness typ (As_prover.run_prover p)) + + let perform p = run (perform (As_prover.run_prover p)) + + let request ?such_that typ r = + match such_that with + | None -> + request_witness typ (fun () -> r) + | Some such_that -> + let x = request_witness typ (fun () -> r) in + such_that x ; x + + let exists ?request ?compute typ = + let request = Option.map request ~f:As_prover.run_prover in + let compute = Option.map compute ~f:As_prover.run_prover in + run (exists ?request ?compute typ) + + let exists_handle ?request ?compute typ = + let request = Option.map request ~f:As_prover.run_prover in + let compute = Option.map compute ~f:As_prover.run_prover in + run (exists_handle ?request ?compute typ) + + type nonrec response = response + + let unhandled = unhandled + + type request = Request.request = + | With : + { request : 'a Request.t + ; respond : 'a Request.Response.t -> response + } + -> request + + module Handler = Handler + + let handle x h = + let h = Request.Handler.create_single h in + 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 := Backend.Run_state.set_handler !state handler ; + a + + let handle_as_prover x h = + let h = h () in + handle x h + + let if_ b ~typ ~then_ ~else_ = run (if_ b ~typ ~then_ ~else_) + + let with_label lbl x = + 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 := Backend.Run_state.set_stack !state stack ; + a + + let inject_wrapper : + type r_var input_var. + f:(r_var -> r_var) -> (input_var -> r_var) -> input_var -> r_var = + fun ~f x a -> + let inject_wrapper ~f x = f x in + inject_wrapper ~f (x a) + + (** Caches the global [state] before running [f]. + It is expected that [f] will reset the global state for its own use only, + hence why we need to reset it after running [f].*) + let finalize_is_running f = + let cached_state = !state in + let x = + match f () with + | exception e -> + (* Warning: it is important to clean the global state before reraising the exception. + Imagine if a user of snarky catches exceptions instead of letting the program panic, + then the next usage of snarky might be messed up. *) + state := cached_state ; + raise e + | x -> + x + in + state := cached_state ; + x + + let constraint_system ~input_typ ~return_typ x : R1CS_constraint_system.t = + finalize_is_running (fun () -> + let x = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in + Perform.constraint_system ~run:as_stateful ~input_typ ~return_typ x ) + + type ('input_var, 'return_var, 'result) manual_callbacks = + { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a + ; finish_computation : 'return_var -> 'result + } + + let constraint_system_manual ~input_typ ~return_typ = + let builder = + Run.Constraint_system_builder.build ~input_typ ~return_typ + in + (* FIXME: This behaves badly with exceptions. *) + let cached_state = ref None in + let cached_active_counters = ref None in + let run_circuit circuit = + (* Check the status. *) + if + Option.is_some !cached_state || Option.is_some !cached_active_counters + then failwith "Already generating constraint system" ; + (* Partial [finalize_is_running]. *) + cached_state := Some !state ; + builder.run_computation (fun input state' -> + (* Partial [as_stateful]. *) + state := state' ; + (* Partial [mark_active]. *) + let counters = !active_counters in + cached_active_counters := Some counters ; + active_counters := this_functor_id :: counters ; + (* Start the circuit. *) + circuit input () ) + in + let finish_computation return_var = + (* Check the status. *) + if + Option.is_none !cached_state || Option.is_none !cached_active_counters + then failwith "Constraint system not in a finalizable state" ; + (* Partial [mark_active]. *) + active_counters := Option.value_exn !cached_active_counters ; + (* Create an invalid state, to avoid re-runs. *) + cached_active_counters := None ; + (* Partial [as_stateful]. *) + let state' = !state in + let res = builder.finish_computation (state', return_var) in + (* Partial [finalize_is_running]. *) + state := Option.value_exn !cached_state ; + res + in + { run_circuit; finish_computation } + + let generate_public_input t x : As_prover.Vector.t = + finalize_is_running (fun () -> generate_public_input t x) + + let generate_witness ~input_typ ~return_typ x a : Proof_inputs.t = + finalize_is_running (fun () -> + let x_wrapped = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in + Perform.generate_witness ~run:as_stateful ~input_typ ~return_typ + x_wrapped a ) + + let generate_witness_conv (type out) + ~(f : Proof_inputs.t -> 'r_value -> out) ~input_typ ~return_typ x input + : out = + finalize_is_running (fun () -> + let x_wrapped = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in + Perform.generate_witness_conv ~run:as_stateful ~f ~input_typ + ~return_typ x_wrapped input ) + + let generate_witness_manual ?handlers ~input_typ ~return_typ input = + let builder = + Run.Witness_builder.auxiliary_input ?handlers ~input_typ ~return_typ + input + in + (* FIXME: This behaves badly with exceptions. *) + let cached_state = ref None in + let cached_active_counters = ref None in + let run_circuit circuit = + (* Check the status. *) + if + Option.is_some !cached_state || Option.is_some !cached_active_counters + then failwith "Already generating constraint system" ; + (* Partial [finalize_is_running]. *) + cached_state := Some !state ; + builder.run_computation (fun input state' -> + (* Partial [as_stateful]. *) + state := state' ; + (* Partial [mark_active]. *) + let counters = !active_counters in + cached_active_counters := Some counters ; + active_counters := this_functor_id :: counters ; + (* Start the circuit. *) + circuit input () ) + in + let finish_computation return_var = + (* Check the status. *) + if + Option.is_none !cached_state || Option.is_none !cached_active_counters + then failwith "Constraint system not in a finalizable state" ; + (* Partial [mark_active]. *) + active_counters := Option.value_exn !cached_active_counters ; + (* Create an invalid state, to avoid re-runs. *) + cached_active_counters := None ; + (* Partial [as_stateful]. *) + let state' = !state in + let res = builder.finish_witness_generation (state', return_var) in + (* Partial [finalize_is_running]. *) + state := Option.value_exn !cached_state ; + res + in + { run_circuit; finish_computation } + + (* start an as_prover / exists block and return a function to finish it and witness a given list of fields *) + let as_prover_manual (size_to_witness : int) : + (field array option -> Field.t array) Staged.t = + let s = !state in + let old_as_prover = Backend.Run_state.as_prover s in + (* enter the as_prover block *) + Backend.Run_state.set_as_prover s true ; + + let finish_computation (values_to_witness : field array option) = + (* leave the as_prover block *) + Backend.Run_state.set_as_prover s old_as_prover ; + + (* return variables *) + 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 _ -> + 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 Backend.Run_state.store_field_elt s + in + Core_kernel.Array.map values_to_witness ~f:store_value + (* the other cases are invalid *) + | false, Some _ -> + failwith "Did not expect values to witness" + | true, None -> + failwith "Expected values to witness" + in + Staged.stage finish_computation + + let request_manual (req : unit -> 'a Request.t) () : 'a = + 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 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 + Backend.Run_state.set_as_prover !state old ; + result ) + else Promise.return (else_ ()) + + let as_prover (f : unit -> unit Promise.t) : unit Promise.t = + run_prover ~else_:(fun () -> ()) f + + let unit_request req = as_prover (request_manual req) + end + + let run_unchecked x = + finalize_is_running (fun () -> + Perform.run_unchecked ~run:as_stateful (fun () -> mark_active ~f:x) ) + + let run_and_check_exn (type a) (x : unit -> (unit -> a) As_prover.t) : a = + finalize_is_running (fun () -> + let res = + Perform.run_and_check_exn ~run:as_stateful (fun () -> + mark_active ~f:(fun () -> + let prover_block = x () in + Backend.Run_state.set_as_prover !state true ; + As_prover.run_prover prover_block ) ) + in + Backend.Run_state.set_as_prover !state true ; + res ) + + let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t) : + a Or_error.t = + finalize_is_running (fun () -> + let res = + Perform.run_and_check ~run:as_stateful (fun () -> + mark_active ~f:(fun () -> + let prover_block = x () in + Backend.Run_state.set_as_prover !state true ; + As_prover.run_prover prover_block ) ) + in + Backend.Run_state.set_as_prover !state true ; + res ) + + module Run_and_check_deferred (M : sig + type _ t + + val return : 'a -> 'a t + + val map : 'a t -> f:('a -> 'b) -> 'b t + end) = + struct + open M + + let run_and_check_exn ~run t = + map (run_and_check_deferred_exn' ~run t ~map) ~f:(fun (x, get_value) -> + let x = Basic.As_prover.run x get_value in + x ) + + let run_and_check ~run t = + map + (run_and_check_deferred' ~run t ~map ~return) + ~f: + (Or_error.map ~f:(fun (x, get_value) -> + let x = Basic.As_prover.run x get_value in + x ) ) + + let as_stateful x state' = + state := state' ; + map (x ()) ~f:(fun a -> (!state, a)) + + let run_and_check_exn (type a) (x : unit -> (unit -> a) As_prover.t M.t) : + a M.t = + finalize_is_running (fun () -> + let mark_active = mark_active_deferred ~map in + let res = + run_and_check_exn ~run:as_stateful (fun () -> + mark_active ~f:(fun () -> + map (x ()) ~f:(fun prover_block -> + Backend.Run_state.set_as_prover !state true ; + As_prover.run_prover prover_block ) ) ) + in + Backend.Run_state.set_as_prover !state true ; + res ) + + let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t M.t) : + a Or_error.t M.t = + finalize_is_running (fun () -> + let mark_active = mark_active_deferred ~map in + let res = + run_and_check ~run:as_stateful (fun () -> + mark_active ~f:(fun () -> + map (x ()) ~f:(fun prover_block -> + Backend.Run_state.set_as_prover !state true ; + As_prover.run_prover prover_block ) ) ) + in + Backend.Run_state.set_as_prover !state true ; + res ) + end + + let check_exn x : unit = + finalize_is_running (fun () -> Perform.check_exn ~run:as_stateful x) + + let check x : unit Or_error.t = + finalize_is_running (fun () -> Perform.check ~run:as_stateful x) + + let constraint_count ?(weight = Fn.const 1) ?log x = + let count = ref 0 in + let log_constraint ?at_label_boundary c = + ( match at_label_boundary with + | None -> + () + | Some (pos, lab) -> + Option.iter log ~f:(fun f -> + let start = + Some (match pos with `Start -> true | _ -> false) + in + f ?start lab !count ) ) ; + count := !count + Option.value_map ~default:0 ~f:weight c + in + (* TODO(mrmr1993): Enable label-level logging for the imperative API. *) + let old = !state in + state := + Runner.State.make ~num_inputs:0 ~input:Vector.null ~aux:Vector.null + ~next_auxiliary:(ref 0) ~eval_constraints:false ~with_witness:false + ~log_constraint () ; + ignore (mark_active ~f:x) ; + state := old ; + !count + + module Internal_Basic = Snark + + let run_checked = run + end + + module Make (Backend : Backend_intf.Input_intf) = struct + module Basic = Make_basic (Backend) + include Basic + module Number = Number.Run.Make (Basic) + module Enumerable = Enumerable.Run.Make (Basic) + end +end + +type ('field, 'field_var) m = + (module Snark_intf.Run + with type field = 'field + and type field_var = 'field_var ) \ No newline at end of file diff --git a/src/base/snark0.mli b/src/base/snark.mli similarity index 100% rename from src/base/snark0.mli rename to src/base/snark.mli diff --git a/src/base/snark0.ml b/src/base/snark0.ml deleted file mode 100644 index a53172d7d..000000000 --- a/src/base/snark0.ml +++ /dev/null @@ -1,1568 +0,0 @@ -open Core_kernel -module Bignum_bigint = Bigint - -exception Runtime_error of string list * exn * string - -module Runner = Checked_runner - -let set_eval_constraints b = Runner.eval_constraints := b - -module Make_basic - (Backend : Backend_intf.S) - (Types : Types.Types - with type field = Backend.Field.t - and type field_var = Backend.Cvar.t) - (Checked : Checked_intf.Extended - with module Types := Types - with type run_state = Backend.Run_state.t - and type constraint_ = Backend.Constraint.t) - (As_prover : As_prover_intf.S with module Types := Types) - (Runner : Runner.S - with module Types := Types - with type constr := Backend.Constraint.t option - and type r1cs := Backend.R1CS_constraint_system.t - and type run_state = Backend.Run_state.t) = -struct - open Backend - - type field_var = Cvar.t - - module Typ = struct - include Types.Typ - module T = Typ.Make (Types) (Checked) - include T.T - - type ('var, 'value) t = ('var, 'value) T.t - - let unit : (unit, unit) t = unit () - - let field : (Cvar.t, Field.t) t = field () - end - - include Runners.Make (Backend) (Types) (Checked) (As_prover) (Runner) - module Bigint = Bigint - module Field0 = Field - module Cvar = Cvar - module Constraint = Constraint - - module Handler = struct - type t = Request.request -> Request.response - end - - let constant (Typ typ : _ Typ.t) x = - let fields, aux = typ.value_to_fields x in - let field_vars = Array.map fields ~f:(fun x -> Cvar.constant x) in - typ.var_of_fields (field_vars, aux) - - module As_prover = struct - include As_prover - - type 'a as_prover = 'a t - end - - module Handle = struct - include Handle - - let value = As_prover.Handle.value - end - - module Checked = struct - include ( - Checked : - Checked_intf.Extended - with module Types := Types - with type run_state = Backend.Run_state.t - and type constraint_ = Backend.Constraint.t ) - - let perform req = request_witness Typ.unit req - - module Runner = Runner - include Utils.Make (Backend) (Types) (Checked) (As_prover) (Typ) (Runner) - - module Control = struct end - - let two_to_the n = - let rec go acc i = - if i = 0 then acc else go (Field0.add acc acc) (i - 1) - in - go Field0.one n - - type _ Request.t += Choose_preimage : Field.t * int -> bool list Request.t - - let choose_preimage_unchecked v ~length = - exists - (Typ.list Boolean.typ ~length) - ~request: - As_prover.(map (read_var v) ~f:(fun x -> Choose_preimage (x, length))) - ~compute: - (let open As_prover.Let_syntax in - let%map x = As_prover.read_var v in - let x = Bigint.of_field x in - List.init length ~f:(fun i -> Bigint.test_bit x i)) - - let packing_sum (bits : Boolean.var list) = - let ts, _ = - List.fold_left bits ~init:([], Field.one) ~f:(fun (acc, c) v -> - ((c, (v :> Cvar.t)) :: acc, Field.add c c) ) - in - Cvar.linear_combination ts - - let choose_preimage (v : Cvar.t) ~length : Boolean.var list t = - let open Let_syntax in - let%bind bits = choose_preimage_unchecked v ~length in - let lc = packing_sum bits in - let%map () = assert_r1cs lc (Cvar.constant Field.one) v in - bits - - let choose_preimage_flagged (v : Cvar.t) ~length = - let open Let_syntax in - let%bind bits = choose_preimage_unchecked v ~length in - let lc = packing_sum bits in - let%map success = equal lc v in - (bits, `Success success) - - module List = - Monad_lib.Monad_sequence.List - (Checked) - (struct - type t = Boolean.var - - include Boolean - end) - - module Array = - Monad_lib.Monad_sequence.Array - (Checked) - (struct - type t = Boolean.var - - let any = Boolean.Array.any - - let all = Boolean.Array.all - end) - end - - module Cvar1 = struct - include Cvar - - let project = - let two = Field.of_int 2 in - fun (vars : Checked.Boolean.var list) -> - let rec go res = function - | [] -> - res - | v :: vs -> - go Cvar.(add v (Cvar.scale res two)) vs - in - match List.rev (vars :> Cvar.t list) with - | [] -> - Cvar.constant Field.zero - | v :: vs -> - go v vs - - let pack vars = - assert (List.length vars < Field.size_in_bits) ; - project vars - - let unpack v ~length = - assert (length < Field.size_in_bits) ; - Checked.choose_preimage v ~length - - let unpack_flagged v ~length = - assert (length < Field.size_in_bits) ; - Checked.choose_preimage_flagged v ~length - end - - module Field = struct - include Field0 - - let gen = - Quickcheck.Generator.map - Bignum_bigint.(gen_incl zero (size - one)) - ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) - - let gen_incl lo hi = - let lo_bigint = Bigint.(to_bignum_bigint @@ of_field lo) in - let hi_bigint = Bigint.(to_bignum_bigint @@ of_field hi) in - Quickcheck.Generator.map - Bignum_bigint.(gen_incl lo_bigint hi_bigint) - ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) - - let gen_uniform = - Quickcheck.Generator.map - Bignum_bigint.(gen_uniform_incl zero (size - one)) - ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) - - let gen_uniform_incl lo hi = - let lo_bigint = Bigint.(to_bignum_bigint @@ of_field lo) in - let hi_bigint = Bigint.(to_bignum_bigint @@ of_field hi) in - Quickcheck.Generator.map - Bignum_bigint.(gen_uniform_incl lo_bigint hi_bigint) - ~f:(fun x -> Bigint.(to_field (of_bignum_bigint x))) - - let typ = Typ.field - - module Var = Cvar1 - - let parity x = Bigint.(test_bit (of_field x) 0) - - module Checked = struct - include Cvar1 - - let equal = Checked.equal - - let mul x y = Checked.mul ~label:"Field.Checked.mul" x y - - let square x = Checked.square ~label:"Field.Checked.square" x - - let div x y = Checked.div ~label:"Field.Checked.div" x y - - let inv x = Checked.inv ~label:"Field.Checked.inv" x - - let sqrt (x : Cvar.t) : Cvar.t Checked.t = - match Cvar.to_constant x with - | Some x -> - Checked.return (Cvar.constant (Field.sqrt x)) - | _ -> - let open Checked in - let open Let_syntax in - let%bind y = - exists ~compute:As_prover.(map (read_var x) ~f:Field.sqrt) typ - in - let%map () = assert_square y x in - y - - let quadratic_nonresidue = - lazy - (let rec go i = - let x = Field.of_int i in - if not (Field.is_square x) then x else go Int.(i + 1) - in - go 2 ) - - (* The trick here is the following. - - Let beta be a known non-square. - - x is not a square iff beta*x is a square - - So we guess the result [is_square] and y a sqrt of one of {x, beta*x} and assert - - y * y = is_square * x + (1 - is_square) * (beta * x) - - which, letting B = beta*x holds iff - - y * y - = is_square * x + B - is_square * B - = is_square * (x - B) + B - *) - let sqrt_check x = - let open Checked in - let open Let_syntax in - let%bind is_square = - exists - ~compute:As_prover.(map (read_var x) ~f:Field.is_square) - Boolean.typ - in - let%bind y = - exists typ - ~compute: - As_prover.( - Let_syntax.( - let%map is_square = read Boolean.typ is_square - and x = read_var x in - if is_square then Field.sqrt x - else Field.(sqrt (Lazy.force quadratic_nonresidue * x)))) - in - let b = scale x (Lazy.force quadratic_nonresidue) in - let%bind t = mul (is_square :> Var.t) (x - b) in - let%map () = assert_square y (t + b) in - (y, is_square) - - let is_square x = - let open Checked.Let_syntax in - let%map _, b = sqrt_check x in - b - - let%test_unit "is_square" = - let x = Field.random () in - let typf = Typ.field in - let x2 = Field.square x in - assert (Field.(equal (x * x) x2)) ; - let run elt = - let answer = - run_and_check - (Checked.map - ~f:(As_prover.read Checked.Boolean.typ) - Checked.( - Let_syntax.( - let%bind x = exists typf ~compute:(As_prover.return elt) in - is_square x)) ) - |> Or_error.ok_exn - in - answer - in - assert (run x2) ; - assert (not (run (Field.mul (Lazy.force quadratic_nonresidue) x2))) - - let choose_preimage_var = Checked.choose_preimage - - type comparison_result = - { less : Checked.Boolean.var; less_or_equal : Checked.Boolean.var } - - let if_ = Checked.if_ - - let compare ~bit_length a b = - (* Overview of the logic: - let n = bit_length - We have 0 <= a < 2^n, 0 <= b < 2^n, and so - -2^n < b - a < 2^n - If (b - a) >= 0, then - 2^n <= 2^n + b - a < 2^{n+1}, - and so the n-th bit must be set. - If (b - a) < 0 then - 0 < 2^n + b - a < 2^n - and so the n-th bit must not be set. - Thus, we can use the n-th bit of 2^n + b - a to determine whether - (b - a) >= 0 <-> a <= b. - - We also need that the maximum value - 2^n + (2^n - 1) - 0 = 2^{n+1} - 1 - fits inside the field, so for the max field element f, - 2^{n+1} - 1 <= f -> n+1 <= log2(f) = size_in_bits - 1 - *) - assert (Int.(bit_length <= size_in_bits - 2)) ; - let open Checked in - let open Let_syntax in - [%with_label_ "compare"] (fun () -> - let alpha_packed = - Cvar.(constant (two_to_the bit_length) + b - a) - in - let%bind alpha = unpack alpha_packed ~length:Int.(bit_length + 1) in - let prefix, less_or_equal = - match Core_kernel.List.split_n alpha bit_length with - | p, [ l ] -> - (p, l) - | _ -> - failwith "compare: Invalid alpha" - in - let%bind not_all_zeros = Boolean.any prefix in - let%map less = Boolean.(less_or_equal && not_all_zeros) in - { less; less_or_equal } ) - - module Assert = struct - let lt ~bit_length (x : Cvar.t) (y : Cvar.t) = - match (Cvar.to_constant x, Cvar.to_constant y) with - | Some x, Some y -> - assert (Field.compare x y < 0) ; - Checked.return () - | _ -> - let open Checked in - let open Let_syntax in - let%bind { less; _ } = compare ~bit_length x y in - Boolean.Assert.is_true less - - let lte ~bit_length (x : Cvar.t) (y : Cvar.t) = - match (Cvar.to_constant x, Cvar.to_constant y) with - | Some x, Some y -> - assert (Field.compare x y <= 0) ; - Checked.return () - | _ -> - let open Checked in - let open Let_syntax in - let%bind { less_or_equal; _ } = compare ~bit_length x y in - Boolean.Assert.is_true less_or_equal - - let gt ~bit_length x y = lt ~bit_length y x - - let gte ~bit_length x y = lte ~bit_length y x - - let non_zero (v : Cvar.t) = - match Cvar.to_constant v with - | Some v -> - if Field.(equal zero v) then - failwithf "assert_non_zero: failed on constant %s" - (Field.to_string v) () ; - Checked.return () - | _ -> - Checked.assert_non_zero v - - let equal x y = Checked.assert_equal x y - - let not_equal (x : t) (y : t) = - match (Cvar.to_constant x, Cvar.to_constant y) with - | Some x, Some y -> - if Field.(equal x y) then - failwithf "not_equal: failed on constants %s and %s" - (Field.to_string x) (Field.to_string y) () ; - Checked.return () - | _, _ -> - Checked.with_label "Checked.Assert.not_equal" (fun () -> - non_zero (sub x y) ) - end - - let lt_bitstring_value = - let module Boolean = Checked.Boolean in - let module Expr = struct - module Binary = struct - type 'a t = Lit of 'a | And of 'a * 'a t | Or of 'a * 'a t - end - - module Nary = struct - type 'a t = Lit of 'a | And of 'a t list | Or of 'a t list - - let rec of_binary : 'a Binary.t -> 'a t = function - | Lit x -> - Lit x - | And (x, And (y, t)) -> - And [ Lit x; Lit y; of_binary t ] - | Or (x, Or (y, t)) -> - Or [ Lit x; Lit y; of_binary t ] - | And (x, t) -> - And [ Lit x; of_binary t ] - | Or (x, t) -> - Or [ Lit x; of_binary t ] - - let rec eval = - let open Checked.Let_syntax in - function - | Lit x -> - return x - | And xs -> - Checked.List.map xs ~f:eval >>= Boolean.all - | Or xs -> - Checked.List.map xs ~f:eval >>= Boolean.any - end - end in - let rec lt_binary xs ys : Boolean.var Expr.Binary.t = - match (xs, ys) with - | [], [] -> - Lit Boolean.false_ - | [ _x ], [ false ] -> - Lit Boolean.false_ - | [ x ], [ true ] -> - Lit (Boolean.not x) - | [ x1; _x2 ], [ true; false ] -> - Lit (Boolean.not x1) - | [ _x1; _x2 ], [ false; false ] -> - Lit Boolean.false_ - | x :: xs, false :: ys -> - And (Boolean.not x, lt_binary xs ys) - | x :: xs, true :: ys -> - Or (Boolean.not x, lt_binary xs ys) - | _ :: _, [] | [], _ :: _ -> - failwith "lt_bitstring_value: Got unequal length strings" - in - fun (xs : Boolean.var Bitstring_lib.Bitstring.Msb_first.t) - (ys : bool Bitstring_lib.Bitstring.Msb_first.t) -> - let open Expr.Nary in - eval - (of_binary (lt_binary (xs :> Boolean.var list) (ys :> bool list))) - - let field_size_bits = - lazy - ( List.init Field.size_in_bits ~f:(fun i -> - Z.testbit - (Bignum_bigint.to_zarith_bigint Field.size) - Stdlib.(Field.size_in_bits - 1 - i) ) - |> Bitstring_lib.Bitstring.Msb_first.of_list ) - - let unpack_full x = - let module Bitstring = Bitstring_lib.Bitstring in - let open Checked.Let_syntax in - let%bind res = - choose_preimage_var x ~length:Field.size_in_bits - >>| Bitstring.Lsb_first.of_list - in - let%map () = - lt_bitstring_value - (Bitstring.Msb_first.of_lsb_first res) - (Lazy.force field_size_bits) - >>= Checked.Boolean.Assert.is_true - in - res - - let parity ?length x = - let open Checked in - let unpack = - let unpack_full x = - unpack_full x >>| Bitstring_lib.Bitstring.Lsb_first.to_list - in - match length with - | None -> - unpack_full - | Some length -> - let length = Int.min length Field.size_in_bits in - if Int.equal length Field.size_in_bits then unpack_full - else choose_preimage_var ~length - in - unpack x >>| Base.List.hd_exn - end - end - - module Bitstring_checked = struct - type t = Checked.Boolean.var list - - let lt_value = Field.Checked.lt_bitstring_value - - let chunk_for_equality (t1 : t) (t2 : t) = - let chunk_size = Field.size_in_bits - 1 in - let rec go acc t1 t2 = - match (t1, t2) with - | [], [] -> - acc - | _, _ -> - let t1_a, t1_b = List.split_n t1 chunk_size in - let t2_a, t2_b = List.split_n t2 chunk_size in - go ((t1_a, t2_a) :: acc) t1_b t2_b - in - go [] t1 t2 - - let equal t1 t2 = - let open Checked in - all - (Base.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> - equal (Cvar1.pack x1) (Cvar1.pack x2) ) ) - >>= Boolean.all - - let equal_expect_true t1 t2 = - let open Checked in - all - (Core_kernel.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> - (* Inlined [Field.equal], but skip creating the field element for - this chunk if possible. - *) - let z = Cvar1.(pack x1 - pack x2) in - let%bind r, inv = - exists - Typ.(field * field) - ~compute: - As_prover.( - match - Core_kernel.List.map2 x1 x2 ~f:(fun x1 x2 -> - let%map x1 = read_var (x1 :> Cvar.t) - and x2 = read_var (x2 :> Cvar.t) in - Field.equal x1 x2 ) - with - | Ok res -> - let%bind res = all res in - if Core_kernel.List.for_all ~f:Fn.id res then - return (Field.one, Field.zero) - else equal_vars z - | _ -> - equal_vars z) - in - let%map () = equal_constraints z inv r in - Boolean.Unsafe.of_cvar r ) ) - >>= Boolean.all - - module Assert = struct - let equal t1 t2 = - let open Checked in - Base.List.map (chunk_for_equality t1 t2) ~f:(fun (x1, x2) -> - Backend.Constraint.equal (Cvar1.pack x1) (Cvar1.pack x2) ) - |> assert_all - end - end - - let%test_unit "lt_bitstring_value" = - let gen = - let open Quickcheck.Generator in - let open Let_syntax in - let%bind length = small_positive_int in - let%map x = list_with_length length bool - and y = list_with_length length bool in - (x, y) - in - Quickcheck.test gen ~f:(fun (x, y) -> - let correct_answer = [%compare: bool list] x y < 0 in - let lt = - run_and_check - (Checked.map - ~f:(As_prover.read Checked.Boolean.typ) - (Field.Checked.lt_bitstring_value - (Bitstring_lib.Bitstring.Msb_first.of_list - (List.map ~f:Checked.(constant Boolean.typ) x) ) - (Bitstring_lib.Bitstring.Msb_first.of_list y) ) ) - |> Or_error.ok_exn - in - assert (Bool.equal lt correct_answer) ) - - include Checked - - let%snarkydef_ if_ (b : Boolean.var) ~typ:(Typ typ : ('var, _) Typ.t) - ~(then_ : 'var) ~(else_ : 'var) = - let then_, then_aux = typ.var_to_fields then_ in - let else_, else_aux = typ.var_to_fields else_ in - let%bind res = - Array.all - (Core_kernel.Array.map2_exn then_ else_ ~f:(fun then_ else_ -> - if_ b ~then_ ~else_ ) ) - in - let%map res_aux = - (* Abstraction leak.. *) - let res_aux = ref None in - let%map () = - as_prover - As_prover.( - if%map read Boolean.typ b then res_aux := Some then_aux - else res_aux := Some else_aux) - in - match !res_aux with - | Some res_aux -> - res_aux - | None -> - typ.constraint_system_auxiliary () - in - typ.var_of_fields (res, res_aux) - - module Test = struct - let checked_to_unchecked typ1 typ2 checked input = - let checked_result = - run_and_check - (let open Let_syntax in - let%bind input = exists typ1 ~compute:(As_prover.return input) in - let%map result = checked input in - As_prover.read typ2 result) - |> Or_error.ok_exn - in - checked_result - - let test_equal (type a) ?(sexp_of_t = sexp_of_opaque) ?(equal = Caml.( = )) - typ1 typ2 checked unchecked input = - let checked_result = checked_to_unchecked typ1 typ2 checked input in - let sexp_of_a = sexp_of_t in - let compare_a x y = if equal x y then 0 else 1 in - [%test_eq: a] checked_result (unchecked input) - end - - module R1CS_constraint_system = struct - include R1CS_constraint_system - end -end - -(** The main functor for the monadic interface. - See [Run.Make] for the same thing but for the imperative interface. *) -module Make (Backend : Backend_intf.Input_intf) = struct - module Backend_intf = Backend_intf.Make (Backend) - module Types = Runner.Simple_types (Backend_intf) - module As_prover1 = As_prover.Make (Backend_intf) (Types) - module Runner0 = Runner.Make (Backend_intf) (Types) (As_prover1) - module Checked_runner = Runner0.Checked_runner - module Checked1 = - Checked.Make (Backend_intf) (Types) (Checked_runner) (As_prover1) - - module Checked_for_basic = struct - include ( - Checked1 : - Checked_intf.S - with module Types := Types - with type 'a t := 'a Checked1.t - and type run_state = Backend.Run_state.t - and type constraint_ = Backend_intf.Constraint.t ) - - type 'a t = 'a Types.Checked.t - - let run = Runner0.run - end - - module Basic = - Make_basic (Backend_intf) (Types) (Checked_for_basic) (As_prover1) - (Runner0) - include Basic - module Number = Number.Make (Basic) - module Enumerable = Enumerable.Make (Basic) -end - -module Typ0 = Typ - -module Run = struct - let functor_counter = ref 0 - - let active_counters = ref [] - - let is_active_functor_id num = - match !active_counters with - | [] -> - (* Show the usual error, the functor isn't wrong as far as we can tell. - *) - true - | active :: _ -> - Int.equal active num - - let active_functor_id () = List.hd_exn !active_counters - - module Make_basic (Backend : Backend_intf.Input_intf) = struct - module Snark = Make (Backend) - open Backend.Run_state - open Snark - - let set_constraint_logger = set_constraint_logger - - let clear_constraint_logger = clear_constraint_logger - - let this_functor_id = incr functor_counter ; !functor_counter - - let state = - ref - (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 () = Backend.Run_state.dump !state - - let in_prover () : bool = Backend.Run_state.has_witness !state - - let in_checked_computation () : bool = - is_active_functor_id this_functor_id - && Backend.Run_state.is_running !state - - let run (checked : _ Checked.t) = - match checked with - | Pure a -> - a - | _ -> - if not (is_active_functor_id this_functor_id) then - failwithf - "Could not run this function.\n\n\ - Hint: The module used to create this function had internal ID \ - %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 (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 - state := state' ; - x - - let as_stateful x state' = - state := state' ; - let a = x () in - (!state, a) - - let make_checked (type a) (f : unit -> a) : _ Checked.t = - let g : run_state -> run_state * a = as_stateful f in - Function g - - module R1CS_constraint_system = Snark.R1CS_constraint_system - - type field = Snark.field - - type field_var = Snark.field_var - - module Bigint = Snark.Bigint - module Constraint = Snark.Constraint - - module Typ = struct - include Types.Typ - open Snark.Typ - module Data_spec = Typ.Data_spec - - type nonrec ('var, 'value) t = ('var, 'value) t - - let unit = unit - - let field = field - - let tuple2 = tuple2 - - let ( * ) = ( * ) - - let tuple3 = tuple3 - - let list = list - - let array = array - - let hlist = hlist - - let transport = transport - - let transport_var = transport_var - - let of_hlistable = of_hlistable - - type nonrec 'a prover_value = 'a prover_value - - let prover_value = prover_value - end - - let constant (Typ typ : _ Typ.t) x = - let fields, aux = typ.value_to_fields x in - let field_vars = Core_kernel.Array.map ~f:Cvar.constant fields in - typ.var_of_fields (field_vars, aux) - - module Boolean = struct - open Snark.Boolean - - type nonrec var = var - - type value = bool - - let true_ = true_ - - let false_ = false_ - - let if_ b ~then_ ~else_ = run (if_ b ~then_ ~else_) - - let not = not - - let ( && ) x y = run (x && y) - - let ( &&& ) = ( && ) - - let ( || ) x y = run (x || y) - - let ( ||| ) = ( || ) - - let ( lxor ) x y = run (x lxor y) - - let any l = run (any l) - - let all l = run (all l) - - let of_field x = run (of_field x) - - let var_of_value = var_of_value - - let typ = typ - - let typ_unchecked = typ_unchecked - - let equal x y = run (equal x y) - - module Expr = struct - open Snark.Boolean.Expr - - type nonrec t = t - - let ( ! ) = ( ! ) - - let ( && ) = ( && ) - - let ( &&& ) = ( && ) - - let ( || ) = ( || ) - - let ( ||| ) = ( ||| ) - - let any = any - - let all = all - - let not = not - - let eval x = run (eval x) - - let assert_ x = run (assert_ x) - end - - module Unsafe = Unsafe - - module Assert = struct - open Snark.Boolean.Assert - - let ( = ) x y = run (x = y) - - let is_true x = run (is_true x) - - let any l = run (any l) - - let all l = run (all l) - - let exactly_one l = run (exactly_one l) - end - - module Array = struct - open Snark.Boolean.Array - - let any x = run (any x) - - let all x = run (all x) - - module Assert = struct - let any x = run (Assert.any x) - - let all x = run (Assert.all x) - end - end - end - - module Field = struct - open Snark.Field - - let size_in_bits = size_in_bits - - let size = size - - module Constant = struct - type t = Snark.Field.t [@@deriving bin_io, sexp, hash, compare, eq] - - let gen = gen - - let gen_uniform = gen_uniform - - module T = struct - let bin_shape_t = bin_shape_t - - let bin_writer_t = bin_writer_t - - let bin_write_t = bin_write_t - - let bin_size_t = bin_size_t - - let bin_reader_t = bin_reader_t - - let __bin_read_t__ = __bin_read_t__ - - let bin_read_t = bin_read_t - - let bin_t = bin_t - - let sexp_of_t = sexp_of_t - - let t_of_sexp = t_of_sexp - - let of_int = of_int - - let one = one - - let zero = zero - - let add = add - - let sub = sub - - let mul = mul - - let inv = inv - - let square = square - - let sqrt = sqrt - - let is_square = is_square - - let equal = equal - - let size_in_bits = size_in_bits - - let print = print - - let to_string = to_string - - let random = random - - module Vector = Vector - - let negate = negate - - let ( + ) = ( + ) - - let ( - ) = ( - ) - - let ( * ) = ( * ) - - let ( / ) = ( / ) - - let of_string = of_string - - let to_string = to_string - - let unpack = unpack - - let project = project - - let parity = parity - end - - include T - end - - open Snark.Field.Var - - type nonrec t = t - - let var_indices = var_indices - - let to_constant_and_terms = to_constant_and_terms - - let constant = constant - - let to_constant = to_constant - - let linear_combination = linear_combination - - let sum = sum - - let add = add - - let negate = negate - - let sub = sub - - let scale = scale - - let project = project - - let pack = pack - - (* New definitions *) - - let of_int i = constant (Constant.of_int i) - - let one = constant Constant.one - - let zero = constant Constant.zero - - open Snark.Field.Checked - - let mul x y = run (mul x y) - - let square x = run (square x) - - let div x y = run (div x y) - - let inv x = run (inv x) - - let is_square x = run (is_square x) - - let sqrt x = run (sqrt x) - - let sqrt_check x = run (sqrt_check x) - - let equal x y = run (equal x y) - - let unpack x ~length = run (unpack x ~length) - - let unpack_flagged x ~length = run (unpack_flagged x ~length) - - let unpack_full x = run (unpack_full x) - - let parity ?length x = run (parity ?length x) - - let choose_preimage_var x ~length = run (choose_preimage_var x ~length) - - type nonrec comparison_result = comparison_result = - { less : Boolean.var; less_or_equal : Boolean.var } - - let compare ~bit_length x y = run (compare ~bit_length x y) - - let if_ b ~then_ ~else_ = run (if_ b ~then_ ~else_) - - let ( + ) = add - - let ( - ) = sub - - let ( * ) = mul - - let ( / ) = div - - module Unsafe = Unsafe - - module Assert = struct - open Snark.Field.Checked.Assert - - let lte ~bit_length x y = run (lte ~bit_length x y) - - let gte ~bit_length x y = run (gte ~bit_length x y) - - let lt ~bit_length x y = run (lt ~bit_length x y) - - let gt ~bit_length x y = run (gt ~bit_length x y) - - let not_equal x y = run (not_equal x y) - - let equal x y = run (equal x y) - - let non_zero x = run (non_zero x) - end - - let typ = typ - end - - module Proof_inputs = Proof_inputs - - module Bitstring_checked = struct - open Snark.Bitstring_checked - - type nonrec t = t - - let equal x y = run (equal x y) - - let equal_expect_true x y = run (equal_expect_true x y) - - let lt_value x y = run (lt_value x y) - - module Assert = struct - open Snark.Bitstring_checked.Assert - - let equal x y = run (equal x y) - end - end - - module As_prover = struct - type 'a t = 'a - - type 'a as_prover = 'a t - - let eval_as_prover f = - 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 () = Backend.Run_state.as_prover !state - - let read_var var = eval_as_prover (As_prover.read_var var) - - let read typ var = eval_as_prover (As_prover.read typ var) - - include Field.Constant.T - - let run_prover f _tbl = - (* Allow for nesting of prover blocks, by caching the current value and - restoring it once we're done. - *) - let old = Backend.Run_state.as_prover !state in - Backend.Run_state.set_as_prover !state true ; - let a = f () in - Backend.Run_state.set_as_prover !state old ; - a - end - - module Handle = struct - type ('var, 'value) t = ('var, 'value) Handle.t - - let value handle () = As_prover.eval_as_prover (Handle.value handle) - - let var = Handle.var - end - - let mark_active ~f = - let counters = !active_counters in - active_counters := this_functor_id :: counters ; - try - let ret = f () in - active_counters := counters ; - ret - with exn -> - active_counters := counters ; - raise exn - - let mark_active_deferred (type a ma) ~(map : ma -> f:(a -> a) -> ma) ~f = - let counters = !active_counters in - active_counters := this_functor_id :: counters ; - try - map (f ()) ~f:(fun (ret : a) -> - active_counters := counters ; - ret ) - with exn -> - active_counters := counters ; - raise exn - - let assert_ c = run (assert_ c) - - let assert_all c = run (assert_all c) - - let assert_r1cs a b c = run (assert_r1cs a b c) - - let assert_square x y = run (assert_square x y) - - let as_prover p = run (as_prover (As_prover.run_prover p)) - - let next_auxiliary () = run (next_auxiliary ()) - - let request_witness typ p = - run (request_witness typ (As_prover.run_prover p)) - - let perform p = run (perform (As_prover.run_prover p)) - - let request ?such_that typ r = - match such_that with - | None -> - request_witness typ (fun () -> r) - | Some such_that -> - let x = request_witness typ (fun () -> r) in - such_that x ; x - - let exists ?request ?compute typ = - let request = Option.map request ~f:As_prover.run_prover in - let compute = Option.map compute ~f:As_prover.run_prover in - run (exists ?request ?compute typ) - - let exists_handle ?request ?compute typ = - let request = Option.map request ~f:As_prover.run_prover in - let compute = Option.map compute ~f:As_prover.run_prover in - run (exists_handle ?request ?compute typ) - - type nonrec response = response - - let unhandled = unhandled - - type request = Request.request = - | With : - { request : 'a Request.t - ; respond : 'a Request.Response.t -> response - } - -> request - - module Handler = Handler - - let handle x h = - let h = Request.Handler.create_single h in - 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 := Backend.Run_state.set_handler !state handler ; - a - - let handle_as_prover x h = - let h = h () in - handle x h - - let if_ b ~typ ~then_ ~else_ = run (if_ b ~typ ~then_ ~else_) - - let with_label lbl x = - 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 := Backend.Run_state.set_stack !state stack ; - a - - let inject_wrapper : - type r_var input_var. - f:(r_var -> r_var) -> (input_var -> r_var) -> input_var -> r_var = - fun ~f x a -> - let inject_wrapper ~f x = f x in - inject_wrapper ~f (x a) - - (** Caches the global [state] before running [f]. - It is expected that [f] will reset the global state for its own use only, - hence why we need to reset it after running [f].*) - let finalize_is_running f = - let cached_state = !state in - let x = - match f () with - | exception e -> - (* Warning: it is important to clean the global state before reraising the exception. - Imagine if a user of snarky catches exceptions instead of letting the program panic, - then the next usage of snarky might be messed up. *) - state := cached_state ; - raise e - | x -> - x - in - state := cached_state ; - x - - let constraint_system ~input_typ ~return_typ x : R1CS_constraint_system.t = - finalize_is_running (fun () -> - let x = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in - Perform.constraint_system ~run:as_stateful ~input_typ ~return_typ x ) - - type ('input_var, 'return_var, 'result) manual_callbacks = - { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a - ; finish_computation : 'return_var -> 'result - } - - let constraint_system_manual ~input_typ ~return_typ = - let builder = - Run.Constraint_system_builder.build ~input_typ ~return_typ - in - (* FIXME: This behaves badly with exceptions. *) - let cached_state = ref None in - let cached_active_counters = ref None in - let run_circuit circuit = - (* Check the status. *) - if - Option.is_some !cached_state || Option.is_some !cached_active_counters - then failwith "Already generating constraint system" ; - (* Partial [finalize_is_running]. *) - cached_state := Some !state ; - builder.run_computation (fun input state' -> - (* Partial [as_stateful]. *) - state := state' ; - (* Partial [mark_active]. *) - let counters = !active_counters in - cached_active_counters := Some counters ; - active_counters := this_functor_id :: counters ; - (* Start the circuit. *) - circuit input () ) - in - let finish_computation return_var = - (* Check the status. *) - if - Option.is_none !cached_state || Option.is_none !cached_active_counters - then failwith "Constraint system not in a finalizable state" ; - (* Partial [mark_active]. *) - active_counters := Option.value_exn !cached_active_counters ; - (* Create an invalid state, to avoid re-runs. *) - cached_active_counters := None ; - (* Partial [as_stateful]. *) - let state' = !state in - let res = builder.finish_computation (state', return_var) in - (* Partial [finalize_is_running]. *) - state := Option.value_exn !cached_state ; - res - in - { run_circuit; finish_computation } - - let generate_public_input t x : As_prover.Vector.t = - finalize_is_running (fun () -> generate_public_input t x) - - let generate_witness ~input_typ ~return_typ x a : Proof_inputs.t = - finalize_is_running (fun () -> - let x_wrapped = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in - Perform.generate_witness ~run:as_stateful ~input_typ ~return_typ - x_wrapped a ) - - let generate_witness_conv (type out) - ~(f : Proof_inputs.t -> 'r_value -> out) ~input_typ ~return_typ x input - : out = - finalize_is_running (fun () -> - let x_wrapped = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in - Perform.generate_witness_conv ~run:as_stateful ~f ~input_typ - ~return_typ x_wrapped input ) - - let generate_witness_manual ?handlers ~input_typ ~return_typ input = - let builder = - Run.Witness_builder.auxiliary_input ?handlers ~input_typ ~return_typ - input - in - (* FIXME: This behaves badly with exceptions. *) - let cached_state = ref None in - let cached_active_counters = ref None in - let run_circuit circuit = - (* Check the status. *) - if - Option.is_some !cached_state || Option.is_some !cached_active_counters - then failwith "Already generating constraint system" ; - (* Partial [finalize_is_running]. *) - cached_state := Some !state ; - builder.run_computation (fun input state' -> - (* Partial [as_stateful]. *) - state := state' ; - (* Partial [mark_active]. *) - let counters = !active_counters in - cached_active_counters := Some counters ; - active_counters := this_functor_id :: counters ; - (* Start the circuit. *) - circuit input () ) - in - let finish_computation return_var = - (* Check the status. *) - if - Option.is_none !cached_state || Option.is_none !cached_active_counters - then failwith "Constraint system not in a finalizable state" ; - (* Partial [mark_active]. *) - active_counters := Option.value_exn !cached_active_counters ; - (* Create an invalid state, to avoid re-runs. *) - cached_active_counters := None ; - (* Partial [as_stateful]. *) - let state' = !state in - let res = builder.finish_witness_generation (state', return_var) in - (* Partial [finalize_is_running]. *) - state := Option.value_exn !cached_state ; - res - in - { run_circuit; finish_computation } - - (* start an as_prover / exists block and return a function to finish it and witness a given list of fields *) - let as_prover_manual (size_to_witness : int) : - (field array option -> Field.t array) Staged.t = - let s = !state in - let old_as_prover = Backend.Run_state.as_prover s in - (* enter the as_prover block *) - Backend.Run_state.set_as_prover s true ; - - let finish_computation (values_to_witness : field array option) = - (* leave the as_prover block *) - Backend.Run_state.set_as_prover s old_as_prover ; - - (* return variables *) - 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 _ -> - 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 Backend.Run_state.store_field_elt s - in - Core_kernel.Array.map values_to_witness ~f:store_value - (* the other cases are invalid *) - | false, Some _ -> - failwith "Did not expect values to witness" - | true, None -> - failwith "Expected values to witness" - in - Staged.stage finish_computation - - let request_manual (req : unit -> 'a Request.t) () : 'a = - 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 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 - Backend.Run_state.set_as_prover !state old ; - result ) - else Promise.return (else_ ()) - - let as_prover (f : unit -> unit Promise.t) : unit Promise.t = - run_prover ~else_:(fun () -> ()) f - - let unit_request req = as_prover (request_manual req) - end - - let run_unchecked x = - finalize_is_running (fun () -> - Perform.run_unchecked ~run:as_stateful (fun () -> mark_active ~f:x) ) - - let run_and_check_exn (type a) (x : unit -> (unit -> a) As_prover.t) : a = - finalize_is_running (fun () -> - let res = - Perform.run_and_check_exn ~run:as_stateful (fun () -> - mark_active ~f:(fun () -> - let prover_block = x () in - Backend.Run_state.set_as_prover !state true ; - As_prover.run_prover prover_block ) ) - in - Backend.Run_state.set_as_prover !state true ; - res ) - - let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t) : - a Or_error.t = - finalize_is_running (fun () -> - let res = - Perform.run_and_check ~run:as_stateful (fun () -> - mark_active ~f:(fun () -> - let prover_block = x () in - Backend.Run_state.set_as_prover !state true ; - As_prover.run_prover prover_block ) ) - in - Backend.Run_state.set_as_prover !state true ; - res ) - - module Run_and_check_deferred (M : sig - type _ t - - val return : 'a -> 'a t - - val map : 'a t -> f:('a -> 'b) -> 'b t - end) = - struct - open M - - let run_and_check_exn ~run t = - map (run_and_check_deferred_exn' ~run t ~map) ~f:(fun (x, get_value) -> - let x = Basic.As_prover.run x get_value in - x ) - - let run_and_check ~run t = - map - (run_and_check_deferred' ~run t ~map ~return) - ~f: - (Or_error.map ~f:(fun (x, get_value) -> - let x = Basic.As_prover.run x get_value in - x ) ) - - let as_stateful x state' = - state := state' ; - map (x ()) ~f:(fun a -> (!state, a)) - - let run_and_check_exn (type a) (x : unit -> (unit -> a) As_prover.t M.t) : - a M.t = - finalize_is_running (fun () -> - let mark_active = mark_active_deferred ~map in - let res = - run_and_check_exn ~run:as_stateful (fun () -> - mark_active ~f:(fun () -> - map (x ()) ~f:(fun prover_block -> - Backend.Run_state.set_as_prover !state true ; - As_prover.run_prover prover_block ) ) ) - in - Backend.Run_state.set_as_prover !state true ; - res ) - - let run_and_check (type a) (x : unit -> (unit -> a) As_prover.t M.t) : - a Or_error.t M.t = - finalize_is_running (fun () -> - let mark_active = mark_active_deferred ~map in - let res = - run_and_check ~run:as_stateful (fun () -> - mark_active ~f:(fun () -> - map (x ()) ~f:(fun prover_block -> - Backend.Run_state.set_as_prover !state true ; - As_prover.run_prover prover_block ) ) ) - in - Backend.Run_state.set_as_prover !state true ; - res ) - end - - let check_exn x : unit = - finalize_is_running (fun () -> Perform.check_exn ~run:as_stateful x) - - let check x : unit Or_error.t = - finalize_is_running (fun () -> Perform.check ~run:as_stateful x) - - let constraint_count ?(weight = Fn.const 1) ?log x = - let count = ref 0 in - let log_constraint ?at_label_boundary c = - ( match at_label_boundary with - | None -> - () - | Some (pos, lab) -> - Option.iter log ~f:(fun f -> - let start = - Some (match pos with `Start -> true | _ -> false) - in - f ?start lab !count ) ) ; - count := !count + Option.value_map ~default:0 ~f:weight c - in - (* TODO(mrmr1993): Enable label-level logging for the imperative API. *) - let old = !state in - state := - Runner.State.make ~num_inputs:0 ~input:Vector.null ~aux:Vector.null - ~next_auxiliary:(ref 0) ~eval_constraints:false ~with_witness:false - ~log_constraint () ; - ignore (mark_active ~f:x) ; - state := old ; - !count - - module Internal_Basic = Snark - - let run_checked = run - end - - module Make (Backend : Backend_intf.Input_intf) = struct - module Basic = Make_basic (Backend) - include Basic - module Number = Number.Run.Make (Basic) - module Enumerable = Enumerable.Run.Make (Basic) - end -end - -type ('field, 'field_var) m = - (module Snark_intf.Run - with type field = 'field - and type field_var = 'field_var ) \ No newline at end of file diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index 402eae73b..2a260de72 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -20,6 +20,5 @@ module Request = Request module Run_state = Run_state module Run_state_intf = Run_state_intf module Snark = Snark -module Snark0 = Snark0 module Snark_intf = Snark_intf module Types = Types diff --git a/src/snark.ml b/src/snark.ml deleted file mode 100644 index 72199a35f..000000000 --- a/src/snark.ml +++ /dev/null @@ -1,3 +0,0 @@ -open Snarky_backendless -include Snark0 -module Merkle_tree = Merkle_tree diff --git a/src/snarky.ml b/src/snarky.ml index 51e0436ac..f43710cc5 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -19,7 +19,6 @@ module Pedersen = Snarky_backendless.Pedersen module Request = Snarky_backendless.Request 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 = Snarky_backendless.Snark module Snark_intf = Snarky_backendless.Snark_intf module Types = Snarky_backendless.Types