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.

[github-actions]

🤖 PR Summary

Structural Generalization

• Generalize the SigmaProtocol structure to operate over an arbitrary monad m with HasEvalSPMF m, removing the hardcoded dependency on the ProbComp monad.
• Add an explicit sampleChal field to the SigmaProtocol definition to support monadic challenge sampling, providing the foundation for transformations such as Kilian's.
• Update the core properties of Sigma protocols—including completeness, special soundness, and Honest Verifier Zero-Knowledge (HVZK)—to account for the generalized monadic context.

Cryptographic Applications and Refactoring

• Refactor the Fiat-Shamir transformation library (including CmaToNma, Fork, and Stateful variants) to propagate the monad parameter through all definitions and theorems.
• Refine security proofs, including euf_cma_to_nma and cma_to_nma_advantage_bound, by adding explicit hypotheses requiring uniform challenge sampling.
• Adjust the Schnorr signature example and Fischlin's construction to maintain compatibility with the updated SigmaProtocol signature.

---

Statistics

Metric	Count
📝 Files Changed	14
✅ Lines Added	130
❌ Lines Removed	109

---

Lean Declarations

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

• def HVZK (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L126 to L132
• def PerfectlyComplete (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L67 to L75
• def toIdenSchemeWithAbort (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel ProbComp) : in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L227 to L233
• def realTranscript (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L109 to L115
• def PerfectHVZK (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L133 to L139
• def SpeciallySoundAt (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L81 to L89
• def UniqueResponses (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L216 to L222
• def SpeciallySound (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel m) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean moved from L88 to L96

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• Examples/Schnorr/SigmaProtocol.lean: This update refines the Schnorr sigma protocol definition by integrating the ProbComp computation context and implementing the sampleChal field for sampling challenges from the scalar field. The changes modify an existing definition without introducing any sorry or admit placeholders.
• Examples/Schnorr/Signature.lean: This update modifies the proofs for Schnorr signature completeness and existential unforgeability (EUF-CMA) by providing explicit reflexivity proofs to satisfy updated parameter requirements in the underlying Fiat-Shamir transformation library. The changes ensure the formal verification of the signature scheme remains consistent with recent modifications to the general Fiat-Shamir framework.
• VCVio/CryptoFoundations/FiatShamir/Sigma.lean: The changes generalize the FiatShamir signature scheme construction to support Sigma protocols defined over arbitrary monads and update the perfectlyCorrect theorem to include a hypothesis regarding challenge sampling. No sorry or admit placeholders were introduced.
• VCVio/CryptoFoundations/FiatShamir/Sigma/CmaToNma.lean: This change updates the variable declaration for the sigma protocol to explicitly include the ProbComp type parameter, ensuring compatibility with the updated definition of SigmaProtocol. No new theorems, proofs, or sorry placeholders are introduced in this modification.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean: This change updates the SigmaProtocol variable declaration to explicitly include the ProbComp type argument, ensuring consistency with the protocol's underlying definition.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Reductions.lean: This update refines the cma_to_nma_advantage_bound theorem by requiring that the Sigma protocol samples challenges uniformly from the challenge space. It also updates the protocol's signature to explicitly use the ProbComp monad and adjusts the corresponding proof to incorporate these new constraints.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Security.lean: This change updates the security theorems euf_cma_to_nma and euf_cma_bound to explicitly require a hypothesis that the protocol's challenge sampling is uniform. It also refines the SigmaProtocol variable signature to specify the ProbComp monad, ensuring the proofs correctly account for the distribution of challenges.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Bridge.lean: This change updates the variable declaration for the stateful sigma protocol to explicitly include the ProbComp monad parameter. This modification ensures type consistency across the library's definitions without introducing new theorems or proofs.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean: This update refines the SigmaProtocol type signatures to explicitly include the ProbComp monad and adds a hypothesis requiring uniform challenge sampling to several key security theorems. The changes modify the proofs for the stateful Fiat-Shamir construction to ensure challenge distribution properties are correctly handled.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: This change updates the type signature of the SigmaProtocol variable σ to include ProbComp as an explicit parameter, ensuring consistency with updated protocol definitions. The modification is a minor refactoring of variable declarations within the FiatShamir.Stateful namespace and does not introduce new theorems or sorry placeholders.
• 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 update modifies several definitions and theorems to include the ProbComp type parameter in SigmaProtocol signatures. It also introduces a new hypothesis requiring that challenge sampling be uniform in key lemmas, such as cmaRealSignGhost_public_evalDist_eq_publicDist and cmaReal_cmaSim_advantage_le_H3_bound, to more accurately reason about probability distributions.
• VCVio/CryptoFoundations/Fischlin.lean: Updates the SigmaProtocol type signature across all definitions and sections in Fischlin.lean to include the ProbComp parameter. These changes ensure consistency with a modified definition of Sigma protocols and do not introduce new theorems, modified proofs, or sorry placeholders.
• VCVio/CryptoFoundations/SigmaProtocol.lean: This change generalizes the SigmaProtocol structure and its associated properties (completeness, soundness, and HVZK) to operate over an arbitrary monad m with probability semantics. It also introduces an explicit sampleChal field to the structure to allow for non-uniform or oracle-dependent challenge sampling, while specializing the IdenSchemeWithAbort conversion to the ProbComp monad.

---

Last updated: 2026-05-30 20:32 UTC.