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 polymorphism from As_prover.t, hoist Typ.t #854

Merged
merged 16 commits into from
Dec 16, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
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
116 changes: 60 additions & 56 deletions src/base/as_prover0.ml
Original file line number Diff line number Diff line change
@@ -1,53 +1,56 @@
open Core_kernel

type ('a, 'f) t = ('a, 'f) Types.As_prover.t
module Make
(Types : Types.Types
with type ('a, 'f) As_prover.t = ('f Cvar.t -> 'f) -> 'a) =
struct
type ('a, 'f) t = ('a, 'f) Types.As_prover.t

let map t ~f tbl =
let x = t tbl in
f x
let map t ~f tbl =
let x = t tbl in
f x

let bind t ~f tbl =
let x = t tbl in
f x tbl
let bind t ~f tbl =
let x = t tbl in
f x tbl

let return x _ = x
let return x _ = x

let run t tbl = t tbl
let run t tbl = t tbl

let get_state _tbl s = (s, s)
let get_state _tbl s = (s, s)

let set_state s _tbl _ = (s, ())
let set_state s _tbl _ = (s, ())

let modify_state f _tbl s = (f 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
f x y
let map2 x y ~f tbl =
let x = x tbl in
let y = y tbl in
f x y

let read_var (v : 'var) : ('field, 'field) t = fun tbl -> tbl v
let read_var (v : 'var) : ('field, 'field) t = fun tbl -> tbl v

let read
(Typ { var_to_fields; value_of_fields; _ } :
('var, 'value, 'field, _) Types.Typ.t ) (var : 'var) : ('value, 'field) t
=
fun tbl ->
let field_vars, aux = var_to_fields var in
let fields = Array.map ~f:tbl field_vars in
value_of_fields (fields, aux)
let read
(Typ { var_to_fields; value_of_fields; _ } :
('var, 'value, 'field) Types.Typ.t ) (var : 'var) : ('value, 'field) t =
fun tbl ->
let field_vars, aux = var_to_fields var in
let fields = Array.map ~f:tbl field_vars in
value_of_fields (fields, aux)

include Monad_let.Make2 (struct
type nonrec ('a, 'e) t = ('a, 'e) t
include Monad_let.Make2 (struct
type nonrec ('a, 'e) t = ('a, 'e) t

let map = `Custom map
let map = `Custom map

let bind = bind
let bind = bind

let return = return
end)
let return = return
end)

module Provider = struct
(** The different ways to generate a value of type ['a] for a circuit
module Provider = struct
(** The different ways to generate a value of type ['a] for a circuit
witness over field ['f].

This is one of:
Expand All @@ -56,29 +59,30 @@ module Provider = struct
* [Both], attempting to dispatch an ['a Request.t], and falling back to
the computation if the request is unhandled or raises an exception.
*)
type nonrec ('a, 'f) t = (('a Request.t, 'f) t, ('a, 'f) t) Types.Provider.t

open Types.Provider

let run t tbl (handler : Request.Handler.t) =
match t with
| Request rc ->
let r = run rc tbl in
Request.Handler.run handler r
| Compute c ->
Some (run c tbl)
| Both (rc, c) -> (
let r = run rc tbl in
match Request.Handler.run handler r with
| None | (exception _) ->
Some (run c tbl)
| x ->
x )
end

module Handle = struct
let value (t : ('var, 'value) Handle.t) : ('value, 'field) t =
fun _ -> Option.value_exn t.value
type nonrec ('a, 'f) t = ('a, 'f) Types.Provider.t
Copy link
Member

Choose a reason for hiding this comment

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

It was confusing first that the type changes. But ok :).


open Types.Provider

let run t tbl (handler : Request.Handler.t) =
match t with
| Request rc ->
let r = run rc tbl in
Request.Handler.run handler r
| Compute c ->
Some (run c tbl)
| Both (rc, c) -> (
let r = run rc tbl in
match Request.Handler.run handler r with
| None | (exception _) ->
Some (run c tbl)
| x ->
x )
end

module Handle = struct
let value (t : ('var, 'value) Handle.t) : ('value, 'field) t =
fun _ -> Option.value_exn t.value
end
end

module type Extended = sig
Expand Down
3 changes: 2 additions & 1 deletion src/base/checked_runner.ml
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ module type Run_extras = sig
val get_value : field Run_state.t -> cvar -> field

val run_as_prover :
('a, field) As_prover0.t option
('a, field) Types.As_prover.t option
-> field Run_state.t
-> field Run_state.t * 'a option
end
Expand Down Expand Up @@ -356,6 +356,7 @@ struct

let clear_constraint_logger () = constraint_logger := None

module As_prover0 = As_prover0.Make (Types)
module Checked_runner = Make_checked (Backend) (Types) (As_prover0)

type run_state = Checked_runner.run_state
Expand Down
5 changes: 3 additions & 2 deletions src/base/snark0.ml
Original file line number Diff line number Diff line change
Expand Up @@ -670,8 +670,9 @@ module Make (Backend : Backend_intf.S) = struct

module Runner0 = Runner.Make (Backend_extended) (Types)
module Checked_runner = Runner0.Checked_runner
module As_prover1 = As_prover0.Make (Types)
module Checked1 =
Checked.Make (Backend.Field) (Types) (Checked_runner) (As_prover0)
Checked.Make (Backend.Field) (Types) (Checked_runner) (As_prover1)

module Field_T = struct
type field = Backend_extended.Field.t
Expand All @@ -682,7 +683,7 @@ module Make (Backend : Backend_intf.S) = struct
(Field_T)
(struct
module Types = Types
include As_prover0
include As_prover1
end)

module Checked_for_basic = struct
Expand Down
2 changes: 1 addition & 1 deletion src/base/snark_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -710,7 +710,7 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t)

This type specialises the {!type:As_prover.t} type for the backend's
particular field and variable type. *)
type 'a t = ('a, field) As_prover0.t
type 'a t = (Field.Var.t -> Field.t) -> 'a

type 'a as_prover = 'a t

Expand Down