feat: generalize monad in SigmaProtocol

[BoltonBailey]

This PR generalizes the monad in SigmaProtocol from ProbComp to any monad m, and adds a field for a monadic challenge sampling procedure. Call sites get HasEvalSPMF m, or are specified to use the ProbComp monad where that's necessary.

This is part of an attempt to generalize SigmaProtocol enough to express the Kilian transformation as returning a SigmaProtocol. This might also require separating out the extractor so I can define non-special soundness, and making the verifier possibly non-deterministic.

I am still not quite sure if this is a good change - I want to understand better to what degree these generalizations can be pushed through downstream without compromising proofs (although perhaps it is a good change even if it can't be pushed through for the existing code, because future code might be able to take advantage of the generalization).

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Generalize SigmaProtocol to use a polymorphic monad m instead of the fixed ProbComp monad.
• Introduce a sampleChal field to the SigmaProtocol structure to abstract challenge generation.
• Update core theorems, including completeness and honest-verifier zero-knowledge (HVZK), to operate over the generalized monadic framework.
• Add hypotheses to security proofs requiring that challenge sampling follows a uniform distribution.

Refactoring

• Update Fiat-Shamir and Fischlin transformation implementations to support the new monadic parameters.
• Adapt the Schnorr protocol implementation to the generalized interface by specifying ProbComp as the underlying monad.
• Adjust security reductions and game definitions to incorporate HasEvalSPMF m constraints where necessary.
• Standardize challenge generation across protocols using the newly added sampleChal field.

---

Statistics

Metric	Count
📝 Files Changed	17
✅ Lines Added	156
❌ Lines Removed	125

---

Lean Declarations

✏️ **Affected:** 10 declaration(s) (line number changed)

• def SpeciallySound (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L88 to L99
• theorem almostComplete (hρ : 0 < ρ) (hc : σ.PerfectlyComplete) in VCVio/CryptoFoundations/Fischlin/Completeness.lean moved from L1491 to L1494
• def PerfectlyComplete (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L67 to L78
• def SpeciallySoundAt (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L81 to L92
• private lemma model_reject_le (_hρ : 0 < ρ) (hc : σ.PerfectlyComplete) in VCVio/CryptoFoundations/Fischlin/Completeness.lean moved from L1402 to L1404
• def PerfectHVZK (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L133 to L144
• def HVZK (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L126 to L137
• def toIdenSchemeWithAbort (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel ProbComp) : in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L227 to L240
• def UniqueResponses (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L216 to L229
• def realTranscript (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L109 to L120

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The pull request performs a significant refactoring of the SigmaProtocol framework to generalize it over an arbitrary monad m, rather than being hardcoded to ProbComp. This allows Σ-protocols to be used in contexts involving additional oracles or non-uniform randomness.\n\n### Observations and Adherence to Instructions\n\n- Monad Generalization: The SigmaProtocol structure now includes a monad parameter m and a sampleChal : m Chal field. This replaces the previous assumption of uniform challenge sampling via $ᵗ Chal in ProbComp. Corresponding definitions like realTranscript and PerfectlyComplete have been updated to use σ.sampleChal.\n- Refactored Theorems: Numerous theorems in the FiatShamir and Fischlin directories (e.g., perfectlyCorrect, euf_cma_bound, almostComplete) now include a hypothesis hsc : σ.sampleChal = ($ᵗ Chal : ProbComp Chal). This ensures that existing proofs, which rely on uniform sampling, remain valid while the underlying structure is more flexible.\n- Documentation: The module and declaration docstrings for SigmaProtocol in VCVio/CryptoFoundations/SigmaProtocol.lean were updated to describe the new monad parameter and its implications (e.g., usage in the Kilian transform). This aligns with the requirement for intrinsic and descriptive docstrings.\n- Style and Formatting:\n - Naming: The new parameter hsc (hypothesis for sigma challenge) follows project naming conventions.\n - Section Headers: The PR preserves the use of /-! ## Title -/ doc-headers for sectioning.\n - Lean Options: No per-file set_option lines or linter suppressions were introduced.\n - Sorry: No sorry placeholders were added to the codebase.\n- Attribution: No new files were added; existing file headers were preserved for routine edits, adhering to the attribution policy.

---

📄 **Per-File Summaries**

• Examples/Schnorr/SigmaProtocol.lean: The changes update the sigma definition for the Schnorr protocol by specifying ProbComp as the underlying computation type and providing a concrete implementation for the sampleChal field. No new theorems, proofs, or sorry placeholders were introduced.
• Examples/Schnorr/Signature.lean: This change modifies the proofs of Schnorr signature completeness and security by providing required reflexivity arguments to the FiatShamir library's completeness and unforgeability theorems. No new theorems were introduced, and no sorry or admit placeholders were added.
• VCVio/CryptoFoundations/FiatShamir/Sigma.lean: This update generalizes the FiatShamir signature construction to support Σ-protocols operating in arbitrary monads via MonadLiftT. It also refines the perfectlyCorrect theorem by adding a hypothesis that equates the protocol's challenge sampling with uniform sampling and updates the corresponding proof to utilize this assumption.
• VCVio/CryptoFoundations/FiatShamir/Sigma/CmaToNma.lean: This change updates the type signature of the SigmaProtocol variable in the CMA-to-NMA reduction to explicitly include the ProbComp type argument. This modification ensures consistency with the underlying protocol definition and the library's probabilistic computation framework.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean: This change modifies the SigmaProtocol variable declaration to include ProbComp as an explicit type parameter. This update ensures the protocol definition correctly reflects its probabilistic computational context within the Fiat-Shamir forking lemma framework.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Reductions.lean: This update modifies the cma_to_nma_advantage_bound theorem and its proof to include a new hypothesis requiring that the protocol's challenge sampling follows a uniform distribution. These changes refine the reduction between chosen-message and no-message attacks within the Sigma protocol framework.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Security.lean: This update refines the security theorems for the Fiat-Shamir transformation by requiring an explicit hypothesis that the Sigma protocol samples challenges uniformly. The changes modify the euf_cma_to_nma and euf_cma_bound theorems to include this requirement, ensuring consistency between the protocol's challenge generation and the expected probability distributions in the security proofs.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Bridge.lean: This change updates the SigmaProtocol variable declaration to include the ProbComp type parameter, aligning the bridge code with a revised signature for the underlying protocol structure. It is a structural update to the variable's type and does not introduce any new theorems or sorry placeholders.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean: This update refines the SigmaProtocol type signature to explicitly include the ProbComp monad and adds a uniform challenge sampling hypothesis to key security theorems, such as cma_advantage_le_fork_bound_of_h1h2. These changes modify existing proofs and definitions to ensure consistency with the updated protocol structure, without introducing any sorry or admit placeholders.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: The change updates the variable declaration for sigma protocols to include the ProbComp type argument, ensuring consistency with the protocol's generalized definition. This modification adjusts existing definitions to support the library's specific computational monad without introducing new theorems or proofs.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Games.lean: This change updates several CMA game definitions, including cmaRealFixedSign and cmaReal, to include an additional ProbComp type parameter for the SigmaProtocol argument. These modifications refine the signatures of the stateful Fiat-Shamir game components without introducing new theorems or sorry placeholders.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean: This file generalizes the SigmaProtocol type parameters to explicitly include the computation monad and modifies several theorems to require a new hypothesis ensuring uniform challenge sampling. These changes refine the formal proofs for CMA advantage and signing loss bounds in the Fiat-Shamir H3 hop by incorporating explicit distribution assumptions.
• VCVio/CryptoFoundations/Fischlin/Completeness.lean: The changes update SigmaProtocol definitions and theorems to explicitly include a computation parameter and a hypothesis requiring that challenges be sampled uniformly. These refinements are propagated through the completeness proofs for the Fischlin transform, ensuring the formal proofs correctly relate the protocol's challenge sampling to uniform distributions.
• VCVio/CryptoFoundations/Fischlin/CostAccounting.lean: The changes update the SigmaProtocol type signature across multiple definitions and sections to include an explicit ProbComp parameter. This ensures consistency with updated protocol definitions used in the Fischlin transformation's cost accounting proofs.
• VCVio/CryptoFoundations/Fischlin/Defs.lean: This change updates the fischlinSearchAux and Fischlin definitions to include the ProbComp monad as an explicit parameter in the SigmaProtocol type signature. These modifications ensure the Fischlin transformation remains compatible with the updated definition of sigma protocols without introducing new theorems or sorry placeholders.
• VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean: This change updates the SigmaProtocol variable signature in VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean to explicitly include the ProbComp type argument. This refactoring ensures consistency with the underlying probabilistic computation framework used in the security proofs.
• VCVio/CryptoFoundations/SigmaProtocol.lean: This change generalizes the SigmaProtocol structure and its associated definitions to operate over an arbitrary monad m instead of being fixed to ProbComp. It also adds an abstract sampleChal field to the structure for challenge generation and updates related theorems and properties—including completeness and honest-verifier zero-knowledge—to support this new polymorphic context.

---

Last updated: 2026-06-24 13:05 UTC.