The GKR protocol

The GKR protocol Goldwasser, Kalai, Rothblum lets a verifier check the claim D about the outputs of a layered arithmetic circuit on an input x over a finite field F, following Thaler, §4.6. Claims about a layer are claims W̃_j(z) = v about the multilinear extension of its gate values (Cslib.Interactive.GKR.LayerClaim).

• The output step (LayeredCircuit.outputStep) draws a uniform point r of the output layer and reduces the claim D to W̃_depth(r) = D̃(r); a wrong D survives with probability at most width depth / |F| (Schwartz–Zippel).
• Each layer (LayeredCircuit.layer) reduces a claim about layer i + 1 at z to a claim about layer i. It runs sumcheck on the GKR summand f_z (sumcheckStage, the library's Sumcheck.rounds bundled over z by Reduction.bundle), and then the line step (lineStep): the prover sends the restriction q of W̃_i to the line through the two halves y, w of the last sumcheck point, the verifier checks the last sumcheck claim against q 0 = W̃_i(y) and q 1 = W̃_i(w), draws t and keeps the claim W̃_i(ℓ(t)) = q(t).
• The input step (inputStep) evaluates x̃ at the last point.

The protocol (LayeredCircuit.protocol) is perfectly complete (protocol_complete) and sound with error (width depth + ∑_{i < depth} 5 · width i) / |F| (protocol_sound): 2 / |F| for each of the 2 · width i sumcheck rounds of layer i, width i / |F| for its line step, and width depth / |F| for the output step. Both follow from the component theorems by the composition theorems for completeness and round-by-round soundness. Verifier efficiency, which needs uniformity of the circuit, is not addressed: the verifier evaluates the wiring extensions directly.

Main definitions

• Cslib.Interactive.GKR.LayeredCircuit.outputStep, Cslib.Interactive.GKR.LayeredCircuit.layer, Cslib.Interactive.GKR.LayeredCircuit.lineStep, Cslib.Interactive.GKR.LayeredCircuit.inputStep: the stages.
• Cslib.Interactive.GKR.LayeredCircuit.protocol: the GKR protocol.

Main results

• Cslib.Interactive.GKR.LayeredCircuit.protocol_complete: perfect completeness.
• Cslib.Interactive.GKR.LayeredCircuit.protocol_sound: soundness.
• Cslib.Interactive.GKR.LayeredCircuit.toOuterMeasure_eval_eq_zero_le: Schwartz–Zippel at a uniform point.

References

• S. Goldwasser, Y. T. Kalai, G. N. Rothblum, Delegating computation: interactive proofs for muggles
• J. Thaler, Proofs, Arguments, and Zero-Knowledge, Section 4.6

def Cslib.Interactive.GKR.line {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) (t : F) : Fin k → F

The line through y (at 0) and w (at 1).

theorem Cslib.Interactive.GKR.line_zero {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) : line y w 0 = y

theorem Cslib.Interactive.GKR.line_one {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) : line y w 1 = w

noncomputable def Cslib.Interactive.GKR.restrictLine {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) (W : (Fin k → Bool) → F) : Polynomial F

The multilinear extension of W, restricted to the line through y and w: a polynomial of degree at most k in the line parameter.

theorem Cslib.Interactive.GKR.eval_restrictLine {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) (W : (Fin k → Bool) → F) (t : F) : Polynomial.eval t (restrictLine y w W) = (MvPolynomial.eval (line y w t)) (BitString.multilinearExtension W)

theorem Cslib.Interactive.GKR.natDegree_restrictLine_le {F : Type} [Field F] {k : ℕ} (y w : Fin k → F) (W : (Fin k → Bool) → F) : (restrictLine y w W).natDegree ≤ k

The line step

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayerClaim (C : LayeredCircuit) (F : Type) (j : ℕ) : Type

A claim about layer j: a point z and the claimed value of the multilinear extension of the layer at z, stored as a sumcheck claim of round 0.

@[reducible, inline]

abbrev Cslib.Interactive.GKR.SumcheckEnd (C : LayeredCircuit) (F : Type) (i : ℕ) : Type

A sumcheck claim of the last round of layer i, at the point z of layer i + 1.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.combine {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (z : Fin (C.width (i + 1)) → F) (y w : Fin (C.width i) → F) (u v : F) : F

The combination the verifier checks against the last sumcheck claim: ãdd_i(z, y, w) (u + v) + m̃ult_i(z, y, w) u v.

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.lineAccepts {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (x : SumcheckEnd C F i) (q : Polynomial F) : Prop

The verifier's test of the line polynomial q against the last sumcheck claim (z, r, c).

def Cslib.Interactive.GKR.LayeredCircuit.lineClaim {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (x : SumcheckEnd C F i) (q : Polynomial F) (t : F) : LayerClaim C F i

The claim about layer i at the point t of the line.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.lineStep {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Reduction OracleSpec.empty OracleSpec.empty (Sumcheck.roundSpec F) (SumcheckEnd C F i) Unit (LayerClaim C F i) Unit

The line step of layer i, for the values W of layer i. The prover sends the restriction q of W̃ to the line through the two halves y, w of the last sumcheck point; the verifier checks the last sumcheck claim against q 0 = W̃(y) and q 1 = W̃(w), draws t and outputs the claim W̃(ℓ(t)) = q(t).

theorem Cslib.Interactive.GKR.LayeredCircuit.lineStep_outputOn {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) (x : SumcheckEnd C F i) (τ : (Sumcheck.roundSpec F).Transcript) : (C.lineStep i W).verifier.outputOn x τ = if C.lineAccepts i x τ.1 then some (C.lineClaim i x τ.1 τ.2.1) else none

def Cslib.Interactive.GKR.LayeredCircuit.layerLang {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Set (LayerClaim C F i)

The claims about layer i that are true.

def Cslib.Interactive.GKR.LayeredCircuit.endLang {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Set (SumcheckEnd C F i)

The true last sumcheck claims of layer i.

theorem Cslib.Interactive.GKR.LayeredCircuit.mem_endLang {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) (x : SumcheckEnd C F i) : x ∈ C.endLang i W ↔ (MvPolynomial.eval x.snd.1) (C.summand i W x.fst) = x.snd.2

theorem Cslib.Interactive.GKR.LayeredCircuit.combine_restrictLine {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) (x : SumcheckEnd C F i) : C.combine i x.fst (x.snd.1 ∘ Fin.castAdd (C.width i)) (x.snd.1 ∘ Fin.natAdd (C.width i)) (Polynomial.eval 0 (restrictLine (x.snd.1 ∘ Fin.castAdd (C.width i)) (x.snd.1 ∘ Fin.natAdd (C.width i)) W)) (Polynomial.eval 1 (restrictLine (x.snd.1 ∘ Fin.castAdd (C.width i)) (x.snd.1 ∘ Fin.natAdd (C.width i)) W)) = (MvPolynomial.eval x.snd.1) (C.summand i W x.fst)

The honest line polynomial passes the check exactly when the last sumcheck claim is true.

theorem Cslib.Interactive.GKR.LayeredCircuit.lineStep_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Reduction.Complete World.plain (C.lineStep i W) (fun (x : SumcheckEnd C F i) (x_1 : Unit) => x ∈ C.endLang i W) (fun (y : LayerClaim C F i) (x : Unit) => y ∈ C.layerLang i W) 0

The line step is perfectly complete.

theorem Cslib.Interactive.GKR.LayeredCircuit.lineStep_rbrSound {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : (C.lineStep i W).verifier.RbrSound (C.endLang i W) (C.layerLang i W) (↑(C.width i) / ↑(Fintype.card F), ())

The line step is round-by-round sound with error width i / |F|: a false last sumcheck claim forces a line polynomial other than the true restriction, which agrees with it at a random point with probability at most width i / |F|.

The sumcheck stage and one layer

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.sumcheckVars (C : LayeredCircuit) (i : ℕ) : ℕ

The number of sumcheck variables of layer i.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.sumcheckSamplers {F : Type} [Field F] [Fintype F] (k : ℕ) : Spec.PerChallenge ProbComp (iterSpec (fun (x : ℕ) => Sumcheck.roundSpec F) k)

The challenge samplers of k sumcheck rounds: one uniform field element per round.

theorem Cslib.Interactive.GKR.LayeredCircuit.samplers_iterate_round {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (k : ℕ) : (Reduction.iterate (Sumcheck.round d P) k).verifier.samplers = sumcheckSamplers k

The challenge samplers of the iterated sumcheck rounds do not depend on the polynomial.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.sumcheckStage {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Reduction OracleSpec.empty OracleSpec.empty (iterSpec (fun (x : ℕ) => Sumcheck.roundSpec F) (C.sumcheckVars i)) (LayerClaim C F (i + 1)) Unit (SumcheckEnd C F i) Unit

The sumcheck stage of layer i, for the values W of layer i: on a claim (z, v) about layer i + 1, sumcheck on the summand f_z, bundled over z.

theorem Cslib.Interactive.GKR.LayeredCircuit.mem_language_rel_zero {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) (x : LayerClaim C F (i + 1)) : x.snd ∈ language (Sumcheck.rel (C.summand i W x.fst) 0) ↔ x ∈ C.layerLang (i + 1) (C.step i W)

A round-0 sumcheck claim on the summand is a claim about the multilinear extension of the layer above.

theorem Cslib.Interactive.GKR.LayeredCircuit.sumcheckStage_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : Reduction.Complete World.plain (C.sumcheckStage i W) (fun (x : LayerClaim C F (i + 1)) (x_1 : Unit) => x ∈ C.layerLang (i + 1) (C.step i W)) (fun (y : SumcheckEnd C F i) (x : Unit) => y ∈ C.endLang i W) 0

The sumcheck stage is perfectly complete.

theorem Cslib.Interactive.GKR.LayeredCircuit.sumcheckStage_rbrSound {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (i : ℕ) (W : (Fin (C.width i) → Bool) → F) : (C.sumcheckStage i W).verifier.RbrSound (C.layerLang (i + 1) (C.step i W)) (C.endLang i W) (PerChallenge.iterate (fun (x : ℕ) => (2 / ↑(Fintype.card F), ())) (C.sumcheckVars i))

The sumcheck stage is round-by-round sound with error 2 / |F| per round.

The output and input steps

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.outputSpec {F : Type} (C : LayeredCircuit) : Spec

The single round of the output step: the verifier draws a point of the output layer.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.outputStep {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) : Reduction OracleSpec.empty OracleSpec.empty C.outputSpec ((Fin (C.width C.depth) → Bool) → F) Unit (LayerClaim C F C.depth) Unit

The output step: on claimed outputs D, the verifier draws a point r of the output layer and turns the claim into W̃_depth(r) = D̃(r).

theorem Cslib.Interactive.GKR.LayeredCircuit.outputStep_outputOn {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (D : (Fin (C.width C.depth) → Bool) → F) (τ : C.outputSpec.Transcript) : C.outputStep.verifier.outputOn D τ = some ⟨τ.1, (Fin.elim0, (MvPolynomial.eval τ.1) (BitString.multilinearExtension D))⟩

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.inputStep {F : Type} [Field F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Reduction OracleSpec.empty OracleSpec.empty [] (LayerClaim C F 0) Unit Unit Unit

The input step: the verifier checks the claim about the input layer by evaluating the multilinear extension of the input.

theorem Cslib.Interactive.GKR.LayeredCircuit.toOuterMeasure_eval_eq_zero_le {F : Type} [Field F] [Fintype F] {k d : ℕ} {p : MvPolynomial (Fin k) F} (hp : p ≠ 0) (hdeg : p.totalDegree ≤ d) : (ProbComp.uniform (Fin k → F)).eval.toOuterMeasure {r : Fin k → F | (MvPolynomial.eval r) p = 0} ≤ ↑d / ↑(Fintype.card F)

Schwartz–Zippel at a uniform point: a nonzero polynomial of total degree at most d vanishes with probability at most d / |F|.

theorem Cslib.Interactive.GKR.LayeredCircuit.totalDegree_multilinearExtension_sub_le {F : Type} [Field F] {k : ℕ} (D E : (Fin k → Bool) → F) : (BitString.multilinearExtension D - BitString.multilinearExtension E).totalDegree ≤ k

theorem Cslib.Interactive.GKR.LayeredCircuit.multilinearExtension_sub_ne_zero {F : Type} [Field F] {k : ℕ} {D E : (Fin k → Bool) → F} (h : D ≠ E) : BitString.multilinearExtension D - BitString.multilinearExtension E ≠ 0

Distinct functions on the cube have distinct multilinear extensions.

theorem Cslib.Interactive.GKR.LayeredCircuit.outputStep_complete {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Reduction.Complete World.plain C.outputStep (fun (D : (Fin (C.width C.depth) → Bool) → F) (x_1 : Unit) => D = C.output x) (fun (y : LayerClaim C F C.depth) (x_1 : Unit) => y ∈ C.layerLang C.depth (C.value x C.depth)) 0

The output step is perfectly complete.

theorem Cslib.Interactive.GKR.LayeredCircuit.outputStep_rbrSound {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : C.outputStep.verifier.RbrSound {C.output x} (C.layerLang C.depth (C.value x C.depth)) (↑(C.width C.depth) / ↑(Fintype.card F), ())

The output step is round-by-round sound with error width depth / |F|, by Schwartz–Zippel for the multilinear extensions of the claimed and the true outputs.

theorem Cslib.Interactive.GKR.LayeredCircuit.inputStep_complete {F : Type} [Field F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Reduction.Complete World.plain (C.inputStep x) (fun (y : LayerClaim C F 0) (x_1 : Unit) => y ∈ C.layerLang 0 x) Accept 0

The input step is perfectly complete.

theorem Cslib.Interactive.GKR.LayeredCircuit.inputStep_rbrSound {F : Type} [Field F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : (C.inputStep x).verifier.RbrSound (C.layerLang 0 x) Set.univ ()

The input step is round-by-round sound without error.

The protocol

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.layerSpec {F : Type} [Field F] (C : LayeredCircuit) (i : ℕ) : Spec

The rounds of layer i: sumcheck on 2 · width i variables, then the line step.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.layer {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (i : ℕ) : Reduction OracleSpec.empty OracleSpec.empty (C.layerSpec i) (LayerClaim C F (i + 1)) Unit (LayerClaim C F i) Unit

One layer of GKR: a claim about layer i + 1 becomes a claim about layer i.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.layerError {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (i : ℕ) : Spec.PerChallenge (fun (x : Type) => ENNReal) (C.layerSpec i)

The per-round errors of layer i: 2 / |F| per sumcheck round and width i / |F| for the line step.

theorem Cslib.Interactive.GKR.LayeredCircuit.layer_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (i : ℕ) : Reduction.Complete World.plain (C.layer x i) (fun (y : LayerClaim C F (i + 1)) (x_1 : Unit) => y ∈ C.layerLang (i + 1) (C.value x (i + 1))) (fun (y : LayerClaim C F i) (x_1 : Unit) => y ∈ C.layerLang i (C.value x i)) 0

theorem Cslib.Interactive.GKR.LayeredCircuit.layer_rbrSound {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (i : ℕ) : (C.layer x i).verifier.RbrSound (C.layerLang (i + 1) (C.value x (i + 1))) (C.layerLang i (C.value x i)) (C.layerError i)

theorem Cslib.Interactive.GKR.LayeredCircuit.sum_layerError {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (i : ℕ) : PerChallenge.sum (C.layerSpec i) (C.layerError i) = ↑(C.sumcheckVars i) * (2 / ↑(Fintype.card F)) + ↑(C.width i) / ↑(Fintype.card F)

def Cslib.Interactive.GKR.LayeredCircuit.descendSpec {F : Type} [Field F] (C : LayeredCircuit) : ℕ → Spec

The rounds from layer m down to the input.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.descend {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (m : ℕ) : Reduction OracleSpec.empty OracleSpec.empty (C.descendSpec m) (LayerClaim C F m) Unit Unit Unit

The layers from m down to the input, followed by the input step.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.descendError {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (m : ℕ) : Spec.PerChallenge (fun (x : Type) => ENNReal) (C.descendSpec m)

The per-round errors of descend.

theorem Cslib.Interactive.GKR.LayeredCircuit.descend_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (m : ℕ) : Reduction.Complete World.plain (C.descend x m) (fun (y : LayerClaim C F m) (x_1 : Unit) => y ∈ C.layerLang m (C.value x m)) Accept 0

theorem Cslib.Interactive.GKR.LayeredCircuit.descend_rbrSound {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) (m : ℕ) : (C.descend x m).verifier.RbrSound (C.layerLang m (C.value x m)) Set.univ (C.descendError m)

theorem Cslib.Interactive.GKR.LayeredCircuit.sum_descendError {F : Type} [Field F] [Fintype F] (C : LayeredCircuit) (m : ℕ) : PerChallenge.sum (C.descendSpec m) (C.descendError m) = ∑ i ∈ Finset.range m, (↑(C.sumcheckVars i) * (2 / ↑(Fintype.card F)) + ↑(C.width i) / ↑(Fintype.card F))

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.protocol {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Reduction OracleSpec.empty OracleSpec.empty (C.outputSpec ++ C.descendSpec C.depth) ((Fin (C.width C.depth) → Bool) → F) Unit Unit Unit

The GKR protocol for the claim that the circuit outputs D on the input x: the output step, then the layers from the output down to the input, then the input step.

theorem Cslib.Interactive.GKR.LayeredCircuit.protocol_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Reduction.Complete World.plain (C.protocol x) (fun (D : (Fin (C.width C.depth) → Bool) → F) (x_1 : Unit) => D = C.output x) Accept 0

Completeness of GKR: the honest prover convinces the verifier of the true output with probability one.

theorem Cslib.Interactive.GKR.LayeredCircuit.protocol_sound {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : LayeredCircuit) (x : (Fin (C.width 0) → Bool) → F) : Verifier.Sound World.plain (C.protocol x).verifier {C.output x} Set.univ (↑(C.width C.depth + ∑ i ∈ Finset.range C.depth, 5 * C.width i) / ↑(Fintype.card F))

Soundness of GKR Goldwasser, Kalai, Rothblum, Thaler, §4.6: any prover convinces the verifier of a wrong output with probability at most (width depth + ∑_{i < depth} 5 · width i) / |F|.