feat: The Kilian transformation

[BoltonBailey]

Introduces the Kilian '92 transformation to derive a SNARG from a PCP.

Co-Authored-By: Claude Opus 4.8 noreply@anthropic.com

[github-actions]

🤖 PR Summary

Kilian Transformation

Formalization of the Kilian '92 transformation (PCPs to SNARGs), including a formal definition of PCPs and a proof of perfect completeness.

Cryptographic Abstractions

• ChallengeVerifyProtocol structure: a monad-based framework for commit–challenge–response protocols capturing special soundness, HVZK, and unique responses.
• Modular interface for Vector Commitments (VC) and Batch-Opening VCs, with a concrete Merkle tree implementation and proofs of correctness.

Library Extensions

• List.map_lookup and related association list lemmas in ToMathlib to support Merkle tree reasoning.
• All properties are fully proven; no sorry or admit placeholders are present.

---

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	1042
❌ Lines Removed	0

---

Lean Declarations

✏️ **Added:** 41 declaration(s)

• theorem perfectCorrectness_accepts_liftedProver in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def toBatchOpening [DecidableEq ι] [DecidableEq α] in VCVio/CryptoFoundations/VectorCommitment/Basic.lean
• theorem extract_sound_of_speciallySoundAt in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• def pathLog (so : QueryImpl spec Id) {α : Type u} (comp : OracleComp spec α) : List ι in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def PositionBinding (bovc : BatchOpeningVectorCommitment m ι α Commit State BatchOpening) : Prop in VCVio/CryptoFoundations/VectorCommitment/Basic.lean
• def leafDataOfFn : (s : Skeleton) → (SkeletonLeafIndex s → α) → LeafData α s in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• def naiveBatchOpenMerkleTree {ι : Type} {m : Type → Type} [Monad m] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem vectorCommitment_decode {ι : Type} {m : Type → Type} [Monad m] [DecidableEq α] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem neverFail_of_perfectCorrectness in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem vectorCommitment_commit {ι : Type} {m : Type → Type} [Monad m] [DecidableEq α] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem toLeafData_buildMerkleTreeWithHash {s : Skeleton} in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• noncomputable def soundness (pcp : PCP Stmt Wit) (rel : Stmt → Wit → Bool) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def PerfectHVZK (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• noncomputable def correctness (pcp : PCP Stmt Wit) (rel : Stmt → Wit → Bool) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem KilianTransformation_perfectlyComplete in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• noncomputable def perfectSoundness (pcp : PCP Stmt Wit) (rel : Stmt → Wit → Bool) : Prop in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem vectorCommitment_openAt {ι : Type} {m : Type → Type} [Monad m] [DecidableEq α] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem map_lookup (f : ι → Sym) (t : ι) : in ToMathlib/Data/List/Lookup.lean
• theorem claimAnswer_run (f : ι → Sym) (claims : List (ι × Sym)) {β : Type u} in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def runVerifier (pcp : PCP Stmt Wit) (stmt : Stmt) (coins : pcp.Coins) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem vector_mk_toList {n : ℕ} (v : List.Vector α n) (h : v.toList.length = n) : in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem KilianTransformation_verify_eq_true in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem mapM_pure_map {m : Type → Type} [Monad m] [LawfulMonad m] {β γ : Type} (g : β → γ) : in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem claimAnswer_map (f : ι → Sym) (L : List ι) (t : ι) (ht : t ∈ L) : in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• noncomputable def perfectCorrectness (pcp : PCP Stmt Wit) (rel : Stmt → Wit → Bool) : Prop in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def realTranscript (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• def vectorCommitment {ι : Type} {m : Type → Type} [Monad m] [DecidableEq α] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• theorem naiveBatchOpenMerkleTree_perfectlyCorrect {ι : Type} {m : Type → Type} in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• def claimAnswer [BEq ι] (claims : List (ι × Sym)) : QueryImpl (ι →ₒ Sym) (OptionT Id) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• noncomputable def KilianTransformation in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def PerfectlyCorrect in VCVio/CryptoFoundations/VectorCommitment/Basic.lean
• def HVZK (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• def PerfectlyComplete (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) : in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• theorem vectorCommitment_perfectlyCorrect {ι : Type} {m : Type → Type} [Monad m] in VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean
• def UniqueResponses (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• def toVectorCommitment (bovc : BatchOpeningVectorCommitment m ι α Commit State BatchOpening) : in VCVio/CryptoFoundations/VectorCommitment/Basic.lean
• lemma perfectHVZK_iff_hvzk_zero in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• def SpeciallySound (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean
• theorem pathLog_query (so : QueryImpl spec Id) {α : Type u} (t : spec.Domain) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• theorem runVerifier_eq_evalWithAnswerFn in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean
• def SpeciallySoundAt (σ : ChallengeVerifyProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and Header Violations

• Copyright Year: All new files (ToMathlib/Data/List/Lookup.lean, VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean, VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean, VCVio/CryptoFoundations/VectorCommitment/Basic.lean, and VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean) use the year 2026 in the copyright header. This should be updated to reflect the current calendar year.
• Naming Conventions: In VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean, the PCP structure fields Prover and Verifier use UpperCamelCase. These should be lowerCamelCase (prover and verifier) as they represent functions/terms.
• Prologue Layout: In VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean, the module docstring contains multiple leading blank lines (lines 14-15) before the title. Per the prologue layout instructions, ensure exactly one blank line separates the import block from the docstring content.
• Section Headers:
  • In VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean, line 83 uses ###. The style guide specifically requests ## for section titles.
  • In VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean, line 140 uses a /-! ... -/ block as a section break/note but lacks the required ## title prefix.
  • In VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean, section blocks (e.g., section complete, section hvzk) are used without corresponding /-! ## docstring headers, which are preferred for documentation visibility.

---

📄 **Per-File Summaries**

• ToMathlib.lean: The change adds an import for ToMathlib.Data.List.Lookup to the central ToMathlib.lean module, incorporating new list-related theorems and definitions into the project's Mathlib-bound extensions. No sorry or admit placeholders were introduced.
• ToMathlib/Data/List/Lookup.lean: This file introduces the theorem List.map_lookup, which establishes that looking up a key in an association list formed by mapping a function over a list of keys returns the function's value for that key. The theorem is fully proved without any sorry placeholders.
• VCVio.lean: The changes update the library's main entry point to include new modules for Challenge-Verify protocols, such as Kilian's construction, and Vector Commitment schemes, including Merkle Trees.
• VCVio/CryptoFoundations/ChallengeVerifyProtocol/Basic.lean: This file introduces the ChallengeVerifyProtocol structure, a monad-generic abstraction for commit–challenge–response protocols that supports oracle-based computations. It defines core security properties—completeness, special soundness, honest-verifier zero-knowledge, and unique responses—along with foundational theorems relating them, and contains no sorry placeholders.
• VCVio/CryptoFoundations/ChallengeVerifyProtocol/Kilian.lean: This file formalizes the Kilian transformation, defining a structure for Probabilistically Checkable Proofs (PCPs) and their conversion into succinct interactive arguments using batch-opening vector commitments. It introduces new definitions and theorems, including a formal proof of the transformation's perfect completeness, and contains no sorry placeholders.
• VCVio/CryptoFoundations/VectorCommitment/Basic.lean: This new file introduces the VectorCommitment and BatchOpeningVectorCommitment structures, providing a monadic abstraction for cryptographic vector commitments. It defines essential security properties, including perfect correctness and position binding, and provides functions to interconvert between single-position and batch-opening interfaces.
• VCVio/CryptoFoundations/VectorCommitment/MerkleTree.lean: This file implements inductive Merkle trees as both single and batch-opening vector commitments by realizing the abstract VectorCommitment interfaces. It introduces the vectorCommitment and naiveBatchOpenMerkleTree definitions along with their respective proofs of perfect correctness.

---

Last updated: 2026-06-29 00:27 UTC.

[alexanderlhicks]

FYI: https://github.com/z-tech/z-lean/tree/main/Kilian

cc @z-tech