Kilian's succinct arguments: PCP + collision-resistant hashing ⇒ succinct arguments for NP

Posted by coordinator-claude-c4b0c164-20261023 at Samuel's direction (2026-10-25). Part of the crypto program (#640, #643).

Goal

Kilian's succinct arguments: if collision-resistant hash families exist, every language in NP has an interactive argument with polylogarithmic communication (Kilian 1992). The library already has the PCP theorem (a curated headline) and keyed collision-resistant hash families (#678), so the main missing piece is the commitment layer. A second endpoint is the random-oracle version: Micali's CS proofs, or the BCS transform for IOPs. It ties this track to #643's sumcheck and GKR work.

Milestones

M0, design (a comment here before any Lean): exact statements and source locators. Candidates are Kilian STOC 1992; Barak–Goldreich, Universal arguments, for the careful analysis; Micali 2000; Ben-Sasson–Chiesa–Spooner, TCC 2016. M0 also fixes the argument model (computational soundness against PPT provers, with explicit communication and verifier time) and the reuse plan.
M1, Merkle-tree vector commitments from a collision-resistant family: position binding with a certified reduction, and opening size O(log n) hash values.
M2, Kilian's protocol: composing a PCP with M1, with completeness and computational soundness by extraction or rewinding, and an exact soundness loss.
M3, the succinctness accounting: communication and verifier time, kept separate from the PCP's query and randomness complexity.
M4 (optional), the random-oracle version: Micali or BCS, reusing the Fiat–Shamir random-oracle API.

Rules

The #897 shared rules apply. Security statements need certified efficient reductions (#733), plain-first statements (#456), and reuse of the existing PCP, hash and interactive APIs.

Claim and M0 design — worker-claude-kilian-c4b0c164 (Claude), delegated by coordinator-claude-c4b0c164-20261023. State: active on M0 and M1. Branch feat/kilian-merkle-999, worktree /home/samuel/Code/complexitylib-wt/999-1.

Sources

Checked against a fetched copy: Barak–Goldreich, Universal Arguments and their Applications, ECCC TR01-093 (the 2 Dec 2001 report; page numbers are the printed ones).

Theorem 1.1 (p. 3): "The existence of (standard) collision-free hashing functions implies the existence of universal arguments. Furthermore, these proof systems are of the public-coin (Arthur–Merlin [3]) type and use a constant number of rounds."
Definition 2.1 (p. 5): efficient verification; completeness by a relatively-efficient prover; computational soundness against polynomial-size circuit families, for each fixed (M, x, t) ∉ L_U; a weak proof of knowledge.
Definition 3.2 (p. 7): auxiliary PCP properties, among them "relatively-efficient oracle-construction" (a polynomial-time map from a witness to an accepted oracle).
Construction 3.4 (pp. 9–10), the adaptation of Kilian's construction. V1 sends a uniform α ∈ {0,1}^n. P1.3 builds the hashing tree: "The label of a leaf associated with γ ∈ {0,1}^d, denoted ℓ_γ, is the value of π_y at position γ … The label of an internal node associated with γ ∈ ∪_{i=0}^{d−1}{0,1}^i is the value obtained by applying h_α to the string ℓ_γ0 ℓ_γ1." P1.4 sends (d, ℓ_λ). V2 sends the PCP random tape. P2 sends the answers and the child labels along each path. V3 runs the PCP decision and checks ℓ'_γ = h_α(ℓ'_γ0 ℓ'_γ1).
Lemma 3.5 (p. 10): Construction 3.4 has the weak proof-of-knowledge property when {h_α} is collision-free.

Locators to be confirmed. These are not pinned anywhere until checked against a copy: Kilian, STOC 1992; Micali, Computationally sound proofs, SIAM J. Comput. 2000; Ben-Sasson–Chiesa–Spooner, TCC 2016-B; Catalano–Fiore, Vector commitments (for the name "position binding"). ePrint is behind a bot check from this machine, and the STOC and SIAM papers are not on arXiv or ECCC.

Argument model

Hash. The security parameter λ is unary and the key is k ← {0,1}^λ, for a HashFamily H (CollisionResistant.lean, uniform strict PPT collision resistance). BG's h_α resists non-uniform circuits, but the library has no non-uniform adversary model yet (feat(crypto): separate restricted and general auxiliary-input zero knowledge (#698) #704, feat(crypto): commitment hiding against a randomized stateful receiver (#682) #686), so every adversary is uniform.
Cheating provers are two-stage uniform strict PPT programs, following CommitmentReceiver: commit : (λ, k) ↦ ((x, root), state) and answer : (λ, state, coins) ↦ openings.
- The prover picks the statement x after seeing k. This is the uniform counterpart of BG's "for every y ∉ L_U": a fixed-y definition would need y as advice for the reduction.
- A prover with a fixed or efficiently sampled x is a special case.
Computational soundness: Pr[x ∉ L ∧ V accepts] is negligible in λ. The game decides x ∉ L classically; no reduction ever runs it.
Completeness: the honest prover takes a compact PCP proof π (below) as its witness and is accepted with probability 1. It runs in time polynomial in λ + |enc x| + |π|.
Resources (M3): communication is counted in bits of the honest transcript. Verifier time is a plain ComputableInPolyTime certificate in (λ, x, transcript). Both are stated separately from the PCP's randomness, query count and proof length.

Labelled gap: the witness relation. NP_subset_PCP_log only asserts that a PCP proof exists. The library has no polynomial-time map from an NP witness to that proof, which is BG Definition 3.2's oracle construction. The NP corollary is therefore: every L ∈ NP has an NP relation with a succinct argument whose prover is efficient on that relation. The relation is compact PCP proofs, checked by PCPVerifier.tableVerifier. Prover efficiency for an arbitrary given NP relation stays open, and will be recorded as open.

Reuse plan

Collision side: HashFamily, CollisionResistant, collisionGame, isCollision.
Security plumbing: Game.Indistinguishable with .of_reduction, Negligible, IsPPT/IsPPTOn.
PCP: PCPVerifier, IsPCPVerifier, NP_subset_PCP_log, and PCPVerifier.queryTable/tableVerifier (Classes/PCP/NP.lean).
- The compact proof is the bit table on queryTable x, and positions are idxOf into it.
- So the Merkle tree has polynomially many leaves, although PCP addresses are arbitrary binary numbers.
Provers: the two-stage pattern of CommitmentReceiver (Commitment.lean).
Interactive core. At fixed (λ, x) the protocol is an Interactive.Reduction on the spec [verifier (List Bool), prover (List Bool), verifier (List (List Bool)), prover (List (List Opening))], and completeness is Reduction.Complete World.plain … 0.
- Verifier.samplers cannot depend on the statement, and Kilian's challenge lengths depend on λ and x. So (λ, x) is the index, as the core's module docs prescribe for shapes.
- Computational soundness is a Crypto-layer notion on top; the core's Verifier.Sound is information-theoretic by design.
What is new. No Merkle tree or vector commitment exists in the library: Commitment.lean is Naor's bit commitment. M1's module is also what Signatures from one-way functions: Merkle trees to Rompel #1001's authentication trees need.

M1: Merkle-tree vector commitments (next, one PR)

New module Complexity/Crypto/Computational/MerkleTree.lean, namespace Cslib.Crypto.MerkleTree, for a keyed H : List Bool → List Bool → List Bool:

def parentLayer (H) (k : List Bool) (layer : List (List Bool)) : List (List Bool) :=
  (List.range ((layer.length + 1) / 2)).map fun m =>
    H k (layer.getD (2 * m) [] ++ layer.getD (2 * m + 1) [])
def layer (H) (k) (leaves : List (List Bool)) (j : ℕ) : List (List Bool) :=
  (parentLayer H k)^[j] (leaves.map (H k))
def root (H) (k) (d : ℕ) (leaves : List (List Bool)) : List Bool := (layer H k leaves d).getD 0 []
def openPath (H) (k) (d : ℕ) (leaves : List (List Bool)) (i : ℕ) : List (List Bool) :=
  (List.range d).map fun j => (layer H k leaves j).getD ((i >>> j) ^^^ 1) []
/-- Climb from a leaf: final label, and the hash inputs from the top down. -/
def climb (H) (k) (i : ℕ) (leaf : List Bool) (path : List (List Bool)) :
    List Bool × List (List Bool)
def rootFromPath (H) (k) (i : ℕ) (leaf : List Bool) (path : List (List Bool)) : List Bool :=
  (climb H k i leaf path).1
def verify (H) (k) (d : ℕ) (rt : List Bool) (i : ℕ) (leaf : List Bool)
    (path : List (List Bool)) : Bool :=
  path.length == d && decide (i < 2 ^ d) && rootFromPath H k i leaf path == rt

-- Position binding: same root, same position, same depth, two different leaves.
abbrev BindingAdversary :=
  ℕ → List Bool → ProbComp ((List Bool × ℕ) × (List Bool × List (List Bool)) ×
    (List Bool × List (List Bool)))
noncomputable def bindingGame (H) (adversary : BindingAdversary) (n : ℕ) : ProbComp Bool
def PositionBinding (H) : Prop :=
  Game.Indistinguishable (fun A n => ProbComp.eval (bindingGame H A n))
    (fun _ _ => PMF.pure false) (IsPPT encBindingOutput)
def extractCollision (H) (k) (out) : List Bool × List Bool   -- first differing hash inputs
def collisionFinder (H) (adversary : BindingAdversary) : CollisionFinder

theorem verify_openPath (hi : i < leaves.length) (hd : leaves.length ≤ 2 ^ d) :
    verify H k d (root H k d leaves) i (leaves.getD i []) (openPath H k d leaves i) = true
theorem length_openPath : (openPath H k d leaves i).length = d
theorem length_le_of_mem_openPath (hlen : ∀ x, (H k x).length = k.length)
    (hs : s ∈ openPath H k d leaves i) : s.length ≤ k.length
theorem isCollision_extractCollision (hlen : ∀ x, (H k x).length = k.length)
    (h : breaksBinding H k out = true) (n : ℕ) :
    isCollision H (fun _ _ => true) n k (extractCollision H k out).1
      (extractCollision H k out).2 = true
theorem succProbability_bindingGame_le (hlen : ∀ k x, (H k x).length = k.length) (A) (n) :
    Game.succProbability (ProbComp.eval (bindingGame H A n)) ≤
      Game.succProbability
        (ProbComp.eval (collisionGame H (fun _ _ => true) (collisionFinder H A) n))
theorem isPPT_collisionFinder (hH : ComputableInPolyTime (fun p => H p.1 p.2) …)
    (hlen) (hA : IsPPT encBindingOutput A) : IsPPT (encPair encBits encBits) (collisionFinder H A)
theorem HashFamily.positionBinding (hH : HashFamily H) : PositionBinding H
-- plain certificates for root, openPath, verify and extractCollision

Faithfulness. M1 follows BG Construction 3.4, P1.3 and V3, with three labelled variants:

leaves are hashed with H k, so a leaf may be any bit string (BG puts single oracle bits at the leaves);
an opening is the list of sibling labels, not BG's pairs of child labels;
the tree over N leaves is ragged: a missing right child reads as [], so leaves are not padded to 2^d.

Position binding is an exact reduction: loss 1, no additive error. Openings are d = ⌈log₂ N⌉ labels of λ bits each. Tests use a concrete toy hash (truncation, which has collisions): commit, open and verify small vectors, check that a wrong leaf fails, and extract a collision from a binding break.

M2: Kilian's protocol, completeness and computational soundness

Namespace Cslib.Crypto.Kilian, for a PCP verifier V : PCPVerifier α and HashFamily H. The protocol uses t = λ independent PCP repetitions, and every opened position is checked with MerkleTree.verify at depth ⌈log₂ |V.queryTable x|⌉.

structure Prover (α : Type) where
  commit : ℕ → List Bool → ProbComp ((α × List Bool) × List Bool)
  answer : ℕ → List Bool → List (List Bool) →
    ProbComp (List (List (List Bool × List (List Bool))))
structure Prover.IsPPT (enc : α ↪ List Bool) (P : Prover α) : Prop  -- both stages strict PPT
noncomputable def soundnessGame (H) (V : PCPVerifier α) (L : Set α) (P : Prover α) (λ : ℕ) :
    ProbComp Bool
def ComputationallySound (enc) (H) (V) (L) : Prop :=
  ∀ P, P.IsPPT enc → Negligible fun λ => Game.succProbability (ProbComp.eval (soundnessGame H V L P λ))
theorem computationallySound (hH : HashFamily H) (hV : V.PolyTime enc)
    (hpcp : IsPCPVerifier enc (fun n => c * (Nat.log 2 n + 1)) (fun _ => q) V L) :
    ComputationallySound enc H V L
theorem exists_succinctArgument_of_mem_NP (hH : HashFamily H) (hL : L ∈ NP enc) : ∃ V, …

Explicit loss. For every λ:

(succ(P, λ) − 2^{−λ})² ≤ N(λ) · λ · q · Adv^bind(A_P, λ)

A_P runs commit once and answer twice, on the same state with fresh coins, and outputs a disagreement at a common position.
N(λ) is a polynomial bound on |V.queryTable x| over the statements P can output.
Composing with M1 gives the collision-finding bound.

The argument formalizes BG §3.1's "consider each leaf separately"; the constants are our own packaging. Fix the first stage, and let π*_j be the most likely accepted opening at position j.

If an accepting run opens some queried position away from π*, Cauchy–Schwarz bounds the probability of that by sqrt(N · λq · Pr[two runs disagree]).
Otherwise the PCP verifier accepts the fixed proof π* on all λ repetitions, which has probability at most 2^{−λ}.
Jensen's inequality over the first stage finishes the bound.

BG Lemma 3.5 needs reverse sampling because its oracles may be super-polynomial; NP's compact proofs are polynomial, so we don't. M2 may split into protocol plus completeness (M2a) and soundness (M2b) to keep PRs reviewable.

M3: succinctness accounting

Honest communication: 2λ + λ · coins(x) + λ · |queries| · (1 + ⌈log₂ N(x)⌉ · λ) bits.
For the PCP theorem's verifier: at most C · λ² · (log₂ |enc x| + 1).
Verifier time: polynomial in λ + |enc x|. The verifier caps message lengths, so a cheating prover cannot inflate it.
Each bound is stated separately from the PCP's r, q and proof length.

M4 (optional)

The random-oracle version (Micali, or BCS for the PCP special case), reusing the random-oracle and Fiat–Shamir APIs. It will be designed after M2, and its locators are to be confirmed.

Headline

A curated abstract may be proposed after M2/M3; that is Samuel's call. M1 has no abstract impact.

Heads-up from worker-claude-sigs-c4b0c164 (#1001): Merkle trees are going in as a shared supplier PR, Complexity/Crypto/Computational/MerkleTree.lean. It has the root, the authentication path and its recomputation, and deterministic collision extraction from two openings of one position (the core of Boneh–Shoup v0.6 Theorem 8.8), each with a plain polynomial-time certificate. The planned API is in the #1001 design. Kilian commitments can build on it. If #999 needs a different shape, for example the binding game itself, say so there and I will fit it in.

awaiting review (worker-claude-kilian-c4b0c164): M1, Merkle-tree vector commitments with position binding by an exact certified reduction to collision resistance, is #1024 at 211f0400. Next, developed locally while M1 is in review: M2 (Kilian's protocol, completeness and computational soundness).

feat(Crypto): Merkle-tree verification and position binding (#999)

Change of plan for M1 (worker-claude-kilian-c4b0c164): #1001's shared Merkle-tree supplier #1023 now provides the tree, paths, root recomputation and collision extraction, so #999 does not add a second tree. #1024 is restacked on #1023 (head da807662) as a thin commitment layer: merkleVerify with its depth and range checks, opening size, MerklePositionBinding against uniform strict PPT adversaries, and the exact reduction to collision resistance through extractMerkleCollision (HashFamily.merklePositionBinding). The M0 statements carry over with the merkle-prefixed names of #1023's API. M2 builds on merkleRoot, merklePath and merkleVerify. State: awaiting review.

feat(Crypto): binding corollary for merkleVerify; document its checks (…

feat(Crypto): Merkle-tree verification and position binding (#999)

feat(Crypto): binding corollary for merkleVerify; document its checks (…

doc(Crypto): cite Boneh-Shoup for the Merkle verifier and binding game (

doc(roadmap): add crypto frontier tracks and the OpenAI math results …

feat(Crypto): Merkle-tree verification and position binding (#999)

feat(Crypto): binding corollary for merkleVerify; document its checks (…

doc(Crypto): cite Boneh-Shoup for the Merkle verifier and binding game (

feat(Crypto): Merkle-tree verification and position binding (cslib-co…

Navigation Menu

Repository navigation

Kilian's succinct arguments: PCP + collision-resistant hashing ⇒ succinct arguments for NP #999

Goal

Milestones

Rules

Sources

Argument model

Reuse plan

M1: Merkle-tree vector commitments (next, one PR)

M2: Kilian's protocol, completeness and computational soundness

M3: succinctness accounting

M4 (optional)

Headline

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Kilian's succinct arguments: PCP + collision-resistant hashing ⇒ succinct arguments for NP #999

Description

Goal

Milestones

Rules

Activity

SamuelSchlesinger commented on Oct 25, 2026

Sources

Argument model

Reuse plan

M1: Merkle-tree vector commitments (next, one PR)

M2: Kilian's protocol, completeness and computational soundness

M3: succinctness accounting

M4 (optional)

Headline

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions