Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove unused code, simplify Typ.Internal.ref to Typ.prover_value #850

Merged
merged 3 commits into from
Dec 12, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 0 additions & 68 deletions src/base/as_prover_ref.ml

This file was deleted.

28 changes: 4 additions & 24 deletions src/base/snark0.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 :
Expand All @@ -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)
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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.
Expand Down
60 changes: 6 additions & 54 deletions src/base/snark_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/base/snarky_backendless.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
36 changes: 9 additions & 27 deletions src/base/typ.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -145,24 +132,19 @@ module Make (Checked : Checked_monad) = struct
; check = (fun _ -> Checked.return ())
}

module Internal = struct
let snarkless value : _ t =
include struct
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

image

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😭

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)
Expand Down
1 change: 0 additions & 1 deletion src/snarky.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading