main_protocol.ml
(*****************************************************************************)
(* *)
(* MIT License *)
(* Copyright (c) 2022 Nomadic Labs <contact@nomadic-labs.com> *)
(* *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"),*)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
(* *)
(*****************************************************************************)
(**
aPlonK is a {e PlonK}-based proving system.
As such, it provides a way to create {e succinct cryptographic proofs}
about a given predicate, which can be then verified with a low
computational cost.
In this system, a predicate is represented by an {e arithmetic circuit},
i.e. a collection of arithmetic {e gates} operating over a {e prime field},
connected through {e wires} holding {e scalars} from this field.
For example, the following diagram illustrates a simple circuit checking that
the addition of two scalars ([w1] and [w2]) is equal to [w0]. Here,
the [add] gate can be seen as taking two inputs and producing an output,
while the [eq] gate just takes two inputs and asserts they're equal.
{[
(w0)│ w1│ w2│
│ └───┐ ┌───┘
│ ┌─┴───┴─┐
│ │ add │
│ └───┬───┘
└──────┐ ┌───┘w3
┌─┴───┴─┐
│ eq │
└───────┘
]}
The wires of a circuit are called {e prover inputs}, since the prover needs
an assignment of all wires to produce a proof.
The predicate also declares a subset of the wires called {e verifier inputs}.
In our example, wire [w0] is the only verifier input, which is
indicated by the parenthesis.
A proof for a given [w0] would prove the following statement:
[∃ w1, w2, w3: w3 = w1 + w2 ∧ w0 = w3]
This means that the verifier only needs a (typically small) subset of the
inputs alongside the (succinct) proof to check the validity of the statement.
A more interesting example would be to replace the [add] gate
by a more complicated hash circuit. This would prove the knowledge of the
pre-image of a hash.
A simplified view of aPlonk's API consists of the following three functions:
{[
val setup : circuit -> srs ->
(prover_public_parameters, verifier_public_parameters)
val prove : prover_public_parameters -> prover_inputs ->
private_inputs -> proof
val verify : verifier_public_parameters -> verifier_inputs ->
proof -> bool
]}
In addition to the prove and verify, the interface provides a function
to setup the system. The setup function requires a {e Structured Reference String}.
Two large SRSs were generated by the ZCash and Filecoin
projects and are both used in aPlonK.
Notice also that the circuit is used during setup only and, independently
from its size, the resulting {e verifier_public_parameters} will be a
succinct piece of data that will be posted on-chain to allow
verification and they are bound to the specific circuit that generated
them.
The {e prover_public_parameters}'s size is linear in the size of the circuit.
*)
open Bls
open Utils
open Identities
include Main_protocol_intf
module Make_impl (PP : Polynomial_protocol.S) = struct
module RangeCheck = Range_check_gate.Range_check_gate (PP)
module Perm = Permutation_gate.Permutation_gate (PP)
module Plook = Plookup_gate.Plookup_gate (PP)
module Gates = Custom_gates
module Commitment = PP.PC.Commitment
module Input_commitment = Input_commitment.Make (PP.PC.Commitment)
module PP = PP
exception Entry_not_in_table = Plook.Entry_not_in_table
exception Rest_not_null = Poly.Rest_not_null
type scalar = Scalar.t [@@deriving repr]
type circuit_map = (Circuit.t * int) SMap.t
type proof = {
perm_and_plook : Commitment.t;
wires_cm : Commitment.t;
pp_proof : PP.proof;
}
[@@deriving repr]
type circuit_prover_input = {
witness : scalar array;
input_commitments : Input_commitment.t list;
}
[@@deriving repr]
type prover_inputs = circuit_prover_input list SMap.t [@@deriving repr]
type public_inputs = scalar array list [@@deriving repr]
type verifier_inputs =
(public_inputs * Input_commitment.public list list) SMap.t
[@@deriving repr]
let check_circuit_name map =
SMap.iter
(fun name _ ->
if name = "" then ()
else if Char.compare name.[0] '9' <= 0 then
failwith
(Printf.sprintf "check_circuit_name : circuit name (= '%s')" name
^ " must not begin with '\\', '#', '$', '%', '&', ''', '(', ')', \
'*', '+', ',', '-', '.', '/' or a digit.")
else if String.contains name SMap.Aggregation.sep.[0] then
failwith
(Printf.sprintf
"check_circuit_name : circuit name (= '%s') mustn't contain '%s'"
name
SMap.Aggregation.sep))
map
let check_circuits circuits_map inputs =
check_circuit_name inputs ;
SMap.(
iter (fun k _ ->
if not (mem k circuits_map) then
failwith
(Printf.sprintf
"check_circuits : circuit %s not found in public parameters."
k)))
inputs
(* Returns the wire names as a string list *)
let wire_names nb_wires = List.init nb_wires Plompiler.Csir.wire_name
(* Convert the wire arrays into maps, keyed as in [wire_names] *)
let name_wires wires_array =
SMap.map
(List.map (fun array ->
let n = Array.length array in
List.combine (wire_names n) (Array.to_list array) |> SMap.of_list))
wires_array
let hash_verifier_inputs verifier_inputs =
let open Utils.Hash in
let bytes_of_com c = Plompiler.Utils.to_bytes Input_commitment.public_t c in
let st = init () in
SMap.iter
(fun key (public_inputs_list, input_commitments_list) ->
update st (Bytes.of_string key) ;
List.iter
(fun pi -> Array.iter (fun s -> update st (Scalar.to_bytes s)) pi)
public_inputs_list ;
List.iter
(List.iter (fun c -> update st (bytes_of_com c)))
input_commitments_list)
verifier_inputs ;
finish st
type gate_randomness = {beta : scalar; gamma : scalar; delta : scalar}
let build_gates_randomness transcript =
let betas_gammas, transcript = Fr_generation.random_fr_list transcript 3 in
( {
beta = List.hd betas_gammas;
gamma = List.nth betas_gammas 1;
delta = List.nth betas_gammas 2;
},
transcript )
module Prover = struct
(* - n : upper-bound on the number of constraints in a circuit
- domain : n powers of an n-th root of unity
- pp_public_parameters : polynomial protocol prover parameters
- g_map : preprocessed polynomials for each circuit, prefixed with the
circuit name ; note that this is circuit specific, but we need
them together in order to commit to the whole g_map once.
- g_prover_aux : auxiliary information returned when commiting to g_map.
Note that the rest of the commitment is not needed by
the prover.
- evaluations : FFT evaluations of commonly used polynomials for all
circuits, e.g. L1, Si1, Si2, Si3, X (Lnp1 for plookup).
Each evaluation is on a domain that may be bigger than
[domain] the size is [4n] for most polynomials and [8n]
for some of them. For that, there must exist a [8n]-th
root of unity in the scalar field. These evaluations
does not contain g_map’s.
- zk : true if we want to hide witness polynomial by adding multiple of
(X^n - 1). This increases polynomials degree & may increase the
the size of the evaluations domain & FFTs.
- nb_of_t_chunks : number of T polynomials returned by PP
- eval_points : used for the PC query ; note that the input commitments
are not here, their eval_points have to be added at
proof/verification time
*)
type common_prover_pp = {
n : int;
domain : Domain.t;
pp_public_parameters : PP.prover_public_parameters;
g_map : Poly.t SMap.t;
g_prover_aux : Commitment.prover_aux;
evaluations : Evaluations.t SMap.t;
zk : bool;
nb_of_t_chunks : int;
eval_points : eval_point list list;
}
[@@deriving repr]
(* - circuit_size : number of constraints in the circuit
- input_com_sizes : the size of each input_commitment
- public_input_size : the size of the public inputs
- gates : map from selector names to an array of selector coefficients
(one selector coefficient per constraint).
The length of such array is the domain size (also n). If there
are fewer constraints than n, the array is padded with 0's,
except qpub, that should be [||] if there are public inputs.
- tables : [tables] is a list of scalar arrays, one per wire, so the list
length is Plompiler.Csir.nb_wires_arch.
Each array is the concatenation of one of the columns of all
Plookup tables. (One column per wire, tables which use fewer
columns are completed with dummy ones).
Each scalar array is a concatenation of tables
- wires : an array where each of the components corresponds to a wire in
the architecture and contains an array of indices (one index
per constraint representing the variable that such wire takes
at that constraint).
Again, the length of such array is the domain size (i.e. n).
If there are fewer constraints than n, the array is padded with
the last array element.
- permutation: indices corresponding to a permutation that preserves
[wires]. Its length is [n * Plompiler.Csir.nb_wires_arch] and
should be maximal in the sense that it splits in as many cycles
as there are variables in the circuit.
- evaluations : similar as the common_pp evaluations, but for the
circuit-specific polynomials (selectors, Ss_i, plookup polys),
that are contained in common_pp.g_map.
- alpha : scalar used by plookup.
- ultra : flag to specify whether plookup is being used.
*)
type circuit_prover_pp = {
circuit_size : int;
input_com_sizes : int list;
public_input_size : int;
gates : Scalar.t array SMap.t;
tables : Scalar.t array list;
wires : int array array;
permutation : int array;
rc_permutations : int array SMap.t;
evaluations : Evaluations.t SMap.t;
alpha : Scalar.t option;
ultra : bool;
range_checks : (int * int) list SMap.t;
}
[@@deriving repr]
type public_parameters = {
common_pp : common_prover_pp;
circuits_map : circuit_prover_pp SMap.t;
transcript : PP.transcript;
}
[@@deriving repr]
(* [build_all_wire_keys nb_proofs nb_wires] returns a list of prefixed wires name *)
let build_all_wires_keys pp nb_proofs_map nb_wires =
let names = wire_names nb_wires in
List.concat_map (fun (circuit_name, n) ->
let wires_keys =
List.concat_map
(SMap.Aggregation.build_all_names circuit_name n)
names
in
let c = SMap.find circuit_name pp.circuits_map in
let rc_keys =
SMap.mapi
(fun wire _ ->
let n = SMap.find circuit_name nb_proofs_map in
List.concat_map
(SMap.Aggregation.build_all_names circuit_name n)
(RangeCheck.z_names wire))
c.range_checks
|> SMap.values |> List.concat
in
wires_keys @ rc_keys)
@@ SMap.bindings nb_proofs_map
(* TODO #5551
Handle Plookup
*)
(* For the distributed_prover *)
let build_all_keys_z pp =
List.concat_map
(fun (c_name, c) ->
let perm =
List.map (SMap.Aggregation.add_prefix c_name) Perm.shared_z_names
in
if SMap.is_empty c.range_checks then perm
else
perm
@ (SMap.mapi
(fun wire _ ->
List.map
(SMap.Aggregation.add_prefix c_name)
(RangeCheck.shared_z_names wire))
c.range_checks
|> SMap.values |> List.concat))
(SMap.bindings pp.circuits_map)
let enforce_wire_values wire_indices wire_values =
try
Array.map
(fun l ->
let w_array = Array.map (fun index -> wire_values.(index)) l in
Evaluations.of_array (Array.length w_array - 1, w_array))
wire_indices
with Invalid_argument _ ->
failwith
"Compute_wire_polynomial : x's length does not match with circuit. \
Either your witness is too short, or some indexes are greater than \
the witness size."
let blind ~pp f_map =
let nb_extra_blinds =
List.fold_left
(fun acc e -> max acc (List.length e))
0
pp.common_pp.eval_points
in
let blind_list_map l =
List.map
(fun unblinded ->
if pp.common_pp.zk then
let blinded =
SMap.map
(Poly.blind ~nb_blinds:(1 + nb_extra_blinds) pp.common_pp.n)
unblinded
|> SMap.to_pair
in
(fst blinded, Some (snd blinded))
else (unblinded, None))
l
|> List.split
in
SMap.map blind_list_map f_map |> SMap.to_pair
let update_wires_with_rc_1 ?shifts_map pp
(all_f_wires, f_wires, f_blinds, wires_list_map) =
let rc_z_evals, rc_map =
SMap.mapi
(fun name w_list ->
let circuit_pp = SMap.find name pp.circuits_map in
if SMap.is_empty circuit_pp.range_checks then ([], [])
else
List.map
(fun values ->
RangeCheck.f_map_contribution_1
~range_checks:circuit_pp.range_checks
~domain:pp.common_pp.domain
~values)
w_list
|> List.split)
wires_list_map
|> SMap.filter (fun _ x -> x <> ([], []))
|> SMap.to_pair
in
let rc_map, rc_blinds = blind ~pp rc_map in
let all_rc_z = SMap.Aggregation.gather_maps ?shifts_map rc_map in
let wires_list_map =
SMap.Aggregation.add_map_list_map wires_list_map rc_z_evals
in
let f_wires = SMap.Aggregation.add_map_list_map f_wires rc_map in
let all_f_wires = SMap.union_disjoint all_f_wires all_rc_z in
let f_blinds =
SMap.mapi
(fun k l1 ->
match SMap.find_opt k rc_blinds with
| Some l2 ->
List.map2
(fun a -> function
| Some b -> Some (SMap.union_disjoint (Option.get a) b)
| None -> None)
l1
l2
| None -> l1)
f_blinds
in
(all_f_wires, f_wires, f_blinds, wires_list_map)
(* returns informations about wires, including commitment, blinds &
different useful representations of wires *)
let commit_to_wires ?all_keys ?shifts_map pp
(inputs_map : circuit_prover_input list SMap.t) =
(* wires values map list map *)
let wires_list_map =
SMap.mapi
(fun name input ->
let circuit_pp = SMap.find name pp.circuits_map in
List.map
(fun w -> enforce_wire_values circuit_pp.wires w.witness)
input)
inputs_map
|> name_wires
in
(* wire-polynomials array list map & there blinds *)
let f_wires, f_blinds =
let f_wires =
SMap.map
(List.map
(SMap.map (Evaluations.interpolation_fft pp.common_pp.domain)))
wires_list_map
in
blind ~pp f_wires
in
(* all wire-polynomials gathered in a map *)
let all_f_wires = SMap.Aggregation.gather_maps ?shifts_map f_wires in
let all_f_wires, f_wires, f_blinds, wires_list_map =
update_wires_with_rc_1
?shifts_map
pp
(all_f_wires, f_wires, f_blinds, wires_list_map)
in
let cm_wires, cm_aux_wires =
Commitment.commit
?all_keys
pp.common_pp.pp_public_parameters
all_f_wires
in
(wires_list_map, f_wires, f_blinds, all_f_wires, cm_wires, cm_aux_wires)
(* For each circuits, compute the shared Z polynomial *)
let build_f_map_perm pp {beta; gamma; _} batched_wires =
SMap.mapi
(fun name values ->
let circuit_pp = SMap.find name pp.circuits_map in
(* Removing everything that is not wires *)
let values =
let wires_names =
wire_names Plompiler.Csir.nb_wires_arch
|> List.map String.capitalize_ascii
in
SMap.filter (fun k _ -> List.mem k wires_names) values
in
let zs =
Perm.f_map_contribution
~permutation:circuit_pp.permutation
~values
~beta
~gamma
~domain:pp.common_pp.domain
()
in
if pp.common_pp.zk then
SMap.map
(fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
zs
else zs)
batched_wires
|> SMap.Aggregation.smap_of_smap_smap
(* For each circuit, computes Plookup-specific polynomials *)
let build_f_map_plook ?shifts_map pp rd wires_list_map =
SMap.mapi
(fun name w_list ->
let circuit_pp = SMap.find name pp.circuits_map in
if not circuit_pp.ultra then []
else
List.map
(fun wires ->
let plook_map =
Plook.f_map_contribution
~wires
~gates:circuit_pp.gates
~tables:circuit_pp.tables
~alpha:circuit_pp.alpha
~beta:rd.beta
~gamma:rd.gamma
~domain:pp.common_pp.domain
in
if pp.common_pp.zk then
SMap.map
(fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
plook_map
else plook_map)
w_list)
wires_list_map
|> SMap.Aggregation.gather_maps ?shifts_map
let build_f_map_rc_2 pp rd batched_values =
SMap.mapi
(fun name values ->
let circuit_pp = SMap.find name pp.circuits_map in
if SMap.is_empty circuit_pp.range_checks then SMap.empty
else
let zs =
RangeCheck.f_map_contribution_2
~permutations:circuit_pp.rc_permutations
~beta:rd.beta
~gamma:rd.gamma
~domain:pp.common_pp.domain
~values
in
if pp.common_pp.zk then
SMap.map
(* 3 blinds because the polynomial is evaluated at x and gx *)
(fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
zs
else zs)
batched_values
|> SMap.Aggregation.smap_of_smap_smap
let format_input_com (inputs_map : circuit_prover_input list SMap.t) =
SMap.mapi
(fun name l ->
let n = List.length l in
List.mapi
(fun i w ->
(* For each proof, transforms the list of inputs commitments into
a map of the form {com_label0 -> ic0 ; com_label1 -> ic1 ; …} *)
(List.mapi (fun j ic ->
let name =
SMap.Aggregation.add_prefix
~n
~i
name
(Gates.com_label ^ string_of_int j)
in
( Input_commitment.(SMap.singleton name ic.prover_aux.poly),
ic.prover_aux.pc_prover_aux )))
w.input_commitments)
l
|> List.concat)
inputs_map
|> SMap.values |> List.concat
let build_evaluations pp f_map =
(* rebuild g_maps’ evaluations *)
let evaluations =
SMap.fold
(fun _ pp evals -> SMap.union_disjoint pp.evaluations evals)
pp.circuits_map
pp.common_pp.evaluations
in
Evaluations.compute_evaluations_update_map ~evaluations f_map
let build_perm_rc2_identities pp rd =
SMap.mapi
(fun circuit_name circuit_pp ->
(* Using the batched wires *)
let wires_names =
List.map
String.capitalize_ascii
(wire_names @@ Array.length circuit_pp.wires)
in
let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
let perm_id =
Perm.prover_identities
~circuit_prefix
~wires_names
~beta:rd.beta
~gamma:rd.gamma
~n:pp.common_pp.n
()
in
let range_checks = circuit_pp.range_checks in
if SMap.is_empty range_checks then perm_id
else
let rc2_ids =
RangeCheck.prover_identities_2
~range_checks
~circuit_prefix
~beta:rd.beta
~gamma:rd.gamma
~domain_size:pp.common_pp.n
()
in
merge_prover_identities [perm_id; rc2_ids])
pp.circuits_map
|> SMap.values |> merge_prover_identities
let build_gates_plook_rc1_identities ?shifts_map pp rd inputs_map =
let identities_map =
SMap.mapi
(fun circuit_name inputs_list ->
let circuit_pp = SMap.find circuit_name pp.circuits_map in
let wires_names = wire_names @@ Array.length circuit_pp.wires in
(* Identities that must be computed for each proof *)
let shift, nb_proofs =
match shifts_map with
| None -> (0, List.length inputs_list)
| Some shifts_map -> SMap.find circuit_name shifts_map
in
let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
let proof_prefix i =
SMap.Aggregation.add_prefix
~n:nb_proofs
~i:(i + shift)
circuit_name
in
let gates_identities =
List.mapi
(fun i inputs ->
let input_coms_size =
List.fold_left ( + ) 0 circuit_pp.input_com_sizes
in
let public_inputs =
Array.sub
inputs.witness
input_coms_size
circuit_pp.public_input_size
in
Gates.aggregate_prover_identities
~circuit_prefix
~input_coms_size
~proof_prefix:(proof_prefix i)
~gates:circuit_pp.gates
~public_inputs
~domain:pp.common_pp.domain
())
inputs_list
in
(* for plookup and rc, we do a mapi on the input_list & ignore the
input (instead of doing a List.init nb_proofs) because for the
distributed prover, the number of inputs given will differ from
nb_proofs *)
let plookup_identities =
if not circuit_pp.ultra then []
else
List.mapi
(fun i _ ->
Plook.prover_identities
~circuit_prefix
~proof_prefix:(proof_prefix i)
~wires_names
~alpha:circuit_pp.alpha
~beta:rd.beta
~gamma:rd.gamma
~n:pp.common_pp.n
())
inputs_list
in
let rc1_identities =
let range_checks = circuit_pp.range_checks in
if SMap.is_empty range_checks then []
else
List.mapi
(fun i _ ->
RangeCheck.prover_identities_1
~range_checks
~circuit_prefix
~proof_prefix:(proof_prefix i)
~domain_size:pp.common_pp.n
())
inputs_list
in
merge_prover_identities
(rc1_identities @ plookup_identities @ gates_identities))
inputs_map
in
merge_prover_identities (SMap.values identities_map)
let prove_parameters ~pp_prove pp ~inputs_map =
let wires_list_map, f_wires, f_blinds, all_f_wires, cm_wires, cm_aux_wires
=
commit_to_wires pp inputs_map
in
(* compute beta & gamma (common for all proofs) *)
let transcript = Transcript.expand Commitment.t cm_wires pp.transcript in
let rd, transcript = build_gates_randomness transcript in
let batched_wires =
Perm.Shared_argument.build_batched_wires_values
~delta:rd.delta
~wires:wires_list_map
()
in
(* The new batched_wires is used for the RC shared perm argument *)
let f_map_contributions =
let f_map_perm = build_f_map_perm pp rd batched_wires in
let f_map_plook = build_f_map_plook pp rd wires_list_map in
let f_map_rc2 = build_f_map_rc_2 pp rd batched_wires in
SMap.union_disjoint_list [f_map_perm; f_map_plook; f_map_rc2]
in
let input_com_secrets = format_input_com inputs_map in
let identities =
let gates_plook_rc1_ids =
build_gates_plook_rc1_identities pp rd inputs_map
in
let perm_rc2_ids = build_perm_rc2_identities pp rd in
merge_prover_identities [perm_rc2_ids; gates_plook_rc1_ids]
in
let eval_points =
pp.common_pp.eval_points @ List.map (Fun.const [X]) input_com_secrets
in
(* Here we introduced the use_batched_wires because f_wires does not contain rc stuff, which will be missing if batched wires polys are deduced from f_wires *)
let batched_wires_polys =
Perm.Shared_argument.build_batched_witness_polys
~use_batched_wires:
(SMap.exists
(fun _ c -> not (SMap.is_empty c.range_checks))
pp.circuits_map)
~zero_knowledge:pp.common_pp.zk
~domain:pp.common_pp.domain
~delta:rd.delta
~batched_wires
~f:(f_wires, f_blinds)
()
in
let evaluations =
build_evaluations
pp
(SMap.union_disjoint_list
(all_f_wires :: f_map_contributions :: batched_wires_polys
:: List.map fst input_com_secrets))
in
let cm_perm_plook_rc, perm_plook_rc_prv_aux =
Commitment.commit pp.common_pp.pp_public_parameters f_map_contributions
in
let transcript =
Transcript.expand Commitment.t cm_perm_plook_rc transcript
in
let secrets =
[
(pp.common_pp.g_map, pp.common_pp.g_prover_aux);
(f_map_contributions, perm_plook_rc_prv_aux);
(all_f_wires, cm_aux_wires);
]
@ input_com_secrets
in
let generator = Domain.get pp.common_pp.domain 1 in
let pp_proof, _transcript =
pp_prove
pp.common_pp.pp_public_parameters
transcript
~n:pp.common_pp.n
~generator
~secrets
~eval_points
~evaluations
~identities
~nb_of_t_chunks:pp.common_pp.nb_of_t_chunks
in
(pp_proof, (cm_perm_plook_rc, cm_wires, rd))
end
module Verifier = struct
(* - n : upper-bound on the number of constraints in a circuit
- generator : primitive n-th root of unity
- pp_public_parameters : polynomial protocol verifier parameters
- cm_g : commitment to the preprocessed polynomials
- eval_points : used for the PC query ; note that the input commitments
are not here, their eval_points have to be added at
proof/verification time
*)
type common_verifier_pp = {
n : int;
generator : Scalar.t;
pp_public_parameters : PP.verifier_public_parameters;
cm_g : Commitment.t;
eval_points : eval_point list list;
}
[@@deriving repr]
(* - gates : map of selector names ; they are binded to unit because we
just need their name for the verification
- alpha : scalar used by plookup.
- ultra : flag to specify whether plookup is being used.
- input_com_sizes : the size of each input_commitment
*)
type circuit_verifier_pp = {
gates : unit SMap.t;
alpha : Scalar.t option;
ultra : bool;
input_com_sizes : int list;
range_checks : bool SMap.t;
}
[@@deriving repr]
let circuit_verifier_pp_of_circuit_prover_pp
(prover_pp : Prover.circuit_prover_pp) =
{
gates = SMap.map (Fun.const ()) prover_pp.gates;
alpha = prover_pp.alpha;
ultra = prover_pp.ultra;
input_com_sizes = prover_pp.input_com_sizes;
range_checks = SMap.map (fun l -> l <> []) prover_pp.range_checks;
}
let build_identities circuits_map (n, generator) rd public_inputs_map =
let identities_map =
SMap.mapi
(fun circuit_name pi_list ->
let circuit_pp = SMap.find circuit_name circuits_map in
let nb_proofs = List.length pi_list in
let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
let proof_prefix i =
SMap.Aggregation.add_prefix ~n:nb_proofs ~i circuit_name
in
let wires_names = wire_names Plompiler.Csir.nb_wires_arch in
let perm_identities =
Perm.verifier_identities
~circuit_prefix
~wires_names
~nb_proofs
~generator
~n
~beta:rd.beta
~gamma:rd.gamma
~delta:rd.delta
()
in
let gates_identities =
List.mapi
(fun i public_inputs ->
Gates.aggregate_verifier_identities
~circuit_prefix
~input_com_sizes:circuit_pp.input_com_sizes
~gates:circuit_pp.gates
~public_inputs
~generator
~size_domain:n
()
~proof_prefix:(proof_prefix i))
pi_list
in
let plookup_identities =
if not circuit_pp.ultra then []
else
List.init nb_proofs (fun i ->
Plook.verifier_identities
~circuit_prefix
~wires_names
~generator
~n
~alpha:circuit_pp.alpha
~beta:rd.beta
~gamma:rd.gamma
~proof_prefix:(proof_prefix i)
())
in
let range_checks = circuit_pp.range_checks in
if SMap.is_empty range_checks then
merge_verifier_identities
(perm_identities :: (plookup_identities @ gates_identities))
else
let rc1_identities =
List.init nb_proofs (fun i ->
RangeCheck.verifier_identities_1
~range_checks
~circuit_prefix
~proof_prefix:(proof_prefix i)
())
in
let rc2_identities =
RangeCheck.verifier_identities_2
~range_checks
~circuit_prefix
~nb_proofs
~beta:rd.beta
~gamma:rd.gamma
~delta:rd.delta
~domain_size:n
~generator
()
in
merge_verifier_identities
(perm_identities :: rc2_identities
:: (rc1_identities @ plookup_identities @ gates_identities)))
public_inputs_map
in
merge_verifier_identities (SMap.values identities_map)
let format_input_com (inputs_map : verifier_inputs) =
SMap.mapi
(fun name (_, l) ->
let n = List.length l in
List.mapi
(fun i ic ->
let rename j s =
SMap.Aggregation.add_prefix ~n ~i name s ^ string_of_int j
in
List.mapi (fun j -> Commitment.rename (rename j)) ic)
l
|> List.concat)
inputs_map
|> SMap.values |> List.concat
(* Assumes the same circuit, i.e. the public parameters are fixed *)
let verify_parameters ((common_pp, circuits_map), transcript) inputs_map
proof =
(* The transcript is the same as the provers's transcript since the proof
is already aggregated *)
let transcript =
Transcript.expand Commitment.t proof.wires_cm transcript
in
(* Get the same randomness for all proofs *)
(* Step 1a : compute beta & gamma *)
let rd, transcript = build_gates_randomness transcript in
(* Step 3 : compute verifier’s identities *)
let identities =
build_identities
circuits_map
(common_pp.n, common_pp.generator)
rd
(SMap.map fst inputs_map)
in
let input_commitments = format_input_com inputs_map in
let commitments =
[common_pp.cm_g; proof.perm_and_plook; proof.wires_cm]
@ input_commitments
in
let eval_points =
common_pp.eval_points @ List.map (Fun.const [X]) input_commitments
in
let transcript =
Transcript.expand Commitment.t proof.perm_and_plook transcript
in
(transcript, identities, rd, commitments, eval_points)
end
type prover_public_parameters = Prover.public_parameters = {
common_pp : Prover.common_prover_pp;
circuits_map : Prover.circuit_prover_pp SMap.t;
transcript : PP.transcript;
}
[@@deriving repr]
type verifier_public_parameters = {
common_pp : Verifier.common_verifier_pp;
circuits_map : Verifier.circuit_verifier_pp SMap.t;
transcript : PP.transcript;
}
[@@deriving repr]
module Preprocess = struct
let eval_points (circuits_map : Prover.circuit_prover_pp SMap.t) =
let open Prover in
let used_ultra = SMap.exists (fun _ c -> c.ultra) circuits_map in
(* We need gX evaluation for wires if there is a next gate, or if there is a range check gate (RC.Z needs to be evaluated at X & gX and is committed with wires) *)
let gx_wires =
SMap.exists
(fun _ c ->
Gates.exists_gx_composition ~gates:c.gates
|| c.range_checks <> SMap.empty)
circuits_map
in
let g_points = if used_ultra then [X; GX] else [X] in
let f_points = if gx_wires then [X; GX] else [X] in
[g_points; [X; GX]; f_points]
let degree_evaluations ~nb_wires ~gates ~ultra =
let min_deg =
(* minimum size needed for permutation gate ; if we are in the gate case, nb_wires = 0 => min_perm = 1 which is the minimum degree anyway *)
let min_perm = Perm.polynomials_degree ~nb_wires in
if ultra then max (Plook.polynomials_degree ()) min_perm else min_perm
in
max min_deg (Gates.aggregate_polynomials_degree ~gates)
let domain_evaluations ~zero_knowledge ~n len_evals =
let zk_factor = if zero_knowledge then if n <= 2 then 4 else 2 else 1 in
let len_evals = zk_factor * len_evals * n in
Domain.build_power_of_two Z.(log2up (of_int len_evals))
(* Function preprocessing the circuit wires and selector polynomials;
Inputs:
- n: the number of constraints in the circuits + the number of public inputs
- domain: the interpolation domain for polynomials of size n
- l, the number of public inputs + the number of elements committed in input_commitments
Outputs:
- interpolated_gates: selector polynomials, prepended with 0/1s for the public inputs,
interpolated on the domain
- extended_gates: gates with "q_pub" selector if there is public_inputs
- extended_wires: circuits wires prepended with wires corresponding to the public inputs
- extended_tables: formatted tables
- adapted_range_checks: range check with indexes shifted regarding public_inputs
*)
let preprocessing n domain (c : Circuit.t) =
let l = List.fold_left ( + ) c.public_input_size c.input_com_sizes in
let ql_name = Plompiler.Csir.linear_selector_name 0 in
(* Updating selectors for public inputs. *)
let gates =
(* Define ql if undefined as it is the gate taking the public input in. *)
if l > 0 && (not @@ SMap.mem ql_name c.gates) then
SMap.add
ql_name
(Array.init c.circuit_size (fun _ -> Scalar.zero))
c.gates
else c.gates
in
(* other preprocessed things in article are computed in prove of permutations *)
let extended_gates =
(* Adding 0s/1s for public inputs & input_commitments *)
SMap.mapi
(fun label gate ->
let length_poly = Array.length gate in
Array.init n (fun i ->
if i < l && label = ql_name then Scalar.one
else if l <= i && i < l + length_poly then gate.(i - l)
else Scalar.zero))
gates
in
let extended_gates, _, _ =
List.fold_left
(fun (acc, i, k) size ->
let acc =
SMap.add
("qcom" ^ string_of_int i)
(Array.init n (fun j ->
if j >= k && j < k + size then Scalar.(negate one)
else Scalar.zero))
acc
in
(acc, i + 1, k + size))
(extended_gates, 0, 0)
c.input_com_sizes
in
let interpolated_gates =
SMap.map (Evaluations.interpolation_fft2 domain) extended_gates
in
let extended_gates =
if c.public_input_size = 0 then extended_gates
else SMap.add_unique "qpub" [||] extended_gates
in
let extended_wires =
let li_array = Array.init l (fun i -> i) in
(* Adding public inputs and resizing *)
Array.map (fun w -> Array.pad (Array.append li_array w) n) c.wires
in
let adapted_range_checks =
SMap.map (List.map (fun (i, n) -> (l + i, n))) c.range_checks
in
let extended_tables =
if not c.ultra then []
else
Plook.format_tables
~tables:c.tables
~nb_columns:Plompiler.Csir.nb_wires_arch
~length_not_padded:c.table_size
~length_padded:n
in
( interpolated_gates,
extended_gates,
extended_wires,
extended_tables,
adapted_range_checks )
let preprocess_map domain domain_evals n circuits_map =
(* Preprocessing wires, gates and tables *)
SMap.fold
(fun circuit_name (circuit, _) (prv, vrf, all_g_maps) ->
(* Generating alpha for Plookup *)
let alpha =
if Circuit.(circuit.ultra) then Some (Scalar.random ()) else None
in
let gates_poly, gates, wires, tables, range_checks =
preprocessing n domain circuit
in
(* Generating permutation *)
let permutation = Perm.build_permutation wires in
let rc_permutations =
RangeCheck.build_permutations ~range_checks ~size_domain:n
in
let g_map_perm =
Perm.preprocessing
~domain
~nb_wires:Plompiler.Csir.nb_wires_arch
~permutation
()
in
let g_map_plook =
if circuit.ultra then Plook.preprocessing ~domain ~tables ~alpha ()
else SMap.empty
in
let g_map_range_check =
RangeCheck.preprocessing
~permutations:rc_permutations
~range_checks:circuit.range_checks
~domain
in
let circuit_g_map =
SMap.union_disjoint_list
[g_map_plook; g_map_perm; gates_poly; g_map_range_check]
|> SMap.Aggregation.prefix_map circuit_name
in
let evaluations =
Evaluations.compute_evaluations ~domain:domain_evals circuit_g_map
in
let prover_pp =
Prover.
{
circuit_size = circuit.circuit_size;
input_com_sizes = circuit.input_com_sizes;
public_input_size = circuit.public_input_size;
gates;
tables;
wires;
evaluations;
permutation;
rc_permutations;
alpha;
ultra = circuit.ultra;
range_checks;
}
in
let verifier_pp =
let gates = SMap.map (fun _ -> ()) gates in
Verifier.
{
gates;
alpha;
ultra = circuit.ultra;
input_com_sizes = circuit.input_com_sizes;
range_checks = SMap.map (fun rc -> rc <> []) range_checks;
}
in
( SMap.add_unique circuit_name prover_pp prv,
SMap.add_unique circuit_name verifier_pp vrf,
SMap.union_disjoint all_g_maps circuit_g_map ))
circuits_map
SMap.(empty, empty, empty)
let compute_sizes circuit_name
( Circuit.
{
public_input_size;
input_com_sizes;
circuit_size;
table_size;
nb_lookups;
ultra;
gates;
range_checks;
_;
},
nb_proofs ) =
(* Computing domain *)
(* For TurboPlonk, we want a domain of size a power of two
higher than or equal to the number of constraints plus public inputs.
As for UltraPlonk, a domain of size stricly higher than the number of constraints
(to be sure we pad the last lookup).
For range-checks, we want to ensure that the domain size is greater than the "size" of the "biggest" range-checks
*)
let nb_max_constraints =
let base_size =
circuit_size
+ List.fold_left ( + ) public_input_size input_com_sizes
+ if ultra then 1 else 0
in
let size_with_rc, biggest_rc_wire =
SMap.fold
(fun wire r (acc, rc_wire) ->
let sum_bounds =
(List.fold_left (fun sum (_, bound) -> sum + bound)) 0 r
in
if sum_bounds > acc then (sum_bounds, wire) else (acc, rc_wire))
range_checks
(base_size, "")
in
(* if the circuit size has been increased because of the range checks we raise a warning *)
let _print_warning =
match biggest_rc_wire with
| "" -> ()
| w ->
Printf.printf
"\n\
WARNING: Circuit %s's size has been increased to %d (initial \
size was %d) because of the range-checks on the %s wire."
circuit_name
size_with_rc
base_size
w
in
size_with_rc
in
(* For UltraPlonk, we want a domain of size a power of two
higher than the number of records and strictly higher than the number of lookups *)
let nb_rec_look = if ultra then max (nb_lookups + 1) table_size else 0 in
let max_nb = max nb_max_constraints nb_rec_look in
let log = Z.(log2up (of_int max_nb)) in
let n = Int.shift_left 1 log in
let pack_size =
(* L1, Ssi, selectors, ultra stuff *)
let nb_g_map_polys =
let ultra_polys = if ultra then 2 else 0 in
1 + Plompiler.Csir.nb_wires_arch + SMap.cardinal gates + ultra_polys
in
let nb_extra_polys = if ultra then 5 else 1 in
let online =
max Plompiler.Csir.nb_wires_arch nb_extra_polys * nb_proofs
in
(* 5 stands for the max number of T polynomials, if we split T *)
let offline = max nb_g_map_polys 5 in
(* Multiply by 2 to have more than needed, just in case *)
2 * max online offline
in
(log, n, pack_size)
let get_sizes ~zero_knowledge circuits_map =
let log, n, total_pack, some_ultra =
SMap.fold
(fun k (c, nb_proofs) (acc_log, acc_n, acc_pack_size, acc_ultra) ->
let log, n, pack_size = compute_sizes k (c, nb_proofs) in
( max acc_log log,
max acc_n n,
acc_pack_size + pack_size,
acc_ultra || c.ultra ))
circuits_map
(0, 0, 0, false)
in
let degree_evals =
SMap.fold
(fun _ ((c : Circuit.t), _) acc_deg_eval ->
let deg_eval =
degree_evaluations
~nb_wires:Plompiler.Csir.nb_wires_arch
~gates:c.gates
~ultra:c.ultra
in
max acc_deg_eval deg_eval)
circuits_map
0
in
let domain_evals = domain_evaluations ~zero_knowledge ~n degree_evals in
let domain = Domain.build_power_of_two log in
let total_pack = 1 lsl Z.(log2up (of_int total_pack)) in
(* Each t chunk should be of degree [n].
We remove 1 because t is divided by (X^n - 1) *)
let nb_of_t_chunks =
degree_evals + (if zero_knowledge then 1 else 0) - 1
in
(domain, n, total_pack, domain_evals, some_ultra, nb_of_t_chunks)
let setup_circuits ~zero_knowledge circuits_map ~srs =
let domain, n, pack_size, domain_evals, some_ultra, nb_of_t_chunks =
get_sizes ~zero_knowledge circuits_map
in
let evaluations =
(* Add X evaluations, which is the domain needed for other evaluations *)
let evaluations =
SMap.singleton "X" (Evaluations.of_domain domain_evals)
in
(* Add L₁, Sid₁, Sid₂, Sid₃, Sid₄, Sid₅ *)
let evaluations =
Perm.common_preprocessing
~nb_wires:Plompiler.Csir.nb_wires_arch
~domain
~evaluations
in
(* if ultra add L_n_plus_1 *)
if some_ultra then Plook.common_preprocessing ~n ~domain ~evaluations
else evaluations
in
let pp_prv, pp_vrf, g_map =
preprocess_map domain domain_evals n circuits_map
in
(* Generating public parameters *)
let pp_prover, pp_verifier = PP.setup ~setup_params:pack_size ~srs in
let cm_g, g_prover_aux = Commitment.commit pp_prover g_map in
(* Generating transcript *)
let transcript =
PP.PC.Public_parameters.to_bytes n pp_prover
|> Transcript.expand Commitment.t cm_g
in
let eval_points = eval_points pp_prv in
let common_prv =
Prover.
{
n;
domain;
pp_public_parameters = pp_prover;
evaluations;
g_map;
g_prover_aux;
zk = zero_knowledge;
nb_of_t_chunks;
eval_points;
}
in
let common_vrf =
Verifier.
{
n;
generator = Domain.get domain 1;
pp_public_parameters = pp_verifier;
cm_g;
eval_points;
}
in
( ({common_pp = common_prv; circuits_map = pp_prv; transcript}
: prover_public_parameters),
{common_pp = common_vrf; circuits_map = pp_vrf; transcript} )
end
let to_verifier_inputs (pp : prover_public_parameters) =
let extract name (secrets : circuit_prover_input list) :
public_inputs * Input_commitment.public list list =
let c = SMap.find name pp.circuits_map in
let ic_size = List.fold_left ( + ) 0 c.input_com_sizes in
let public_inputs =
List.map
(fun s -> Array.sub s.witness ic_size c.public_input_size)
secrets
in
let input_commitments =
List.map
(fun s ->
List.map
(fun (c : Input_commitment.t) -> c.public)
s.input_commitments)
secrets
in
(public_inputs, input_commitments)
in
SMap.mapi extract
let expand_transcript_with_verifier_inputs transcript verifier_inputs =
Transcript.expand
Repr.bytes
(hash_verifier_inputs verifier_inputs)
transcript
let input_commit ?size ?shift (pp : prover_public_parameters) secret =
Input_commitment.commit
?size
?shift
pp.common_pp.pp_public_parameters
pp.common_pp.n
secret
let update_prover_public_parameters x (pp : prover_public_parameters) =
{pp with transcript = Transcript.expand Repr.bytes x pp.transcript}
let update_verifier_public_parameters x (pp : verifier_public_parameters) =
{pp with transcript = Transcript.expand Repr.bytes x pp.transcript}
(* [filter_pp_circuits pp inputs_map] returns [pp]
without the circuits that don’t appear in [inputs_map]’s keys
*)
let filter_prv_pp_circuits (pp : prover_public_parameters) inputs_map =
check_circuits pp.circuits_map inputs_map ;
{pp with circuits_map = SMap.sub_map inputs_map pp.circuits_map}
let filter_vrf_pp_circuits pp inputs_map =
check_circuits pp.circuits_map inputs_map ;
{pp with circuits_map = SMap.sub_map inputs_map pp.circuits_map}
let setup ~zero_knowledge circuits_map ~srs =
check_circuit_name circuits_map ;
Preprocess.setup_circuits ~zero_knowledge circuits_map ~srs
(* inputs is a map between circuit names to list of public inputs *)
let prove (pp : prover_public_parameters) ~inputs =
check_circuit_name pp.circuits_map ;
(* add the verifier inputs to the transcript *)
let pp =
{
pp with
transcript =
expand_transcript_with_verifier_inputs
pp.transcript
(to_verifier_inputs pp inputs);
}
in
let pp_proof, (perm_and_plook, wires_cm, _) =
Prover.prove_parameters
~pp_prove:PP.prove
(filter_prv_pp_circuits pp inputs)
~inputs_map:inputs
in
{perm_and_plook; wires_cm; pp_proof}
let verify pp ~inputs proof =
check_circuit_name pp.circuits_map ;
let circuits_map = SMap.sub_map inputs pp.circuits_map in
(* add the verifier inputs to the transcript *)
let transcript =
expand_transcript_with_verifier_inputs pp.transcript inputs
in
let transcript, identities, _, commitments, eval_points =
Verifier.verify_parameters
((pp.common_pp, circuits_map), transcript)
inputs
proof
in
PP.verify
pp.common_pp.pp_public_parameters
transcript
~n:pp.common_pp.n
~generator:pp.common_pp.generator
~commitments
~identities
~eval_points
proof.pp_proof
|> fst
let scalar_encoding =
Data_encoding.(
conv
Scalar.to_bytes
Scalar.of_bytes_exn
(Fixed.bytes Scalar.size_in_bytes))
let data_encoding_of_repr repr =
Data_encoding.conv
(Plompiler.Utils.to_bytes repr)
(Plompiler.Utils.of_bytes repr)
Data_encoding.bytes
let proof_encoding = data_encoding_of_repr proof_t
let verifier_public_parameters_encoding =
data_encoding_of_repr verifier_public_parameters_t
module Internal_for_tests = struct
let mutate_vi verifier_inputs =
(* TODO we could do a more randomized search *)
let key, (public_inputs_list, input_commitments_list) =
SMap.choose verifier_inputs
in
match public_inputs_list with
| head :: tail ->
if head = [||] then None (* empty public inputs *)
else
let new_head = Array.copy head in
new_head.(0) <- Scalar.(add one new_head.(0)) ;
let public_inputs_list = new_head :: tail in
let inputs = (public_inputs_list, input_commitments_list) in
Some (SMap.add key inputs verifier_inputs)
| [] -> failwith "mutate_vi : all circuits should have verifier inputs."
end
end
module Make : functor (PP : Polynomial_protocol.S) ->
S with type public_inputs = Scalar.t array list =
Make_impl
include Make (Polynomial_protocol)
