From 905da2e3aa55cf5d9746d379aa44a8d432499145 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Wed, 11 Dec 2024 16:47:23 +0000 Subject: [PATCH 1/3] Remove now-unused Typ toplevel module --- src/base/snarky_backendless.ml | 1 - src/snarky.ml | 1 - 2 files changed, 2 deletions(-) diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml index df1e433e1..55b31bf8b 100644 --- a/src/base/snarky_backendless.ml +++ b/src/base/snarky_backendless.ml @@ -27,5 +27,4 @@ module Run_state = Run_state module Snark = Snark module Snark0 = Snark0 module Snark_intf = Snark_intf -module Typ = Typ module Types = Types diff --git a/src/snarky.ml b/src/snarky.ml index 190f36293..08d3fbdd2 100644 --- a/src/snarky.ml +++ b/src/snarky.ml @@ -27,5 +27,4 @@ module Run_state = Snarky_backendless.Run_state module Snark = Snark module Snark0 = Snarky_backendless.Snark0 module Snark_intf = Snarky_backendless.Snark_intf -module Typ = Snarky_backendless.Typ module Types = Snarky_backendless.Types From 889a5b66dadc64f758ef0365db0ec0f8a0b4c97b Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Wed, 11 Dec 2024 16:55:20 +0000 Subject: [PATCH 2/3] Remove unused function --- src/base/typ.ml | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/src/base/typ.ml b/src/base/typ.ml index c98f0505a..35aeb9d14 100644 --- a/src/base/typ.ml +++ b/src/base/typ.ml @@ -108,19 +108,6 @@ module Make (Checked : Checked_monad) = struct * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t - - let size t = - let rec go : - type r_var r_value k_var k_value. - int -> (r_var, r_value, k_var, k_value, 'f) t -> int = - fun acc t -> - match t with - | [] -> - acc - | Typ { size_in_field_elements; _ } :: t' -> - go (acc + size_in_field_elements) t' - in - go 0 t end let unit () : (unit, unit, 'field) t = From 98805117bcce13e09a6e7de0da24ed2e50e9b267 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Wed, 11 Dec 2024 17:57:17 +0000 Subject: [PATCH 3/3] Replace Typ.Internal and As_prover.Ref with prover_value --- src/base/as_prover_ref.ml | 68 --------------------------------------- src/base/snark0.ml | 28 +++------------- src/base/snark_intf.ml | 60 ++++------------------------------ src/base/typ.ml | 23 ++++++------- 4 files changed, 19 insertions(+), 160 deletions(-) delete mode 100644 src/base/as_prover_ref.ml diff --git a/src/base/as_prover_ref.ml b/src/base/as_prover_ref.ml deleted file mode 100644 index a818f2960..000000000 --- a/src/base/as_prover_ref.ml +++ /dev/null @@ -1,68 +0,0 @@ -open Core_kernel - -type 'a t = 'a option ref - -module Make_ref_typ (Checked : Monad_let.S2) = struct - let typ : ('a t, 'a, _, _) Types.Typ.t = - Typ - { var_to_fields = (fun x -> ([||], !x)) - ; var_of_fields = (fun (_, x) -> ref x) - ; value_to_fields = (fun x -> ([||], Some x)) - ; value_of_fields = (fun (_, x) -> Option.value_exn x) - ; size_in_field_elements = 0 - ; constraint_system_auxiliary = (fun () -> None) - ; check = (fun _ -> Checked.return ()) - } -end - -module type S = sig - module Types : Types.Types - - type ('a, 'f) checked - - type 'f field - - type nonrec 'a t = 'a t - - val create : ('a, 'f field) As_prover0.t -> ('a t, 'f field) checked - - val get : 'a t -> ('a, 'f field) As_prover0.t - - val set : 'a t -> 'a -> (unit, 'f field) As_prover0.t -end - -module Make - (Checked : Checked_intf.S) - (As_prover : As_prover_intf.Basic - with type 'f field := 'f Checked.field - and type ('a, 'f) Provider.t = - ('a, 'f) Checked.Types.Provider.t) : - S - with module Types = Checked.Types - and type ('a, 'f) checked := ('a, 'f) Checked.t - and type 'f field = 'f Checked.field = struct - module Types = Checked.Types - - type 'f field = 'f Checked.field - - type nonrec 'a t = 'a t - - let create (x : ('a, 'f Checked.field) As_prover.t) : - ('a t, 'f Checked.field) Checked.t = - let r = ref None in - let open Checked in - let%map () = - Checked.as_prover (As_prover.map x ~f:(fun x -> r := Some x)) - in - r - - open As_prover.Let_syntax - - let get (r : 'a t) = - let%map () = As_prover.return () in - Option.value_exn !r - - let set (r : 'a t) x = - let%map () = As_prover.return () in - r := Some x -end diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 6fcef9c5f..b0ed161e9 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -12,10 +12,6 @@ module Make_basic (Backend : Backend_extended.S) (Checked : Checked_intf.Extended with type field = Backend.Field.t) (As_prover : As_prover0.Extended with type field := Backend.Field.t) - (Ref : As_prover_ref.S - with module Types := Checked.Types - and type 'f field := Backend.Field.t - and type ('a, 'f) checked := 'a Checked.t) (Runner : Runner.S with module Types := Checked.Types with type field := Backend.Field.t @@ -659,13 +655,6 @@ module Make (Backend : Backend_intf.S) = struct module As_prover_ext = As_prover0.Make_extended (Field_T) (As_prover0) - module Ref : - As_prover_ref.S - with module Types = Checked1.Types - and type ('a, 'f) checked := ('a, 'f) Checked1.t - and type 'f field := Backend_extended.Field.t = - As_prover_ref.Make (Checked1) (As_prover0) - module Checked_for_basic = struct include ( Checked1 : @@ -682,8 +671,7 @@ module Make (Backend : Backend_intf.S) = struct end module Basic = - Make_basic (Backend_extended) (Checked_for_basic) (As_prover_ext) (Ref) - (Runner0) + Make_basic (Backend_extended) (Checked_for_basic) (As_prover_ext) (Runner0) include Basic module Number = Number.Make (Basic) module Enumerable = Enumerable.Make (Basic) @@ -795,7 +783,9 @@ module Run = struct let of_hlistable = of_hlistable - module Internal = Internal + type nonrec 'a prover_value = 'a prover_value + + let prover_value = prover_value end let constant (Typ typ : _ Typ.t) x = @@ -1133,16 +1123,6 @@ module Run = struct include Field.Constant.T - module Ref = struct - type 'a t = 'a As_prover_ref.t - - let create f = run As_prover.(Ref.create (map (return ()) ~f)) - - let get r = eval_as_prover (As_prover.Ref.get r) - - let set r x = eval_as_prover (As_prover.Ref.set r x) - end - let run_prover f _tbl = (* Allow for nesting of prover blocks, by caching the current value and restoring it once we're done. diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 718a83782..e5164b711 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -133,8 +133,6 @@ module type Typ_intf = sig type checked_unit - type _ prover_ref - type ('var, 'value, 'aux, 'field, 'checked) typ' = { var_to_fields : 'var -> 'field Cvar.t array * 'aux ; var_of_fields : 'field Cvar.t array * 'aux -> 'var @@ -256,33 +254,15 @@ module type Typ_intf = sig -> value_of_hlist:((unit, 'k_value) H_list.t -> 'value) -> ('var, 'value) t - (** [Typ.t]s that make it easier to write a [Typ.t] for a mix of R1CS data - and normal OCaml data. - - Using this module is not recommended. - *) - module Internal : sig - (** A do-nothing [Typ.t] that returns the input value for all modes. This - may be used to convert objects from the [Checked] world into and - through [As_prover] blocks. + type _ prover_value - This is the dual of [ref], which allows [OCaml] values from - [As_prover] blocks to pass through the [Checked] world. - - Note: Reading or writing using this [Typ.t] will assert that the - argument and the value stored are physically equal -- ie. that they - refer to the same object. - *) - val snarkless : 'a -> ('a, 'a) t - - (** A [Typ.t] for marshalling OCaml values generated in [As_prover] + (** A [Typ.t] for marshalling OCaml values generated in [As_prover] blocks, while keeping them opaque to the [Checked] world. This is the dual of [snarkless], which allows [OCaml] values from the [Checked] world to pass through [As_prover] blocks. *) - val ref : unit -> ('a As_prover_ref.t, 'a) t - end + val prover_value : unit -> ('a prover_value, 'a) t end module type Constraint_intf = sig @@ -606,7 +586,6 @@ module type Basic = sig and type field_var := Field.Var.t and type checked_unit := unit Checked.t and type _ checked := unit Checked.t - and type 'a prover_ref := 'a As_prover_ref.t end (** Representation of booleans within a field. @@ -736,19 +715,6 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t) type 'a as_prover = 'a t - (** Mutable references for use by the prover in a checked computation. *) - module Ref : sig - (** A mutable reference to an ['a] value, which may be used in checked - computations. *) - type 'a t = 'a As_prover_ref.t - - val create : 'a as_prover -> 'a t Checked.t - - val get : 'a t -> 'a as_prover - - val set : 'a t -> 'a -> unit as_prover - end - include Monad_let.S with type 'a t := 'a t (** Combine 2 {!type:As_prover.t} blocks using another function. *) @@ -1160,8 +1126,7 @@ module type Run_basic = sig with type field := Field.Constant.t and type field_var := Field.t and type checked_unit := unit Internal_Basic.Checked.t - and type _ checked := unit - and type 'a prover_ref := 'a As_prover_ref.t) + and type _ checked := unit) (** Representation of booleans within a field. @@ -1240,19 +1205,6 @@ module type Run_basic = sig type 'a as_prover = 'a t - (** Opaque references for use by the prover in a checked computation. *) - module Ref : sig - (** A mutable reference to an ['a] value, which may be used in checked - computations. *) - type 'a t = 'a As_prover_ref.t - - val create : (unit -> 'a) as_prover -> 'a t - - val get : 'a t -> 'a as_prover - - val set : 'a t -> 'a -> unit as_prover - end - val in_prover_block : unit -> bool val read_var : Field.t -> Field.Constant.t @@ -1278,11 +1230,11 @@ module type Run_basic = sig (Basic with type field = field and type 'a Checked.t = ('a, field) Checked_runner.Simple.t - and type 'a As_prover.Ref.t = 'a As_prover_ref.t and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' = ('var, 'value, 'aux, 'field, 'checked) Typ.typ' and type ('var, 'value, 'field, 'checked) Typ.typ = - ('var, 'value, 'field, 'checked) Typ.typ) + ('var, 'value, 'field, 'checked) Typ.typ + and type 'a Typ.prover_value = 'a Typ.prover_value) module Bitstring_checked : sig type t = Boolean.var list diff --git a/src/base/typ.ml b/src/base/typ.ml index 35aeb9d14..90da372dc 100644 --- a/src/base/typ.ml +++ b/src/base/typ.ml @@ -132,24 +132,19 @@ module Make (Checked : Checked_monad) = struct ; check = (fun _ -> Checked.return ()) } - module Internal = struct - let snarkless value : _ t = + include struct + type 'a prover_value = 'a option + + let prover_value () : _ t = Typ - { var_to_fields = (fun _ -> ([||], ())) - ; var_of_fields = (fun _ -> value) - ; value_to_fields = - (fun value' -> - assert (phys_equal value value') ; - ([||], ()) ) - ; value_of_fields = (fun _ -> value) + { var_to_fields = (fun x -> ([||], x)) + ; var_of_fields = (fun (_, x) -> x) + ; value_to_fields = (fun x -> ([||], Some x)) + ; value_of_fields = (fun (_, x) -> Option.value_exn x) ; size_in_field_elements = 0 - ; constraint_system_auxiliary = (fun () -> ()) + ; constraint_system_auxiliary = (fun () -> None) ; check = (fun _ -> Checked.return ()) } - - module Ref_typ = As_prover_ref.Make_ref_typ (Checked) - - let ref () = Ref_typ.typ end let transport (type var value1 value2 field)