GMW zero knowledge in full: nonuniform OWF ⇒ auxiliary-input ZK for NP with negligible soundness (ROADMAP landmark)

Tracking issue for the first ROADMAP landmark, Goldreich–Micali–Wigderson zero knowledge in full, opened by coordinator-jetski-fc77e3ec (Jetski, crypto area) from a gap analysis of main @ b69b946bb.

Target (ROADMAP). If nonuniformly one-way functions exist, every language in NP has a computational zero-knowledge proof in Goldreich's sense (Foundations of Cryptography Vol. 1, Def. 4.3.10): for every x ∈ L and arbitrary auxiliary input z, against probabilistic polynomial-time verifiers, with negligible soundness error. Locators for the composition lemma and the final theorem (Goldreich Vol. 1 §4.3–4.4, believed to be Lemma 4.3.11 and Thm 4.4.11) must be checked against the text in M0 before they are cited.

What `main` has

OneWay.exists_zeroKnowledgeProof_of_mem_NP (Crypto/Computational/ZeroKnowledge.lean): uniform OWF ⇒ GenerableZeroKnowledge for every A ∈ NP, by a Karp reduction to 3SAT and a masked-3SAT truth-table protocol with inlined Naor PRG commitments. The prover's witness is a 3SAT witness for the reduced instance, not a witness of A's own verifier.
PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP: general AuxiliaryInputZeroKnowledge, but only under GMW.AdvicePRG, which nothing derives.
Both ZK notions use a separate security parameter with polynomially bounded z (the verifier's clock is charged on all of z). Distinguishers are uniform. Soundness is a constant 1/3, hard-wired in ZeroKnowledgeProof. The simulator is strict PPT.
sequentialRepeat with ε^k soundness exists in Classes/IP/Repetition.lean, with efficiency only for constant k. There is no ZK composition theorem.
HILL (OWF ⇒ PRG) is fully uniform. There is no nonuniform OWF/PRG notion, and no Levin (witness-preserving) reduction to an NP-complete relation.

Milestones

Each one is an independently reviewable PR or PR series.

M1 (S): advice notions. NonuniformOneWay, NonuniformPRG (security against uniform PPT adversaries given every polynomially bounded advice family), .toOneWay/.toPRG, and NonuniformPRG → GMW.AdvicePRG. Also an audit of whether the HILL chain's reductions are generic over the adversary's input type, so that advice carries through by instantiation, or whether M2 needs a refactor.
M2 (XL, split after the M1 audit): nonuniform HILL. NonuniformOneWay.exists_nonuniformPRG_three_mul, by relativizing the uniform proof to a passive advice input (Goldreich–Levin, pseudoentropy pair, generator, stretch). Simply assuming a nonuniform PRG is ruled out by the ROADMAP.
M3 (M): clock bridge. A prefix-locality lemma for (oracle) probabilistic machines (a T-step run on u ++ v depends only on u ++ take T v), and the derivation of a Goldreich-style, x-indexed definition with unbounded z from the family form.
M4 (L): Levin reductions. A LevinReduction structure (instance map, poly-time forward witness map, relation preservation, trans), a computable poly-time Cook–Levin witness map, the to3CNF witness extension, and ThreeSAT_levinHard. These are reusable beyond ZK.
M5 (S/M): ZK from a Levin reduction. The prover takes A's own NP witness, and AuxiliaryInputZeroKnowledge carries through.
M6 (L): amplification and composition. Polynomial-count sequential repetition with an efficiency certificate, a sequential-composition theorem for auxiliary-input ZK, and a proof-system predicate with a negligible soundness function.
M7 (S): assembly. NonuniformOneWay.exists_goldreichZK_of_mem_NP, plus ROADMAP/README updates and an abstract assessment.

Design decisions (proposed defaults; objections welcome)

Distinguishers in the final definition get their own advice family (Goldreich's indistinguishability is nonuniform). GMW's black-box simulator should make this cost only the M1 premise.
Prove the family form first and derive the x-indexed form in M3.
Keep masked 3SAT as the base relation (the ROADMAP does not require 3-colouring), so M4 targets 3SAT.
Add a new proof-system predicate with a soundness function for the endpoint, and do not churn ZeroKnowledgeProof unless review prefers the refactor.

M1, M3 and M4 are independent and can start in parallel. M2 waits for the M1 audit.

Claiming M4 (Levin reductions). Role: worker, worker-jetski-2927d222 (Jetski), assigned by coordinator-jetski-fc77e3ec. Branch feat/levin-reduction-2316 (further PRs on feat/levin-*-2316 branches).

Scope, split into reviewable PRs:

NPRelation (polynomial certificate length + polynomial-time verifier, with language, IsVerifier and NP bridges) and LevinReduction between NP relations: polynomial-time instance map, polynomial-time forward and backward witness maps (Goldreich-style), with refl, trans and toPolyTimeReducible; plus the SAT → 3SAT Levin reduction (explicit to3CNF witness extension and restriction, both certified polynomial-time). Nonvacuity tests in ComplexityTests/.
A polynomial-time Cook–Levin witness map (run simulation → tableau assignment → SAT certificate) and its backward map (certificate bits), giving SAT_levinHard and ThreeSAT_levinHard: every NP relation Levin-reduces to 3SAT's verifier relation.

Done when both are review-ready with no new axioms or heartbeat overrides. M5 is not in scope. If item 2 turns out larger than expected, I'll record it here as its own milestone.

Claiming M1 as worker worker-jetski-3ceb65c9 (Jetski/Gemini; coordinator coordinator-jetski-fc77e3ec), branch feat/nonuniform-owf-prg-2316.

Scope: (a) one PR adding NonuniformOneWay and NonuniformPRG (uniform strict PPT adversaries that also receive an arbitrary polynomially bounded advice word family), .toOneWay / .toPRG, NonuniformPRG.advicePRG : … → GMW.AdvicePRG enc … with the corollary discharging the premise of PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP, checked tests, and the [#2316] link on ROADMAP landmark 1; (b) an audit comment here on whether the uniform HILL chain relativizes to advice by instantiation, with a proposed M2 split.

Done when: the PR is open with CI green and the audit is posted. M1 does not derive any nonuniform primitive from a uniform one; the landmark stays open.

M1 audit: can the uniform HILL chain be relativized to advice by instantiation? (worker-jetski-3ceb65c9, worker. Source: main @ 13ea15dc0.)

Short answer: not by instantiation alone, but most of the proof can be reused unchanged. The transitive import closure of OneWayToPRG inside Crypto/Computational has 56 modules and about 14.9k lines. They fall into three layers:

Quantitative core: reusable as is (about 5.5k lines). These modules have no IsPPT in any statement. Their bounds hold for arbitrary predictor or adversary functions: GoldreichLevin/{Decoding,Parameters,Reduction,WordDecoder}, Pseudoentropy/{HashReduction,Reduction,EntropyGrid,ExtractionSchedule,Learning,MaskedExtraction,SeedExtraction,ThreeSource/Seeded}, Boosting/{Loop,Potential,Progress} and Stretch/Quantitative (881). A fixed advice family z can be curried into such a function, as in fun n w => A ((n, z n), w), and these lemmas then apply verbatim.
Program constructions: already generic (about 5k lines). Their efficiency lemmas are stated over an arbitrary context input : α ↪ List Bool (IsPPTOn input …). Examples: Stretch.isPPT_test, GeneratorXor/GeneratorPadding.isPPTOn_test, Prediction.*, Masking.isPPTOn_maskedSample, SequenceLearner.exists_evaluator ({Param} {input}), WordExtraction.isPPTOn_extractedWordTest, Boosting/Program.isPPTOn_run, Hybrid/Sequence (mostly), and the general IsPPTOn.exists_total_seeded_evaluator. Advice enters by instantiating α := (ℕ × List Bool) × ….
Security interfaces: hard-wired (about 3–3.5k lines). This layer needs the work. The adversary's context is fixed to n (Distinguisher, Inverter, IsPPT encBool) or to (n, i) (encPair (encPair encUnary encUnary) …, where i is a chosen candidate index). Clock and coin budgets are computed from the encoded length of that fixed context. Examples: coinBudget c d n imageLength and fixedPredictor_distribution's hrealize over (encPair encUnary encBits (n, input)).length. Affected declarations:
- Inversion side (M2a): Pseudoentropy.WordReduction.{wordInverter,isPPT_wordInverter,fixedPredictor_distribution} (309), Pseudoentropy.OneWay.{eventually_prediction_entropy_le,pair_hasGap}, OneWay.exists_pseudoentropyPair (125), and OneWay/Normalize.{OneWay.normalize,exists_fixedOutputLength} (120). The definition Pseudoentropy.SamplablePair.HasGap (Basic, 158) quantifies over Distinguisher.
- Pair → generator (M2b): DenseMask.HasGap.eventually_exists_{indexed_,}mask (265), LabelExtraction (233), WordExtraction indexed theorems (225), WordSeedExtraction/RepeatedExtraction (fixed parts), ThreeSource.{replace_*,HasGap.extract_indexed_three,extract_three} (556), ThreeSource/{Candidates,Padding,Amplification,Combined} (about 675), Pseudoentropy/Generator (79) and GeneratorReindex.pseudorandomGenerator (230). The fixed Hybrid/SavedPrediction pieces (436) can mostly stay as they are.
- Stretch (M2c): Stretch.{isPPT_reduction,indexed_indistinguishable,indistinguishable,pseudorandomGenerator,PseudorandomGenerator.amplify,truncate} (465).
- HardCore.lean and GoldreichLevin/HardCore.lean (the one-way-permutation route) are not on the HILL path, so M2 does not need them.

The (n, i) pattern is the important finding. The uniform proof already supports one form of nonuniformity: the candidate index choose : ℕ → ℕ is passed to one indexed test through a unary context. Stretch.indexed_indistinguishable and ThreeSource.replace_indexed_labels show this. Generalizing that unary index to an arbitrary encoded context ctx : ℕ → κ, polynomially bounded, mostly changes signatures rather than mathematics: encUnary becomes encCtx, and budgets are computed from the generalized encoded length. M1's NonuniformlyIndistinguishable.negligible_encoded / NonuniformOneWay.inversion_negligible_encoded (via IsPPTOn.exists_extension, #2320) already turn such a context back into the advice-word definitions.

Recommendation: relativize in place, without duplicating. Restate each layer-3 theorem relative to a fixed context family. The uniform theorems then come back as the trivial-context instance (κ := Unit, or empty advice; NonuniformOneWay.toOneWay and friends already show that empty advice is uniform). Duplicating the theorems as advice variants would add roughly 3k parallel lines. If review prefers to leave the uniform statements unchanged, the fallback is advice variants that call the generalized lemmas.

Proposed M2 split

M2c (stretch). Independent; can start now, since it needs only NonuniformPRG. Generalize Stretch.indexed_indistinguishable from the (n, i) context to an encoded context. Then prove NonuniformPRG.amplify / NonuniformPRG.truncate (one-bit nonuniform PRG ⇒ any polynomial stretch, including 3n+1). About 465 lines touched plus 100–150 new. One PR.
M2a (OWF ⇒ pseudoentropy pair, with advice). First PR, scoped precisely:
- NonuniformOneWay.normalize / NonuniformOneWay.exists_fixedOutputLength, mirroring OneWay/Normalize.
- An advice-context version of Pseudoentropy.WordReduction.isPPT_wordInverter / fixedPredictor_distribution. Here evaluate takes the advice word and the budget is computed from the encoded advice-carrying context.
- Validation: the uniform isPPT_wordInverter is recovered at empty advice. Size about 300–400 lines.
Second PR: a context-relative SamplablePair.HasGap (or HasNonuniformGap) and NonuniformOneWay.exists_pseudoentropyPair.
M2b (pair ⇒ one-bit nonuniform PRG). Three PRs:
1. DenseMask + LabelExtraction, with the context generalized from (n, i) to (n, i, ctx n).
2. WordExtraction / WordSeedExtraction / ThreeSource.
3. ThreeSource/{Candidates,Padding,Amplification,Combined}, Pseudoentropy/Generator and GeneratorReindex, ending in HasNonuniformGap.exists_nonuniformPRG.
Assembly (M2 endpoint): NonuniformOneWay.exists_nonuniformPRG_three_mul from M2a + M2b + M2c.

Line counts are module sizes from wc -l. The layer split was found by grepping statements for IsPPT, Distinguisher, Inverter and fixed encodings, plus reading the boundary theorems named above. It was not a line-by-line read of all 56 modules, so expect a few surprises in the M2b RepeatedExtraction and SavedPrediction internals.

worker-jetski-3ceb65c9 (worker): per coordinator decision, M2 relativizes in place. Starting M2c (stretch) on feat/nonuniform-stretch-2316, stacked on #2320.

Scope:

add a fixed-advice relative notion IndistinguishableWithAdvice advice X Y; uniform indistinguishability is its empty-advice case, and NonuniformlyIndistinguishable quantifies it over bounded advice;
generalize PRGStretch.indexed_indistinguishable from the unary (n, i) context to an arbitrary encoded context;
derive the relative stretch theorem; recover the uniform PRGStretch.indistinguishable at empty advice;
add PRGStretch.nonuniformPRG, NonuniformPRG.amplify and NonuniformPRG.truncate.

All clients are updated in the same PR, with no wrappers. I will merge main after #2010 lands, before requesting review. Next: the first M2a PR.

Claiming Milestone M3 (Clock Bridge: prefix-locality lemmas, IsPPTWithAux / IsOraclePPTWithAux, and unbounded-auxiliary-input / instance-indexed zero-knowledge bridges from AuxiliaryInputZeroKnowledge) — jetski-worker-252a2093 (252a2093-1f93-43aa-85bf-432251102a3b), branch feat/zk-clock-bridge-2316, PR #2339.

worker-jetski-2927d222 (M4): awaiting review.

feat(Complexity): Levin reductions between NP relations, with SAT to 3SAT #2322 adds NPRelation, LevinReduction (polynomial-time instance map plus forward and backward witness maps) and LevinHard, together with the explicit to3CNF witness extension and the SAT → 3SAT Levin reduction. Review fixes are pushed.
feat(Complexity): Cook-Levin as a Levin reduction, every NP relation Levin-reduces to 3SAT #2329 is stacked on feat(Complexity): Levin reductions between NP relations, with SAT to 3SAT #2322. It adds a polynomial-time tracked simulation of a fixed machine, the Cook–Levin forward and backward witness maps with plain polynomial-time certificates, CookLevin.SAT_levinHard and CookLevin.ThreeSAT_levinHard.

Together they cover the M4 scope (a)–(d). M4 is not done until both land and are reviewed. M5 is not in scope.

Claiming M5 (ZK from a Levin reduction). Role: worker, worker-jetski-2927d222. Branch feat/zk-levin-2316, stacked on #2329.

Scope:

A GMW zero-knowledge proof system for the language of any NPRelation. The bundled witness check is the relation's own (decide (R.IsWitness a w)). The honest prover sends a's own witness through the forward map of ThreeSAT_levinHard (more generally, of any Levin reduction to 3SAT) into a 3SAT witness for the reduced formula. Verifier, simulator and soundness are those of the Karp version.
Transport both properties: GenerableZeroKnowledge (the mapped witness family stays polynomial-time generable) and, under GMW.AdvicePRG, AuxiliaryInputZeroKnowledge (the mapped family stays polynomially bounded).
Endpoint theorems for PRGs and OWFs: every NPRelation has a ZK proof complete for its own witnesses.
The non-blocking review nits from feat(Complexity): Cook-Levin as a Levin reduction, every NP relation Levin-reduces to 3SAT #2329.

Done when the PR is review-ready (all six gates pass) with no tidy code. M6/M7 are not in scope.

feat(Crypto): nonuniform one-way functions and PRGs with the GMW advi…

Claiming M6 (amplification and composition). Role: worker, worker-jetski-2927d222. Branches feat/zk-amplify-2316-*, stacked on #2337 where needed. @252a2093 owns M3: the composition below is stated in the family form (Cslib.Crypto.AuxiliaryInputZeroKnowledge), and M3 derives the x-indexed form from it.

Size: XL overall. I propose four PRs:

M6a (S/M): polynomial repetition and a soundness function.

IsOraclePPTOn.sequentialRepeat_count: for k : α → ℕ computable in unary polynomial time, fun a => sequentialRepeat (k a) (round a) is strict oracle PPT. It goes through the plain IsOraclePPTOn.iterate_spec'/iterateWith rules, with a Bool state (sequentialRepeat k r = OracleComp.iterate k (fun ok => if ok then r else pure false) true); no tidy code.
A new structure Cslib.Crypto.ZKProof enc A (soundness : ℕ → ℝ≥0∞), with the fields of ZeroKnowledgeProof except that sound reads acceptProb (verifier n a) P ≤ soundness n. A coercion ZeroKnowledgeProof.toZKProof : ZKProof enc A (fun _ => 1/3) keeps every existing client unchanged.
- Choice recorded here: ZeroKnowledgeProof is not changed now. Restating it as ZKProof … (fun _ => 1/3) is a possible later migration, if review prefers.
- NegligibleSoundness zk := Negligible soundness, and negligible_one_third_pow (hk : ∀ n, n ≤ k n).

M6b (L): sequential composition machinery.

Prover.sequential (P : ℕ → Prover Unit): session-tagged messages encode i ++ m. It keeps the state of the current session only, starts session i fresh when the first message tagged i arrives after earlier sessions, and answers [] to messages for finished sessions. This enforces sequential, not concurrent, composition.
sequentialVerifier k V: run V i for sessions i < k, tagging the queries, and accept when all accept. Soundness ε^k comes from acceptProb_sequentialRepeat_le (generalized to session-indexed rounds), and completeness from le_acceptProb_sequentialRepeat.
Residual verifiers: for a malicious V* of the composed protocol and a recorded history (V*'s coins and the replies so far, as bits), residual V* i runs V* from that history through session i's messages and outputs its state. Certificate: if V* is strict oracle PPT, so is the residual, polynomially in the history. This reuses the saved-coin replay in Probabilistic/Replay. It is the largest piece.

M6c (L): the composition theorem.

Averaging: if a strict PPT distinguisher has non-negligible advantage on views whose auxiliary input is drawn from a polynomially bounded distribution family, then some fixed polynomially bounded auxiliary-input family does no better on average. This is the "random aux ⇒ worst fixed aux family" step, and it matches the quantifiers of AuxiliaryInputZeroKnowledge, where z ranges over arbitrary polynomially bounded families.
AuxiliaryInputZeroKnowledge.sequential: if (prover, isWitness) is auxiliary-input ZK, then Prover.sequential (fun _ => prover n a w) with k(n) ≤ poly(n) sessions is auxiliary-input ZK for the composed verifiers. The simulator runs the single-session simulator on each residual verifier in turn. The proof is a hybrid over k(n) sessions using Hybrid/Sequence.lean: hybrid i has its first i sessions simulated, and the witness travels in the auxiliary input of the hybrid distinguisher. This is Goldreich, Foundations of Cryptography Vol. 1, §4.3.4 (sequential composition, believed Lemma 4.3.11). I'll check the locator before citing it.

M6d (S): assembly for GMW.

levinZeroKnowledgeProof.sequential (k := n + 1) gives a ZKProof with soundness (1/3)^(n+1) (negligible) and auxiliary-input ZK under GMW.AdvicePRG. Composed with M5, this covers every NP relation. M7 then replaces AdvicePRG by the nonuniform OWF.

Done when each PR is review-ready with no tidy code, and M6d proves a ZK proof with negligible soundness for every NP relation (still conditional on GMW.AdvicePRG until M7). I'm starting M6a now. Objections to the ZKProof choice or the session-tagged prover are welcome before M6b.

feat(Crypto): relativize PRG stretch to fixed advice and amplify nonu…

fix(Probabilistic): state runOracle_of_clock on plain IsOraclePPTOn (#…

Milestone M3 (Clock Bridge) is complete and merged in #2339 (ddc0599ea4dde678f31b86e54df1a0c25af29474) — jetski-worker-252a2093.

Progress update (jetski-worker-252a2093):

Milestone M2b-3 + M2 endpoint (nonuniform amplification, XOR generator, NonuniformOneWay.exists_nonuniformPRG, NonuniformOneWay.exists_nonuniformPRG_three_mul, and single-round auxiliary-input ZK from NonuniformOneWay) merged in feat(Crypto): construct nonuniform PRGs and auxiliary-input ZK from nonuniform OWFs #2354 (5785f94a4).
Next up: Milestones M6b–M6d + M7 (sequential soundness amplification to negligible soundness (1/3)^(n+1) preserving AuxiliaryInputZeroKnowledge / UnboundedAuxiliaryInputZeroKnowledge / InstanceAuxiliaryInputZeroKnowledge, final landmark assembly, ROADMAP/README/manual updates, and formal abstract) on branch feat/zk-soundness-amplification-2316.

feat(Crypto): prefix-locality clock bridge for auxiliary-input zero k…

feat(Crypto): relativize one-wayness to fixed advice and normalize no…

feat(Crypto): relativize the pseudoentropy gap to fixed advice (cslib…

feat(Crypto): polynomial-count sequential repetition and ZKProof with…

Opened #2362 completing M6b–M6d and M7 (sequential soundness amplification for the 3-copy GMW protocol, multi-round rewinding simulator via open oracle machine execution, removal of the syntactic verifier-congruence clause from AuxiliaryInputZeroKnowledge, and the full nonuniform-OWF landmark theorems NonuniformOneWay.exists_zkProof_of_mem_NP and NonuniformOneWay.exists_zkProof_of_npRelation). Ready for independent review.

feat(crypto): GMW sequential soundness amplification and full landmark (

Merge refreshed feat/rompel-signatures-1001-m4c into feat/rompel-word…

Navigation Menu

Repository navigation

GMW zero knowledge in full: nonuniform OWF ⇒ auxiliary-input ZK for NP with negligible soundness (ROADMAP landmark) #2316

What `main` has

Milestones

Design decisions (proposed defaults; objections welcome)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

GMW zero knowledge in full: nonuniform OWF ⇒ auxiliary-input ZK for NP with negligible soundness (ROADMAP landmark) #2316

Description

What main has

Milestones

Design decisions (proposed defaults; objections welcome)

Activity

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 2, 2026

SamuelSchlesinger commented on Nov 3, 2026

SamuelSchlesinger commented on Nov 3, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

What `main` has