Intro to PLONKish/halo2

0xPARC Halo2 Learning Group

13 Jun 2022

arithmetisation

polynomial commitment scheme

accumulation scheme

arithmetisation

polynomial commitment scheme

accumulation scheme

satisfying witness

relation

low-degree polynomial

PLONKish arithmetisation

polynomial commitment scheme

accumulation scheme

satisfying witness

relation

low-degree polynomial

deep dive: 22 Jun

PLONKish arithmetisation

polynomial commitment scheme

accumulation scheme

satisfying witness

relation

low-degree polynomial

commitment opening proof

commit to polynomial, and provably evaluate it at arbitrary points

PLONKish arithmetisation

inner product argument

accumulation scheme

satisfying witness

relation

low-degree polynomial

commitment opening proof

commit to polynomial, and provably evaluate it at arbitrary points

PLONKish arithmetisation

inner product argument

accumulation scheme

satisfying witness

relation

low-degree polynomial

commitment opening proof

commitment opening proof

Θ(log d) accumulator size; amortised Θ(d) final check cost

PLONKish arithmetisation

inner product argument

accumulation scheme

satisfying witness

relation

low-degree polynomial

commitment opening proof

commitment opening proof

Θ(log d) accumulator size; amortised Θ(d) final check cost

PLONKish arithmetisation

UltraPLONK [halo2]

​

​

​

​

TurboPLONK [GW19]

​

​

​

​

​

​

lookup tables

TurboPLONK [GW19]

​

​

​

​

​

custom constraints

PLONK [GWC19]

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

"local" consistency check: are all gate equations satisfied?

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

"local" consistency check: are all gate equations satisfied?

q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

"local" consistency check: are all gate equations satisfied?

q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

preprocessed selector polynomials

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

"local" consistency check: are all gate equations satisfied?

add: 1·x_a + 1·x_b + (-1)·x_c + 0·(x_ax_b) = 0

q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

PLONKish arithmetisation (vanilla)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• gates take two values as inputs, either add or multiply them, and then emit the result through an output wire;

"local" consistency check: are all gate equations satisfied?

add: 1·x_a + 1·x_b + (-1)·x_c + 0·(x_ax_b) = 0

mul: 0·x_a + 0·x_b + (-1)·x_c + 1·(x_ax_b) = 0

q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

PLONKish arithmetisation (custom gates)

TurboPLONK [GW19]

vanilla PLONK gate: q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

q_add·(a₀ + a₁ - a₂) = 0

custom gates (arbitrary linear combinations):

PLONKish arithmetisation (custom gates)

TurboPLONK [GW19]

vanilla PLONK gate: q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

q_add·(a₀ + a₁ - a₂) + q_mul·(a₀ · a₁ - a₂) = 0

custom gates (arbitrary linear combinations):

PLONKish arithmetisation (custom gates)

TurboPLONK [GW19]

vanilla PLONK gate: q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

q_add·(a₀ + a₁ - a₂) + q_mul·(a₀ · a₁ - a₂) + q_bool·(a₀·a₀ - a₀) = 0

custom gates (arbitrary linear combinations):

PLONKish arithmetisation (custom gates)

TurboPLONK [GW19]

vanilla PLONK gate: q_L·x_a + q_R·x_b + q_O·x_c + q_M·(x_ax_b) = 0

custom gates (arbitrary linear combinations):

q_add·(a₀ + a₁ - a₂) + y ·q_mul·(a₀ · a₁ - a₂) + y²· q_bool·(a₀·a₀ - a₀) = 0

PLONKish arithmetisation (permutation)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• wires carry values into and out of gates

PLONKish arithmetisation (permutation)

PLONK [GWC19]

+

⨉

w₀[0]

w₁[0]

w₁[1]

w₀[1]

w₂[1]

w₂[0]

• wires carry values into and out of gates

"global" consistency check: do the wires correctly join the gates together?

​

* in Groth16, routing is baked into the trusted setup; we can't do this for universal SNARKs

PLONKish arithmetisation (permutation)

PLONK [GWC19]

each wire (column i) is encoded as a Lagrange polynomial w_i over the powers (rows) of an n^th root of unity {1, ⍵, …,⍵^n-1}, where ⍵ⁿ = 1:

w_i(⍵^j) = w_i[j]

PLONKish arithmetisation (permutation)

PLONK [GWC19]

each wire (column i) is encoded as a Lagrange polynomial w_i over the powers (rows) of an n^th root of unity {1, ⍵, …,⍵^n-1}, where ⍵ⁿ = 1:

w_i(⍵^j) = w_i[j]

​

to enforce equality of wires, use permutation argument (deep-dive); show that swapping w₂(⍵⁰) with w₀(⍵¹) doesn't change the polynomials.

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

problem: SHA is expensive to do in-circuit

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

solution: load precomputed SHA (e.g. for 8-bit values) as lookup table

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

(q_lookup·w₀, t₀)

(q_lookup·w₁, t₁)

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

(q_lookup·w₀ + (1 - q_lookup)·0, t₀)

(q_lookup·w₁ + (1 - q_lookup)·SHA(0), t₁)

lookup default value when q_lookup is not enabled, so that lookup argument passes on every row

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

the lookup argument is a more permissive version of the permutation argument. it enforces that:�

every cell in a set of input columns is equal to� some cell in a set of table columns

PLONKish arithmetisation (lookup)

UltraPLONK [halo2]

the lookup argument is a more permissive version of the permutation argument. it enforces that:�

every expression in a set of input columns is equal to� some expression in a set of table columns

more on this in the deep-dive!

PLONKish arithmetisation

we conceptualise the circuit as a matrix of m columns and n rows

PLONKish arithmetisation

​

we conceptualise the circuit as a matrix of m columns and n rows,�over a given finite field 𝔽 (so the cells contain elements of 𝔽)

PLONKish arithmetisation

​

each column j corresponds to a Lagrange interpolation polynomial p_j(X)

PLONKish arithmetisation

​

each column j corresponds to a Lagrange interpolation polynomial p_j(X)�evaluating to p_j(⍵ⁱ) = x_ij, where ⍵ is the n^th primitive root of unity.

x_ij

PLONKish arithmetisation

instance columns contain inputs shared between prover/verifier (e.g. public inputs)

PLONKish arithmetisation

advice columns contain private values witnessed by the prover

PLONKish arithmetisation

fixed columns contain preprocessed values set at key generation

example: Fibonacci sequence

write this in tomorrow's session!

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

+ =

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_0,next) = 0

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_0,next) = 0

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

q_fib·(a_1,cur + a_2,cur - a_1,next) = 0

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_0,next) = 0

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

q_fib·(a_1,cur + a_2,cur - a_1,next) = 0

global permutation: a₂[i] = a₀[i + 1]

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_0,next) = 0

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

q_fib·(a_1,cur + a_2,cur - a_1,next) = 0

global permutation: a₂[i] = a₀[i + 1]

exercise: can you see how to constrain this locally (using q_fib)?

example: Fibonacci sequence

q_fib·(a_0,cur + a_1,cur - a_0,next) = 0

q_fib·(a_0,cur + a_1,cur - a_2,cur) = 0

q_fib·(a_1,cur + a_2,cur - a_1,next) = 0

global permutation:

• i₀[0] = a₀[0] // initialisation
• i₀[0] = a₁[0] // initialisation
• i₀[2] = a₂[2] // output

PLONKish arithmetisation

​

how do we optimise global layout while reasoning about local offsets?

PLONKish arithmetisation

​

regions!

regions

"regions" are the boundary between gates and the global circuit layouter

• a block of assignments preserving relative offsets: easy to reason about how gates apply within the region�
• not affected by offsets in other regions: can be freely rearranged to optimise global space usage

​

layouter

single-pass layouter (2¹² rows)

layouter

dual-pass layouter (2¹¹ rows)

single-pass layouter (2¹² rows)

halo2_gadgets

Sinsemilla

Poseidon

2¹⁰ lookup table of indexed Sinsemilla generators:

​

(i, P[i]_x, P[i]_y)

halo2_gadgets

ECC

SHA256 (experimental)

open problems / wishlist

• DSL / intermediate representation
• add an API to construct a Halo 2 circuit from a set of constraints (halo2#550)
• improve connection between gate configuration and assignment (halo2#365)
• multi-phase prover (halo2#593)
• dynamic lookup tables (halo2#534)

​

• what other features would you like to see?

arithmetisation (cont.)

1. arithmetise statement using UltraPLONK circuit

arithmetisation (cont.)

• arithmetise statement using UltraPLONK circuit
• commit to polynomials encoding the main components of the circuit;

Commit(p) = ∑ⁿ [p[i]]G_i,

where i = [0..=n], and G_i's are commitments to the Lagrange basis polynomials

a_i(X)

advice polys

f_i(X)

fixed polys

arithmetisation (cont.)

• arithmetise statement using UltraPLONK circuit
• commit to polynomials encoding the main components of the circuit;
• construct vanishing argument to constrain all circuit relations to zero;

where t(X) is the vanishing polynomial on the domain {ω⁰,…,ω^n-1}; in other words, t(X) = Xⁿ-1

arithmetisation (cont.)

• arithmetise statement using UltraPLONK circuit
• commit to polynomials encoding the main components of the circuit;
• construct vanishing argument to constrain all circuit relations to zero;
• evaluate the above polynomials at all necessary points;

a₀(x), a₀(⍵x), a₁(⍵x),…

f₀(x), f₁(⍵x), f₁(⍵^-1x),…

arithmetisation (cont.)

• arithmetise statement using UltraPLONK circuit
• commit to polynomials encoding the main components of the circuit;
• construct vanishing argument to constrain all circuit relations to zero;
• evaluate the above polynomials at all necessary points;
• construct the multipoint opening argument to check that all evaluations are consistent with their respective commitments;

1. group commitments by the sets of points at which they were queried:���
2. construct polynomials to accumulate polynomials at each point set; sample x₁ to keep them linearly independent:�� q₀(X) = A₀(X) + x₁·A₁(X)� q₁(X) = A₂(X) + x₁·A₃(X)�
3. evaluate the q_i's at their respective points: q₀(x), q₁(x), q₁(⍵x)

multipoint opening argument

{x}

A₀

A₁

{x, ⍵x}

A₂

A₃

• at each query point, interpolate the relevant q_i evaluations:� r₀(X) s.t. r₀(x) = A₀(x) + x₁·A₁(x);�� r₁(X) s.t.�
• construct polynomials to check the correctness of q_i polynomials�� f₀(X) =�� f₁(X) =�
• construct f(X) = f₀(X) + x₂·f₁(X), with random x₂ to keep f_i polynomials linearly independent

multipoint opening argument

r₁(x) = A₂(x) + x₁·A₃(x)

r₁(⍵x) = A₂(⍵x) + x₁·A₃(⍵x)

q₀(X) - r₀(X)

X - x

q₁(X) - r₁(X)

(X - x)(X - ⍵x)

multipoint opening argument

• construct�� final_poly(X) = f(X) + x₄·q₀(X) + x₄²·q₁(X),��with random x₄ challenge to keep polynomials linearly independent.��this checks that all evaluations are consistent with their respective commitments.

polynomial commitment scheme

Setup(): generates a setup pk

​

Commit(pk, P): creates a commitment c to P

VerifyPoly(pk, c, P): checks c is a valid commitment to P

​

Open(pk, P, x): generates an opening proof π

VerifyOpen(pk, c, x, y, π): checks if y = P(x) using π

added in "Math Building Blocks" (15 Jun)

arithmetisation

polynomial commitment scheme

accumulation scheme

satisfying witness

relation

low-degree polynomial

commitment opening proof

commitment opening proof

Θ(log d) accumulator size; amortised Θ(d) final check cost

PLONKish arithmetisation +�vanishing argument, multipoint opening argument

inner product argument

accumulation scheme

satisfying witness

relation

final_poly

commitment opening proof

commitment opening proof

Θ(log d) accumulator size; amortised Θ(d) final check cost

inner product argument

Setup(1^λ,d) produces a crs σ = (𝔾, 𝔽_p, G, H) for group 𝔾 of � prime order p, with random G ∈ 𝔾^d and H ∈ 𝔾.

​

Commit(σ, p(X); r): P =〈a, G〉 + [r]H, where a_i∈𝔽 is the coeff � for the i^th deg term in p(X), i ∈ [0,d)

VerifyPoly(pk, P, p): checks that P =〈a, G〉 + [r]H

​

Open(pk, p, x): generates an opening proof π for y = p(x)� =〈a, (1,x,…,x^d-1)〉

VerifyOpen(pk, C, x, y, π): checks y =〈a, (1,x,…,x^d-1)〉using π

added in "Math Building Blocks" (15 Jun)

NOT trusted!

inner product argument

Setup(1^λ,d) produces a crs σ = (𝔾, 𝔽_p, G, H) for group 𝔾 of � prime order p, with random G ∈ 𝔾^d and H ∈ 𝔾.

​

Commit(σ, p(X); r): P =〈a, G〉 + [r]H, where a_i∈𝔽 is the coeff � for the i^th deg term in p(X), i ∈ [0,d)

VerifyPoly(pk, P, p): checks that P =〈a, G〉 + [r]H

​

Open(pk, p, x): generates an opening proof π for y = p(x)� =〈a, (1,x,…,x^d-1)〉

VerifyOpen(pk, C, x, y, π): checks y =〈a, (1,x,…,x^d-1)〉using π

naive opening proof: send a (O(n) communication)

want: π with O(log d) communication

added in "Math Building Blocks" (15 Jun)

inner product argument�(originally from [Bootle et al, 2016])

we have vectors a, b each of length d = 2^k. we want to prove that a given inner product c and a commitment P are related as:

y = ⟨a, b⟩

P = ⟨a, G⟩ + ⟨b, H⟩

where G, H are length-n vectors of random group elements.�

we can combine this into a single commitment P_k using a random group element U:

P_k = P + [y]U = ⟨a, G⟩ + ⟨b, H⟩ + [⟨a, b⟩]U�

the naive solution would be to send the verifier a, b — but this requires sending 2d scalars. instead, the inner product argument uses O(log(d)) = O(k) communication cost.

a^(k)

b^(k)

added in "Math Building Blocks" (15 Jun)

modified inner product argument

we have vectors a, b each of length d = 2^k.

fix b = (1, x, x²,…,x^d-1) for a chosen evaluation point x, known to both prover and verifier. since b is known, no random vector H is needed.

we want to prove that v, which is an evaluation of a at x, and a commitment P are related as:

v = ⟨a, (1, x, x²,…,x^d-1)⟩

P = ⟨a, G⟩ + [r]H

where G is a length-n vector of random group elements.

we can combine this into a single commitment P_k using a random group element U:

P_k = P + [v]U = ⟨a, G⟩ + [r]H + [⟨a, b⟩]U

a^(k)

b^(k)

added in "Math Building Blocks" (15 Jun)

modified inner product argument

we start at the k^th round, where we split a, b, G into lo and hi halves. we introduce a random challenge u_k and compress the vectors by adding the left and the right halves separated by u_k:�

a^(k-1) = u_k · a_lo^(k) + u_k^-1 · a_hi^(k)

b^(k-1) = u_k^-1 · b_lo^(k) + u_k · b_hi^(k)

G^(k-1) = u_k^-1 · G_lo^(k) + u_k · G_hi^(k)

�now, we can write a commitment P_k-1 (of the same form as P_k) using the compressed vectors:

P_k-1 = ⟨a^(k-1), G^(k-1)⟩ + [⟨a^(k-1), b^(k-1)⟩] U

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

added in "Math Building Blocks" (15 Jun)

modified inner product argument

we can examine the compressed P_k-1 equation in terms of the original vectors:

P_k-1 = ⟨a^(k-1), G^(k-1)⟩ + [⟨a^(k-1), b^(k-1)⟩]U

= ⟨u_k·a_lo + u_k^-1·a_hi, u_k^-1·G_lo + u_k·G_hi⟩ +

[⟨u_k·a_lo+ u_k^-1·a_hi, u_k^-1·b_lo + u_k·b_hi⟩]U

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

added in "Math Building Blocks" (15 Jun)

modified inner product argument

we can examine the compressed P_k-1 equation in terms of the original vectors:

P_k-1 = ⟨a^(k-1), G^(k-1)⟩ + [⟨a^(k-1), b^(k-1)⟩]U

= ⟨u_k·a_lo + u_k^-1·a_hi, u_k^-1·G_lo + u_k·G_hi⟩ +

[⟨u_k·a_lo+ u_k^-1·a_hi, u_k^-1·b_lo + u_k·b_hi⟩]U

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

P_k-1 = ⟨a_lo,G_lo⟩ + ⟨a_hi,G_hi⟩ + u_k² ⟨a_lo,G_hi⟩ + u_k^-2 ⟨a_hi,G_lo⟩ +

[⟨a_lo,b_lo⟩ + ⟨a_hi,b_hi⟩)]U + [u_k² ⟨a_lo,b_hi⟩ + u_k^-2 ⟨a_hi,b_lo⟩]U

= P_k + [u_k²] L_k + [u_k^-2] R_k

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

P_k-1 = P_k + [u_k²]L_k + [u_k^-2]R_k

P_k-1 is the sum of P_k and the cross-terms L_k, R_k (with coefficients from the round challenge u_k)

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

round k-1

we repeat this in the k-1^st round, defining the new compressed eqn

​

P_k-2 = ⟨a^(k-2),G^(k-2)⟩ + [⟨a^(k-2),b^(k-2)⟩]U

u_k-1·a_lo^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

we repeat this in the k-1^st round, defining the new compressed eqn

​

P_k-2 = ⟨a^(k-2),G^(k-2)⟩ + [⟨a^(k-2),b^(k-2)⟩]U

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

and deriving new cross-terms

L_k-1, R_k-1 such that

​

P_k-2 = P_k-1 + [u_k-1²]L_k-1 + [u_k-1^-2]R_k-1

round k-1

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

we repeat this in the k-1^st round, defining the new compressed eqn

​

P_k-2 = ⟨a^(k-2),G^(k-2)⟩ + [⟨a^(k-2),b^(k-2)⟩]U

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

and deriving new cross-terms

L_k-1, R_k-1 such that

​

P_k-2 = P_k-1 + [u_k-1²]L_k-1 + [u_k-1^-2]R_k-1

� = P_k + [u_k²]L_k + [u_k^-2]R_k

+ [u_k-1²]L_k-1 + [u_k-1^-2]R_k-1

round k-1

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

�a^(k-2)

�b^(k-2)

round k-1

round k-2

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

�a^(k-2)

�b^(k-2)

round k-1

round k-2

…

…

…

…

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

�a^(k-2)

�b^(k-2)

round k-1

round k-2

…

…

…

…

round 1

�a⁽⁰⁾

�b⁽⁰⁾

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

�a^(k-2)

�b^(k-2)

round k-1

round k-2

…

…

…

…

round 1

�a⁽⁰⁾

�b⁽⁰⁾

added in "Math Building Blocks" (15 Jun)

modified inner product argument

a^(k)

b^(k)

�u_k·a_lo^(k)

�u_k^-1·a_hi^(k)

�u_k·b_hi^(k)

�u_k^-1·b_lo^(k)

round k

�a^(k-1)

�b^(k-1)

u_k-1^-1·a_hi^(k-1)

u_k-1·a_lo^(k-1)

u_k-1^-1·b_lo^(k-1)

u_k-1·b_hi^(k-1)

�a^(k-2)

�b^(k-2)

round k-1

round k-2

…

…

…

…

round 1

�a⁽⁰⁾

�b⁽⁰⁾

our proof is now just 2k - 1 field elements!

added in "Math Building Blocks" (15 Jun)

modified inner product argument

P₀ = [a⁽⁰⁾]G⁽⁰⁾ + [a⁽⁰⁾·b⁽⁰⁾] U

but P₀ = ∑^k([u_j²] L_j) + P_k + ∑^k([u_j^-2] R_j)

​

verifier checks this equivalence

​

[a]G + [a·b] U == ∑^k([u_j²] L_j) + P_k + ∑^k([u_j^-2] R_j)

added in "Math Building Blocks" (15 Jun)

modified inner product argument

P₀ = [a⁽⁰⁾]G⁽⁰⁾ + [a⁽⁰⁾·b⁽⁰⁾] U