Project-declaredLean 4.32.0 · mathlib@81a5d257

Cma advantage le fork bound of h5

FiatShamir.Stateful.cma_advantage_le_fork_bound_of_h5

program verification separation logic cryptography chain

Project documentation

Native stateful top-level chain, assuming the H5 replay-forking boundary. This theorem carries the H1/H2/H3/H4 arithmetic directly in the stateful chain. The bound is in terms of the verify-wrapped adversary nmaAdvFromCmaWithFinalQuery at fork slot parameter qH.

Exact Lean statement

theorem cma_advantage_le_fork_bound_of_h5
    (simT : Stmt → ProbComp (Commit × Chal × Resp))
    (ζ_zk : ℝ) (hζ_zk : 0 ≤ ζ_zk)
    (hHVZK : σ.HVZK simT ζ_zk)
    (β : ENNReal)
    (hPredSim : σ.simCommitPredictability simT β)
    (adv : SourceAdv (σ := σ) (hr := hr) (M := M))
    (qS qH : ℕ)
    (hQ : ∀ pk, signHashQueryBound (M := M) (Commit := Commit) (Chal := Chal)
      (S' := Commit × Resp) (oa := adv.main pk) qS qH)
    (hH1H2 :
      adv.advantage (FiatShamir.runtime M) ≤
        Pr[= true | (cmaReal M Commit Chal σ hr).runProb
          (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)])
    (hH5 :
      Pr[= true |
          (cmaSim M Commit Chal hr simT).runProb
            (cmaInit M Commit Chal Stmt Wit)
            (signedFreshAdv σ hr M adv)] ≤
        Fork.advantage σ hr M
          (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH) :
    adv.advantage (FiatShamir.runtime M) ≤
      Fork.advantage σ hr M
          (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH +
        ENNReal.ofReal ((qS : ℝ) * ζ_zk) +
        (qS : ENNReal) * ((qS : ENNReal) + (qH : ENNReal)) * β

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem cma_advantage_le_fork_bound_of_h5    (simT : Stmt → ProbComp (Commit × Chal × Resp))    (ζ_zk : ℝ) (hζ_zk : 0 ≤ ζ_zk)    (hHVZK : σ.HVZK simT ζ_zk)    (β : ENNReal)    (hPredSim : σ.simCommitPredictability simT β)    (adv : SourceAdv (σ := σ) (hr := hr) (M := M))    (qS qH : ℕ)    (hQ : ∀ pk, signHashQueryBound (M := M) (Commit := Commit) (Chal := Chal)      (S' := Commit × Resp) (oa := adv.main pk) qS qH)    (hH1H2 :      adv.advantage (FiatShamir.runtime M) ≤        Pr[= true | (cmaReal M Commit Chal σ hr).runProb          (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)])    (hH5 :      Pr[= true |          (cmaSim M Commit Chal hr simT).runProb            (cmaInit M Commit Chal Stmt Wit)            (signedFreshAdv σ hr M adv)] ≤        Fork.advantage σ hr M          (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH) :    adv.advantage (FiatShamir.runtime M) ≤      Fork.advantage σ hr M          (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH +        ENNReal.ofReal ((qS : ℝ) * ζ_zk) +        (qS : ENNReal) * ((qS : ENNReal) + (qH : ENNReal)) * β := by  let A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool :=    signedFreshAdv σ hr M adv  have hζ_zk_lt : ENNReal.ofReal ζ_zk < ∞ := ENNReal.ofReal_lt_top  have hHVZK' : σ.HVZK simT (ENNReal.ofReal ζ_zk).toReal := by    rwa [ENNReal.toReal_ofReal hζ_zk]  have hH3_abs :      ENNReal.ofReal          (((cmaReal M Commit Chal σ hr).runProb              (cmaInit M Commit Chal Stmt Wit) A).boolDistAdvantage            ((cmaSim M Commit Chal hr simT).runProb              (cmaInit M Commit Chal Stmt Wit) A))        ≤ (qS : ℝ≥0∞) * ENNReal.ofReal ζ_zk          + (qS : ℝ≥0∞) * ((qS : ℝ≥0∞) + (qH : ℝ≥0∞)) * β := by    simpa [A, cmaH3Advantage, QueryImpl.Stateful.advantage] using      signedFreshAdv_H3_bound (σ := σ) (hr := hr) (M := M)        (Commit := Commit) (Chal := Chal) (Resp := Resp)        adv simT (ENNReal.ofReal ζ_zk) β hζ_zk_lt hHVZK' hPredSim qS qH hQ  have hH3_prob :      Pr[= true | (cmaReal M Commit Chal σ hr).runProb        (cmaInit M Commit Chal Stmt Wit) A] ≤      Pr[= true | (cmaSim M Commit Chal hr simT).runProb        (cmaInit M Commit Chal Stmt Wit) A] +        ((qS : ℝ≥0∞) * ENNReal.ofReal ζ_zk          + (qS : ℝ≥0∞) * ((qS : ℝ≥0∞) + (qH : ℝ≥0∞)) * β) :=    le_trans      (ProbComp.probOutput_true_le_add_ofReal_boolDistAdvantage        ((cmaReal M Commit Chal σ hr).runProb          (cmaInit M Commit Chal Stmt Wit) A)        ((cmaSim M Commit Chal hr simT).runProb          (cmaInit M Commit Chal Stmt Wit) A))      (add_le_add le_rfl hH3_abs)  calc    adv.advantage (FiatShamir.runtime M)        ≤ Pr[= true | (cmaReal M Commit Chal σ hr).runProb          (cmaInit M Commit Chal Stmt Wit) A] := by            simpa [A] using hH1H2    _ ≤ Pr[= true | (cmaSim M Commit Chal hr simT).runProb          (cmaInit M Commit Chal Stmt Wit) A] +        ((qS : ℝ≥0∞) * ENNReal.ofReal ζ_zk          + (qS : ℝ≥0∞) * ((qS : ℝ≥0∞) + (qH : ℝ≥0∞)) * β) := hH3_prob    _ ≤ Fork.advantage σ hr M          (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH +        ((qS : ℝ≥0∞) * ENNReal.ofReal ζ_zk          + (qS : ℝ≥0∞) * ((qS : ℝ≥0∞) + (qH : ℝ≥0∞)) * β) :=        add_le_add hH5 le_rfl    _ = Fork.advantage σ hr M            (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH +          ENNReal.ofReal ((qS : ℝ) * ζ_zk) +          (qS : ENNReal) * ((qS : ENNReal) + (qH : ENNReal)) * β := by        rw [ENNReal.ofReal_mul (Nat.cast_nonneg qS), ENNReal.ofReal_natCast]        ring_nf

Project: VCVio
License: Apache-2.0
Commit: 2ceb2d825ee3
Source: VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean:2043-2119

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Expected Cost Nat eq sum tail probs of pathwise Cost At Most

AddWriterT.expectedCostNat_eq_sum_tail_probs_of_pathwiseCostAtMost

Plain-language statement

Finite tail-sum formula for natural-valued writer cost under a pathwise upper bound. If every execution path of oa incurs cost at most n, then the tail probabilities vanish above n, so the infinite tail sum truncates to Finset.range n.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

IND CPA advantage to Real le sum step signed Advantage Real abs

AsymmEncAlg.IND_CPA_advantage_toReal_le_sum_step_signedAdvantageReal_abs

Plain-language statement

Planned generic one-time-to-many-time lift: bounded multi-query IND-CPA advantage is at most the sum of the extracted one-time signed advantages over the first q fresh LR queries.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

IND CPA LR hybrid Game q eval Dist eq left of Makes At Most Queries

AsymmEncAlg.IND_CPA_LR_hybridGame_q_evalDist_eq_left_of_MakesAtMostQueries

Plain-language statement

If an adversary makes at most q fresh LR queries, then the leftUntil = q LR-hybrid is the all-left endpoint game.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record