Restricted versus general auxiliary-input zero knowledge (#680 item 1) #698

Parent tracker: #680 (Item 1), under #593 and #643.

Scope & Acceptance Criteria

1. Explicit public API identities for restricted vs. general auxiliary-input zero knowledge in Complexity/Crypto/Computational/ZeroKnowledge.lean:
   • GenerableZeroKnowledge enc prover isWitness: uniform computational zero-knowledge against uniform strict oracle PPT malicious verifiers Vstar quantified over deterministic polynomial-time-generable instance, valid-witness, and auxiliary-input families (ComputableInPolyTime · encUnary _), with one efficient witness-free simulator S chosen per Vstar before the choice of (a, w, z).
   • AuxiliaryInputZeroKnowledge enc prover isWitness (and ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge): general auxiliary-input computational zero-knowledge for arbitrary polynomially bounded valid families a : ℕ → α, w z : ℕ → List Bool (PolynomiallyBounded (fun n => (enc (a n)).length), PolynomiallyBounded (fun n => (w n).length), PolynomiallyBounded (fun n => (z n).length), and ∀ n, isWitness (a n) (w n) = true), against full-input uniform strict PPT distinguishers adversary : ℕ → α → List Bool → List Bool → ProbComp Bool charged for the complete encoded input ((1^n, (a n, z n)), view), with one efficient witness-free simulator S per Vstar chosen before the families and distinguisher.
2. Stronger-to-restricted bridge:
   • Prove AuxiliaryInputZeroKnowledge.generableZeroKnowledge (and ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.generableZeroKnowledge): general auxiliary-input zero knowledge implies restricted poly-time-generable zero knowledge (GenerableZeroKnowledge), using the fact that deterministic polynomial-time-generable families have polynomially bounded encoded lengths and any unary-indexed ComputationallyIndistinguishable distinguisher lifts to a full-input distinguisher.
3. Advice-PRG consequence for GMW:
   • Package the explicit advice-PRG premise of GMW.gmwView_negligible_of_advice_prg as a named predicate (GMW.AdvicePRG) and prove that PseudorandomGenerator.zeroKnowledgeProofOfReduction and PseudorandomGenerator.zeroKnowledgeProofThreeSAT satisfy ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge under GMW.AdvicePRG, without inferring that stronger premise from uniform OWF/PRG security.
4. Tests & Documentation:
   • Preserve all existing ZeroKnowledgeProof fields and theorems; update docstrings and ROADMAP.md to clearly distinguish GenerableZeroKnowledge from AuxiliaryInputZeroKnowledge; add nonvacuous checks and #print axioms guards in ComplexityTests/Crypto/ZeroKnowledge.lean.