Halo2 Circuit Aggregation
1 Schema:
1.1 Query with commits and evaluations.
Given polynomial
Thus a proof and verification schema can be defined as a large multi-open of queries.
For example we can write down the verifying schema of standard plonk in some ast in the following AST:
let r = eval!(a) * eval!(b) * commit!(qm) + eval!(a) * commit!(ql)
+ eval!(b) * commit!(qr) + eval!(c) * commit!(qo) + pi_xi + commit!(qc)
+ scalar!(self.alpha) * (
(eval!(a) + (scalar!(self.beta) * xi.clone()) + scalar!(self.gamma))
* (eval!(b) + (scalar!(self.beta)
* scalar!(self.common.k[0]) * xi.clone()) + scalar!(self.gamma))
* (eval!(c) + (scalar!(self.beta)
* scalar!(self.common.k[1]) * xi) + scalar!(self.gamma))
* commit!(z)
+ (eval!(a) + (scalar!(self.beta) * eval!(sigma1))
+ scalar!(self.gamma))
* (eval!(b) + (scalar!(self.beta) * eval!(sigma2))
+ scalar!(self.gamma))
* (eval!(c) + (scalar!(self.beta) * commit!(sigma3))
+ scalar!(self.gamma))
* eval!(zxi)
)
+ scalar!(self.alpha) * scalar!(self.alpha)
* l1_xi * (commit!(z) + scalar!(neg_one))
+ zh_xi * (commit!(tl) + xi_n * commit!(tm) + xi_2n * commit!(th))
+ scalar!(self.v) * (
commit!(a) + scalar!(self.v) * (
commit!(b) + scalar!(self.v) * (
commit!(c) + scalar!(self.v) * (
commit!(sigma1) + scalar!(self.v) * commit!(sigma2)
)
)
)
)
+ scalar!(self.v) * (
eval!(a) + scalar!(self.v) * (
eval!(b) + scalar!(self.v) * (
eval!(c) + scalar!(self.v) * (
eval!(sigma1) + scalar!(self.v) * eval!(sigma2)
)
)
)
);
Ok(EvaluationProof {s:r, point:self.xi.clone(), w: self.commits.w_z})
1.2 Arithment within special context:
This document is a design brief of how to generate plonk verifying code and plonk verification circuit (mainly for proof aggregation) at the same time. The main idea is to abstract a trait of group and field algebra for both code and circuit(We believe there are various benifits to do so both for maintaince and for furture updating of the proof schema for the verifying circuit). To achieve this, we notice that in verifying code generation, arithment are performed with no side effects but when using fp over fr arithment gates, integer and pointer arithment will have side effects(change the state of the gate).
Thus our arithment trait is a trait that will assume side effects do exists during the arithment of scalar fields, base fields and point groups of ecc.
For example, arithment like "a + b * p" needs to be performed under a arith_in_ctx macro looks like
arith_in_ctx!([ctx], a + b * p)
Moreover the context has to components, one for scalar arithment and the other for elliptic arithment.
pub trait ArithEccChip:
ArithCommonChip<Value = Self::Point, AssignedValue = Self::AssignedPoint>
{
type ScalarChip: ArithFieldChip<
Context = Self::Context,
Field = Self::Scalar,
AssignedField = Self::AssignedScalar,
Error = Self::Error,
>;
type NativeChip: ArithFieldChip<
Context = Self::Context,
Field = Self::Native,
AssignedField = Self::AssignedNative,
Error = Self::Error,
>;
1.3 Different context for schema:
There are three computation context involved in the codebase:
- Pure calculation context
- Halo2 circuit context
- Solidity runtime context
When basic arithment are implemented for all these three context, we implement the eval trait of schema to evaluate the result of the mutl_exp
impl<P: Clone, S: Clone> EvaluationQuerySchema<P, S> {
pub fn eval<
Scalar: FieldExt,
A: ArithEccChip<AssignedPoint = P, AssignedScalar = S, Scalar = Scalar>,
>(
self,
ctx: &mut A::Context,
schip: &A::ScalarChip,
pchip: &A,
one: &A::AssignedScalar,
) -> Result<(A::AssignedPoint, Option<A::AssignedScalar>), A::Error> {
Based on this trait, we will be able to implement some universal code base for verifying code (executable files to generate witness), verifying circuit(can be used for proof aggregator) and solidity code.
then by providing different trait implementation of scalar, basefield and ecc points, we can use the same code base for both executable verifier and verifying circuit.
2. Proof Aggregation Approach
2.1. Top level sketch:
Suppose that verifying a single proof of a target circuit
- Query Constructing (read from transcript)
- Construct schema.
- Evaluate the multiopen result of
$W_x$ and$W_e$ such that$$(W_x[i], x) = (W_e[i], 1)$$ - Check the above pair.
Then by the linearity of pairing, we can construct random linear combinition of multiple
Motivated by the above thoughts, we split the process of verifying into 4 stages
-
- Argument Preparing
-
- Query Constructing (read from transcript) for multiple proofs
-
- Construct schema from queries of multiple proofs
-
- Construct the schema using the linear combination of the schemas from multiple proofs.
-
- Evaluate the multiopen result of the schema.
More precisely the top level pseudo code might looks like the following
pub fn verify_aggregation_proofs_in_chip<
E: MultiMillerLoop,
A: ArithEccChip<
Point = E::G1Affine,
Scalar = <E::G1Affine as CurveAffine>::ScalarExt,
Native = <E::G1Affine as CurveAffine>::ScalarExt,
>,
T: TranscriptRead<A>,
>(
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
pchip: &A,
mut circuits: Vec<CircuitProof<E, A, T>>,
transcript: &mut T,
) -> Result<
(
A::AssignedPoint, // w_x
A::AssignedPoint, // w_g
Vec<A::AssignedScalar>, // plain assigned instance
Vec<Vec<A::AssignedPoint>>, // advice commitments
),
A::Error>
{
let mut plain_assigned_instances = vec![];
let multiopen_proofs: Vec<Vec<(MultiOpenProof<A>, Vec<A::AssignedPoint>)>> = circuits
.iter_mut()
.map(|circuit_proof| {
let r = circuit_proof
.proofs
.iter_mut()
.map(|proof| {
...
let (assigned_instances, assigned_instance_commitments) =
assign_instance_commitment(
ctx,
schip,
pchip,
&instances2[..],
circuit_proof.vk,
circuit_proof.params,
)?;
for assigned_instance in assigned_instances {
plain_assigned_instances.push(assigned_instance)
}
let (p, c) = verify_single_proof_no_eval()?;
Ok((p,c))
})
.collect();
/* update aggregation challenge */
for p in circuit_proof.proofs.iter_mut() {
let scalar = p.transcript.squeeze_challenge_scalar(ctx, nchip, schip)?;
transcript.common_scalar(ctx, nchip, schip, &scalar)?;
}
return r;
})
.collect()?;
let aggregation_challenge = transcript.squeeze_challenge_scalar(ctx, nchip, schip)?;
let mut acc: Option<MultiOpenProof<A>> = None;
let mut commits: Vec<Vec<A::AssignedPoint>> = vec![];
for (proof, c) in proofs.into_iter() {
acc = match acc {
None => Some(proof),
Some(acc) => {
Some(MultiOpenProof {
w_x: acc.w_x * scalar!(aggregation_challenge) + proof.w_x,
w_g: acc.w_g * scalar!(aggregation_challenge) + proof.w_g,
})
}
};
commits.push(c)
}
let aggregated_proof = acc.unwrap();
evaluate_multiopen_proof::<E, A, T>(ctx, schip, pchip, aggregated_proof)
.map(|pair| (pair.0, pair.1, plain_assigned_instances, commits))
2.2. Calculating the Queries:
Ingredients of queries are decoded from transcripts. We implement the following trait for each context of schema:
Encode Trait
pub trait Encode<A: ArithEccChip> {
fn encode_point(
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
pchip: &A,
v: &A::AssignedPoint,
) -> Result<Vec<A::AssignedNative>, A::Error>;
fn encode_scalar(
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
v: &A::AssignedScalar,
) -> Result<Vec<A::AssignedNative>, A::Error>;
fn decode_scalar(
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
v: &[A::AssignedNative],
) -> Result<A::AssignedScalar, A::Error>;
}
Transcript Read Trait
pub trait TranscriptRead<A: ArithEccChip> {
fn read_point(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
pchip: &A,
) -> Result<A::AssignedPoint, A::Error>;
fn read_scalar(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
) -> Result<A::AssignedScalar, A::Error>;
fn read_constant_point(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
pchip: &A,
) -> Result<A::AssignedPoint, A::Error>;
fn read_constant_scalar(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
) -> Result<A::AssignedScalar, A::Error>;
fn common_point(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
pchip: &A,
p: &A::AssignedPoint,
) -> Result<(), A::Error>;
fn common_scalar(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
s: &A::AssignedScalar,
) -> Result<(), A::Error>;
fn squeeze_challenge_scalar(
&mut self,
ctx: &mut A::Context,
nchip: &A::NativeChip,
schip: &A::ScalarChip,
) -> Result<A::AssignedScalar, A::Error>;
}
2.3 Construct schemas
Schema is construct simply construct the multi-exp ast for queries:
pub fn batch_multi_open_proofs(
&self,
ctx: &mut A::Context,
schip: &A::ScalarChip,
) -> Result<MultiOpenProof<A>, A::Error> {
let proofs = self.get_point_schemas(ctx, schip)?;
let mut w_x = None;
let mut w_g = None;
for (i, p) in proofs.into_iter().enumerate() {
let s = &p.s;
let w = CommitQuery {
key: format!("{}_w{}", self.key, i),
commitment: Some(p.w.clone()),
eval: None,
};
w_x = w_x.map_or(Some(commit!(w)), |w_x| {
Some(scalar!(self.u) * w_x + commit!(w))
});
w_g = w_g.map_or(Some(scalar!(p.point) * commit!(w) + s.clone()), |w_g| {
Some(scalar!(self.u) * w_g + scalar!(p.point) * commit!(w) + s.clone())
});
}
Ok(MultiOpenProof {
w_x: w_x.unwrap(),
w_g: w_g.unwrap(),
})
}
Recall that at this stage no real calculation was performed but only schema (ast of mult-exp) is constructed.
Evaluate multi-exp:
After multi-exp for all proofs are constructed, we construct the final ast for multi-exp as follows:
for (proof, c) in proofs.into_iter() {
acc = match acc {
None => Some(proof),
Some(acc) => {
Some(MultiOpenProof {
w_x: acc.w_x * scalar!(aggregation_challenge) + proof.w_x,
w_g: acc.w_g * scalar!(aggregation_challenge) + proof.w_g,
})
}
};
commits.push(c)
}
acc.unwrap();
And eventually, we can start calculating the final result by
evaluate_multiopen_proof::<E, A, T>(ctx, schip, pchip, aggregated_proof)
.map(|pair| (pair.0, pair.1, plain_assigned_instances, commits))
Circuit structure
Base Arith Gate
#[derive(Clone, Debug)]
pub struct BaseGateConfig<const VAR_COLUMNS: usize, const MUL_COLUMNS: usize> {
pub base: [Column<Advice>; VAR_COLUMNS],
pub coeff: [Column<Fixed>; VAR_COLUMNS],
pub mul_coeff: [Column<Fixed>; MUL_COLUMNS],
pub next_coeff: Column<Fixed>,
pub constant: Column<Fixed>,
}
Transcript Chip
Base field Arith Chip
Ecc Arith Chip
Furture Work
- Wider arith base gate
- Multi-layer aggregator
License
Licensed under either of
- Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Appendix
Fp over fr materials
- Multiexp in TurboPlonk
- Aztec emulated field and group operations
- Implementing ECC addition in orchard using Halo2 (Zcash)
- Implementing Fp arithmetic in an Fq circuit (Zcash, R1CS)
- Xjsnark paper for Long Integer Arithmetic (R1CS)
Query layout:
digraph hierarchy {
rankdir="LR"
nodesep=1.0 // increases the separation between nodes
node[color=Black,fontname=Courier,shape=box] //All nodes will this shape and colour
edge [color=Black] //All the lines look like this
Queries->{
InstanceQueries
AdviceQueries
FixedQueries
PermutationQueries
LookupQueries
LocalPermutationQueries
VanishQueries
} // Put them on the same level
VanishQueries[color = red]
AdviceQueries-> {
AdviceCommitments
AdviceEvals
AdviceEvaluationPoints
}
InstanceQueries-> {
InstanceCommitments
InstanceEvals
InstanceEvaluationPoints
}
FixedQueries-> {
FixedEvals
FixedCommitments
FixedEvaluationPoints
}
LocalPermutationQueries -> {
LocalPermutationEval
LocalPermutationCommitment
LocalPermutationEvaluationPoints
}
VanishQueries -> {
VanishExpressions
VanishCommitment
VanishEvaluationPoints
}
PermutationQueries -> {
PermutationProductCommitments
PermutationProductEvals
PermutationEvaluationPoints
}
LookupQueries -> {
LookupCommitment
LookupEval
LookupEvaluationPoints
}
LocalPermutationCommitment -> Setup
FixedCommitments -> Setup
InstanceCommitments -> InputBeforeXChallenge
AdviceCommitments -> InputBeforeXChallenge
VanishCommitment -> InputBeforeXChallenge
InstanceEvals -> InputAfterXChallenge
AdviceEvals -> InputAfterXChallenge
FixedEvals -> InputAfterXChallenge
LocalPermutationEval -> InputBeforeXChallenge
LocalPermutationCommitment-> InputBeforeXChallenge
PermutationProductCommitments -> InputBeforeXChallenge
PermutationProductEvals -> InputAfterXChallenge
LocalPermutationEvaluationPoints-> xChallenge
PermutationEvaluationPoints -> xChallenge
FixedEvaluationPoints-> xChallenge
InstanceEvaluationPoints -> xChallenge
AdviceEvaluationPoints -> xChallenge
VanishEvaluationPoints -> xChallenge
LookupEvaluationPoints -> xChallenge
VanishExpressions -> xChallenge
xChallenge-> InputBeforeXChallenge
LookupCommitment -> InputBeforeXChallenge
LookupEval -> InputAfterXChallenge
}