feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds

[alik-eth]

Extracts the generic GPV development out of #466 into its own self-contained PR, per @quangvdao's review there. #466 will be rebased on top of this branch and retitled to carry only the idealized-Falcon instantiation.

What this adds

A generic hash-and-sign framework in VCVio/CryptoFoundations/GPVHashAndSign/ following [GPV08], parameterized by a preimage-sampleable function (PSF), with the EUF-CMA reduction of [FGdG+25, Thm 1] shape:

• GPVHashAndSign.euf_cma_split_bound — the headline: any EUF-CMA forger's advantage is bounded by a PSF-collision adversary's advantage, plus an exact-match term (qSign + qHash) · programmedPreimageAdvantage, plus the salt-collision birthday bound (qSign + qHash)² / (2 · |Salt|).
• GPVHashAndSign.euf_cma_collision_bound — the collision-only corollary under a preimage-min-entropy hypothesis.
• GPVHashAndSign.forgery_yields_collision_or_exact_match / forgery_yields_collision — the core game hops (pre-sampled embed index, never-overwrite cache; no reservoir overwrite-restore).
• Examples/GPVNonVacuity.lean — a hypothesis-consistency (inhabitance) witness: a toy bijective PSF instance satisfying all side conditions simultaneously. Logical consistency only; no quantitative security content.

Module layout

Split along proof phases per review of #465/#466: Basic → CollisionTelescope → Factorization → GameRuns → TapeFactorization → FlagHandlers → CombinedHandler → GameIdentification → VerificationBridge → TrapCount → EmbedIndex → Security, re-exported by the umbrella module (no consumer or name changes).

The only touch outside the new framework is an 8-line arity adaptation of the two sorried legacy Falcon placeholder statements (collisionBound now takes qHash); that file is rewritten wholesale in #466.

Verification

• lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets green on leanprover/lean4:v4.31.0, zero non-sorry warnings.
• Kernel axiom check: all four headline theorems and the witness report [propext, Classical.choice, Quot.sound].

Scope caveats (disclosed in the code)

• The forge-a-queried-point convention (hForge) is the standard ROM WLOG, stated as a hypothesis; the append-query compiler discharging it is planned follow-up work (feat(Falcon): idealized-model EUF-CMA via GPV, down to NTRU-SIS (#188) #466 thread).
• Query counts are pinned by the signHashQueryBound hypothesis; reductions are not cost-tracked.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

sorry delta: -4 (4 removed) — net proof progress

PR Overview: Generic GPV Hash-and-Sign Framework with EUF-CMA Collision Bounds

Mathematical Formalization

This PR introduces a self-contained generic hash-and-sign framework in VCVio/CryptoFoundations/GPVHashAndSign/, following [GPV08] and the EUF-CMA reduction of [FGdG+25, Thm 1]. The framework is parameterized by a preimage-sampleable function (PSF), defined in Basic.lean as the PreimageSampleableFunction structure (fields eval, trapdoorSample, isShort), together with correctness (Correct, CorrectAt) and regularity (Regularity) properties. The GPVHashAndSign signature scheme is built on top as a SignatureAlg using the random oracle, parameterized by a PSF, a generable key relation, a salt type, and a message type.

Main Security Theorems (all in Security.lean and exposed via the umbrella module)

• GPVHashAndSign.euf_cma_split_bound — the headline: any EUF-CMA forger's advantage is bounded by a PSF-collision adversary's advantage plus an exact-match term (qSign + qHash) · programmedPreimageAdvantage plus the salt-collision birthday bound (qSign + qHash)² / (2 · |Salt|) (via collisionBound).
• GPVHashAndSign.euf_cma_collision_bound — the collision-only corollary under a preimage-min-entropy hypothesis.
• GPVHashAndSign.forgery_yields_collision_or_exact_match / forgery_yields_collision — the core game hops (pre-sampled embed index, never-overwrite cache; no reservoir overwrite-restore).

Append-Query Compiler (discrepancy with PR body)

The PR includes a compiler appendForgeQuery in AppendQuery.lean that transforms an arbitrary adversary into one satisfying the ForgesQueriedPoint convention. The three key lemmas are:

• forgesQueriedPoint_appendForgeQuery: the compiled adversary unconditionally queries its forgery point.
• signHashQueryBound_appendForgeQuery: the query bound increases by one hash (qHash + 1).
• advantage_appendForgeQuery: the EUF-CMA advantage is exactly preserved.

The final corollary euf_cma_split_bound_of_queryBound discharges the ForgesQueriedPoint hypothesis from the headline bound, making it applicable to any adversary given only query bounds. Note: The PR body states this compiler is “planned follow‑up work (#466 thread)”, but the code in this PR already implements it. The overview here reflects the actual code; the PR body is inaccurate on this point.

Supporting Mathematical Infrastructure

• Collision telescope (CollisionTelescope.lean): defines the salt-collision reduction (reduction), the birthday bound collisionBound, the salt-drawing collision process saltSeq, and proves coupling theorems signRunF_tvDist_le_saltSeq and signRunF_tvDist_le_collisionBound that bound TV distance by the salt-collision probability.
• Factorization (Factorization.lean): formalizes the adaptive GPV run through fixed-step signRunF recursion; introduces AdaptiveFactorizesSignRunF predicate and proves factorized_advantage_le_collisionBound using the data-processing inequality.
• Flag handlers (FlagHandlers.lean): flag‑instrumented game runs (gpvRealImplFlag, progGameRunImplNoRecFlag) with a collision flag, proving gpv_orig_flag_le_collisionBound and extending to the verify‑Bool coupling.
• Min‑entropy analysis (MinEntropy.lean): defines trapdoorGuessingProbability and proves programmedPreimageAdvantage_le_trapdoorGuessingProbability, supplying the exact‑match branch for euf_cma_collision_bound.
• Tape factorization (TapeFactorization.lean): rephrases real/programmed runs as a front block of salts drawn from drawList ($ᵗ Salt) qSign followed by a tape‑consuming simulation; provides bridging theorems realGameRun_eq_drawList_gpvRealImplTape and progGameRun_eq_drawList_progGameRunImplTape.
• Combined handler (CombinedHandler.lean): defines the combined handler progGameRunImplCombined that runs the programmed freshness game and the collision reduction in lockstep, with invariants combinedCacheTableInv and combinedCacheImpliesTableInv.
• Embed index, trap count, verification bridge, sampler transport: additional submodules (EmbedIndex, TrapCount, VerificationBridge, SamplerTransport) providing index‑augmented handlers, counter instruments, the forger‑queries‑point property, and adaptive sampler‑swap TV accumulation lemmas.
• Game identification (GameIdentification.lean): summary unavailable (parsing error), but the file is part of the framework.

Non‑vacuity Witness

Examples/GPVNonVacuity.lean provides a concrete bijective PSF instance bijPSF over Bool (keys Unit, identity eval, inverse trapdoorSample, constantly‑true shortness), a trivial generable relation, and a query‑then‑forge adversary adv. It proves gpv188_hyps_inhabited showing all four side conditions of the headline theorems are simultaneously satisfiable. This is a logical consistency check, not a quantitative security witness.

Protocols / Soundness

The PR provides the following EUF‑CMA bounds:

1. Split bound: euf_cma_split_bound (with ForgesQueriedPoint hypothesis) and euf_cma_split_bound_of_queryBound (discharging it via the append‑query compiler).
2. Collision bound: euf_cma_collision_bound under a preimage‑min‑entropy hypothesis.
3. One‑sided and symmetric sampler‑transport bounds in SamplerTransport.lean: advantage_le_advantage_add_of_trapdoorSample_tvDist and abs_advantage_toReal_sub_le_of_trapdoorSample_tvDist, which allow swapping the trapdoor sampler at a TV cost.

The formalization is parameterized by qSign and qHash via the signHashQueryBound predicate. The birthday bound collisionBound now uses (qSign + qHash)² / (2 · |Salt|), reflecting the inclusion of hash queries.

Infrastructure / CI

• lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets passes on leanprover/lean4:v4.31.0 with zero non‑sorry warnings.
• Kernel axiom check: all four headline theorems and the witness report [propext, Classical.choice, Quot.sound].
• No sorry or admit are introduced by this PR. (The existing sorried Falcon placeholder statements in LatticeCrypto/Falcon/Security.lean have their signature updated but remain sorried; no new placeholders are added.)

Refactoring

• The monolithic VCVio/CryptoFoundations/GPVHashAndSign.lean is restructured into an umbrella module that re‑exports content from 15 submodules (Basic, MinEntropy, CollisionTelescope, Factorization, GameRuns, TapeFactorization, FlagHandlers, CombinedHandler, GameIdentification, VerificationBridge, TrapCount, EmbedIndex, Security, AppendQuery, SamplerTransport). The module docstring now reflects the modular layout and the updated birthday bound formula; authors include Oleksandr Vovkotrub.
• VCVio.lean adds imports of the 15 new submodules, making them available downstream.
• LatticeCrypto/Falcon/Security.lean (8‑line change): euf_cma_security and euf_cma_security_bytes40 now pass qHash as an additional argument to collisionBound. The docstring of euf_cma_security_bytes40 is updated to reflect the new collision term (qSign + qHash)² / (2 · 2^320). These changes adapt the existing (sorried) Falcon placeholder statements to the updated API.

Documentation

• Module‑level docstring for GPVHashAndSign.lean updated to describe the modular layout and the new birthday bound.
• Falcon/Security.lean docstring updated to reflect the inclusion of qHash in the collision bound.

Note: The per‑file summary for GameIdentification.lean was unavailable due to a parsing error, but the file is included and participates in the module structure.

---

Statistics

Metric	Count
📝 Files Changed	20
✅ Lines Added	12991
❌ Lines Removed	376

---

Lean Declarations

✏️ Removed: 18 declaration(s)

VCVio/CryptoFoundations/GPVHashAndSign.lean (18)

• abbrev CollisionAdversary
• abbrev ProgrammedPreimageAdversary
• def Correct (psf : PreimageSampleableFunction PK SK Domain Range) : Prop
• def GPVHashAndSign
• def collisionFindingExp [DecidableEq Domain]
• def hashQueryBound {S' α : Type}
• def programmedPreimageExp [DecidableEq Domain]
• def signHashQueryBound {S' α : Type}
• noncomputable def collisionBound (qSign : ℕ) : ENNReal
• noncomputable def collisionFindingAdvantage [DecidableEq Domain]
• noncomputable def programmedPreimageAdvantage [DecidableEq Domain]
• noncomputable def programmedPreimageReduction
• noncomputable def reduction
• noncomputable def runtime :
• theorem euf_cma_collision_bound [DecidableEq Domain]
• theorem euf_cma_split_bound [DecidableEq Domain]
• theorem forgery_yields_collision [DecidableEq Domain]
• theorem forgery_yields_collision_or_exact_match [DecidableEq Domain]

✏️ Added: 360 declaration(s)

Examples/GPVNonVacuity.lean (10)

• def bijPSF : PreimageSampleableFunction Unit Unit Bool Bool where
• def hr : GenerableRelation Unit Unit (fun _ _ => true) where
• lemma step_caches (pk : Unit)
• noncomputable def adv :
• noncomputable def domainSample : Unit → ProbComp Bool
• theorem adv_signHashQueryBound (pk : Unit) :
• theorem bijPSF_correct : bijPSF.Correct
• theorem bijPSF_hForge :
• theorem bijPSF_regularity : bijPSF.Regularity
• theorem gpv188_hyps_inhabited :

VCVio/CryptoFoundations/GPVHashAndSign/AppendQuery.lean (12)

• def appendForgeQuery
• lemma advantage_eq_keygen_average_realGameVerifyFresh
• lemma appendForgeQuery_main
• lemma gpvRealImplFlagFresh_run_liftM_query (pk : PK) (sk : SK) (mc : Salt × M)
• lemma gpvRealImplFlagFresh_run_read_bind_run_read (pk : PK) (sk : SK) (mc : Salt × M)
• lemma progGameRunImplNoRecFlagFresh_read_caches (domainSample : PK → ProbComp Domain)
• theorem advantage_appendForgeQuery
• theorem euf_cma_split_bound_of_queryBound [DecidableEq Domain]
• theorem forgesQueriedPoint_appendForgeQuery
• theorem realGameVerifyFresh_appendForgeQuery (pk : PK) (sk : SK)
• theorem signHashQueryBound_appendForgeQuery
• theorem withCaching_run_bind_run_self (so : QueryImpl spec m) (t : spec.Domain)

VCVio/CryptoFoundations/GPVHashAndSign/Basic.lean (12)

• abbrev CollisionAdversary
• abbrev ProgrammedPreimageAdversary
• def Correct (psf : PreimageSampleableFunction PK SK Domain Range) : Prop
• def CorrectAt (psf : PreimageSampleableFunction PK SK Domain Range) (pk : PK) (sk : SK) : Prop
• def GPVHashAndSign
• def Regularity [SampleableType Range]
• def collisionFindingExp [DecidableEq Domain]
• def programmedPreimageExp [DecidableEq Domain]
• def signHashQueryBound {S' α : Type}
• noncomputable def collisionFindingAdvantage [DecidableEq Domain]
• noncomputable def programmedPreimageAdvantage [DecidableEq Domain]
• noncomputable def runtime :

VCVio/CryptoFoundations/GPVHashAndSign/CollisionTelescope.lean (18)

• lemma probEvent_mem_uniformSample (cache : Finset Salt) :
• lemma probEvent_salt_collision_le_collisionBound (qSign qHash : ℕ)
• lemma sum_range_div_card_le_collisionBound (qSign qHash : ℕ) :
• noncomputable def collisionBound (qSign qHash : ℕ) : ENNReal
• noncomputable def reduction
• noncomputable def saltSeq (c : ℕ → Finset Salt) : (n : ℕ) → ProbComp Bool
• noncomputable def signRunF {St : Type} (step : ℕ → St → Salt → ProbComp St)
• theorem evalDist_signRunF_bind_const {St γ : Type} [Nonempty Salt]
• theorem probEvent_saltSeq_le (c : ℕ → Finset Salt) (n : ℕ) :
• theorem probEvent_saltSeq_le_collisionBound (qSign qHash : ℕ)
• theorem probEvent_saltSeq_succ (c : ℕ → Finset Salt) (n : ℕ) :
• theorem signRunF_neverFail {St : Type} [Nonempty Salt]
• theorem signRunF_tvDist_le_collisionBound {St : Type} [Finite Salt] [Nonempty Salt]
• theorem signRunF_tvDist_le_saltSeq {St : Type} [Finite Salt]
• theorem signRunF_tvDist_le_saltSeq_aux {St : Type} [Finite Salt]
• theorem tsum_probOutput_uniformSample_ite (s : Finset Salt) (q : ℝ≥0∞) :
• theorem tvDist_bind_le_of_forall_le {α β : Type} (mx : ProbComp α) (f g : α → ProbComp β)
• theorem tvDist_signStep_real_programmed_le_collision [Nonempty Salt] {β : Type}

VCVio/CryptoFoundations/GPVHashAndSign/CombinedHandler.lean (40)

• def combinedCacheImpliesTableInv (pk : PK)
• def combinedCacheTableInv (pk : PK)
• def combinedTableInDomainInv (M Salt : Type) (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma combinedCacheImpliesTableInv_step (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma combinedCacheTableInv_step (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma combinedTableInDomainInv_step (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma embedAtIndexImpl_run_inl_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma embedAtIndexImpl_run_inl_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma embedAtIndexImpl_run_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma embedTrapImpl_run_inl_inl (pk : PK) (sk : SK)
• lemma embedTrapImpl_run_inl_inr (pk : PK) (sk : SK)
• lemma embedTrapImpl_run_inr (pk : PK) (sk : SK)
• lemma evalDist_embedAtIndex_step_eq_embedTrap
• lemma evalDist_progGameRunImplCombined_step_eq_trap
• lemma evalDist_run_embedAtIndexImpl_eq_embedTrap {β : Type}
• lemma evalDist_run_progGameRunImplCombinedTrap_eq {β : Type}
• lemma map_run_progGameRunImplCombined_proj_reduction (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma map_run_progGameRunImplCombined_proj_table (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombinedTrap_run_inl_inl (pk : PK)
• lemma progGameRunImplCombinedTrap_run_inl_inr (pk : PK)
• lemma progGameRunImplCombinedTrap_run_inr (pk : PK)
• lemma progGameRunImplCombined_proj_reduction (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_proj_table (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_run_cacheImpliesTable (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_run_inl_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_run_inl_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_run_inr (domainSample : PK → ProbComp Domain) (pk : PK) (msg : M)
• lemma progGameRunImplCombined_run_inv (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplCombined_run_tableInDomain (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRec_run_inl_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRec_run_inl_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma reductionImpl_run_inl_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma reductionImpl_run_inl_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma reductionImpl_run_inr (domainSample : PK → ProbComp Domain) (pk : PK) (msg : M)
• lemma reduction_eq_run_reductionImpl
• noncomputable def embedAtIndexImpl (domainSample : PK → ProbComp Domain) (pk : PK)
• noncomputable def embedTrapImpl (pk : PK) (sk : SK)
• noncomputable def progGameRunImplCombined (domainSample : PK → ProbComp Domain) (pk : PK) :
• noncomputable def progGameRunImplCombinedTrap (pk : PK) (sk : SK) :
• noncomputable def reductionImpl (domainSample : PK → ProbComp Domain) (pk : PK) :

VCVio/CryptoFoundations/GPVHashAndSign/EmbedIndex.lean (20)

• lemma embedTrapFreshIdxSigImpl_proj (pk : PK) (sk : SK)
• lemma embedTrapFreshIdxSigImpl_run_inl_inl (pk : PK) (sk : SK) (q : unifSpec.Domain)
• lemma embedTrapFreshIdxSigImpl_run_inl_inr (pk : PK) (sk : SK) (q : (Salt × M →ₒ Range).Domain)
• lemma embedTrapFreshIdxSigImpl_run_inr (pk : PK) (sk : SK) (msg : M)
• lemma embedTrapIdxSigImpl_fresh_idx_cache_eq (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma embedTrapIdxSigImpl_fresh_idx_cache_eq_general (pk : PK) (sk : SK) (j : ℕ) (y : Range) :
• lemma embedTrapIdxSigImpl_proj (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma embedTrapIdxSigImpl_run_inl_inl (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma embedTrapIdxSigImpl_run_inl_inr (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma embedTrapIdxSigImpl_run_inr (pk : PK) (sk : SK) (j : ℕ) (y : Range) (msg : M)
• lemma embedTrapIdxSigImpl_run_step_count_le (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma embedTrapIdxSigImpl_run_step_eq_embedTrapFreshIdxSig (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma evalDist_frontDraw_embedTrapIdxSigImpl_eq_embedTrapFreshSigImpl [Inhabited Range]
• lemma evalDist_run_embedTrapIdxSigImpl_eq_embedTrapFreshIdxSig_of_lt (pk : PK) (sk : SK) (j : ℕ)
• lemma map_run_embedTrapFreshIdxSigImpl_proj (pk : PK) (sk : SK)
• lemma map_run_embedTrapIdxSigImpl_proj (pk : PK) (sk : SK) (j : ℕ) (y : Range)
• lemma progGameRunImplCombinedTrapCount_table_support (pk : PK) (sk : SK) :
• lemma tsum_probOutput_embedTrapFreshIdxSig_mul_eq_frontDraw [Inhabited Range]
• noncomputable def embedTrapFreshIdxSigImpl (pk : PK) (sk : SK) :
• noncomputable def embedTrapIdxSigImpl (pk : PK) (sk : SK) (j : ℕ) (y : Range) :

VCVio/CryptoFoundations/GPVHashAndSign/Factorization.lean (9)

• def AdaptiveFactorizesSignRunF [Nonempty Salt] {α : Type}
• noncomputable def gpvStepProg (pk : PK) (domainSample : PK → ProbComp Domain) (msgs : ℕ → M) :
• noncomputable def gpvStepReal (pk : PK) (sk : SK) (msgs : ℕ → M) :
• theorem evalDist_gpvSignBody_run_eq_gpvStepProg (pk : PK) (domainSample : PK → ProbComp Domain)
• theorem evalDist_gpvSignBody_run_eq_gpvStepReal (pk : PK) (sk : SK) (msgs : ℕ → M) (n : ℕ)
• theorem factorized_advantage_le_collisionBound [Finite Salt] [Nonempty Salt] {α : Type}
• theorem gpvStepReal_neverFail (pk : PK) (sk : SK) (msgs : ℕ → M)
• theorem gpvStep_agree (pk : PK) (sk : SK) (msgs : ℕ → M)
• theorem regularity_signAnswer_agree (hreg : psf.Regularity) (pk : PK) (sk : SK) :

VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean (45)

• lemma gpvRealImplFlagFresh_bad_mono (pk : PK) (sk : SK)
• lemma gpvRealImplFlagFresh_proj (pk : PK) (sk : SK)
• lemma gpvRealImplFlagFresh_proj_flag (pk : PK) (sk : SK)
• lemma gpvRealImplFlagFresh_run_inl (pk : PK) (sk : SK)
• lemma gpvRealImplFlagFresh_run_inr (pk : PK) (sk : SK) (msg : M)
• lemma gpvRealImplFlag_bad_mono (pk : PK) (sk : SK)
• lemma gpvRealImplFlag_proj_fst (pk : PK) (sk : SK)
• lemma gpvRealImplFlag_run_inl (pk : PK) (sk : SK)
• lemma gpvRealImplFlag_run_inr (pk : PK) (sk : SK) (msg : M)
• lemma gpvRealImplFresh_run_inl (pk : PK) (sk : SK)
• lemma gpvRealImplFresh_run_inr (pk : PK) (sk : SK) (msg : M)
• lemma keyedSalts_cacheQuery_card_le (cache : (Salt × M →ₒ Range).QueryCache)
• lemma keyedSalts_randomOracle_run_card_le (mc : Salt × M)
• lemma map_run_gpvRealImplFlagFresh_eq (pk : PK) (sk : SK)
• lemma map_run_gpvRealImplFlagFresh_proj_flag (pk : PK) (sk : SK) {β : Type}
• lemma map_run_gpvRealImplFlag_eq (pk : PK) (sk : SK)
• lemma map_run_progGameRunImplNoRecFlag_eq (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma probEvent_flag_gpvRealImplFlagFresh_eq (pk : PK) (sk : SK)
• lemma probOutput_flagSignedTag_false {α' : Type}
• lemma progGameRunImplNoRecFlagFresh_bad_mono (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlagFresh_proj (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlagFresh_run_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlagFresh_run_inr (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlag_bad_mono (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlag_proj_fst (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlag_run_inl (domainSample : PK → ProbComp Domain) (pk : PK)
• lemma progGameRunImplNoRecFlag_run_inr (domainSample : PK → ProbComp Domain) (pk : PK) (msg : M)
• noncomputable def gpvRealImplFlag (pk : PK) (sk : SK) :
• noncomputable def gpvRealImplFlagFresh (pk : PK) (sk : SK) :

…and 210 more not listed.

---

sorry Tracking

✅ Removed: 4 `sorry`(s)

VCVio/CryptoFoundations/GPVHashAndSign.lean (4)

• noncomputable def programmedPreimageReduction (L283)
• noncomputable def reduction (L270)
• theorem forgery_yields_collision [DecidableEq Domain] (L332)
• theorem forgery_yields_collision_or_exact_match [DecidableEq Domain] (L363)

---

Coverage Notes

• AI file summarization partially analyzed 6 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• VCVio/CryptoFoundations/GPVHashAndSign/CombinedHandler.lean (+1103/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean (+1394/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/GameRuns.lean (+1252/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/Security.lean (+1958/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/TrapCount.lean (+1351/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/VerificationBridge.lean (+1399/-0)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• Examples.lean: Added an import of Examples.GPVNonVacuity, making the definitions and theorems from that module (related to proving non‑vacuity of the GPV construction) accessible in the Examples file.
• Examples/GPVNonVacuity.lean: This new file provides a logical consistency (inhabitance) witness for the side conditions of the GPV hash-and-sign EUF-CMA bounds (GPVHashAndSign.forgery_yields_collision_or_exact_match and its euf_cma_* corollaries). It defines a concrete bijective PSF bijPSF over Bool with keys in Unit (identity eval, inverse trapdoorSample, constantly‑true shortness), a trivial generable relation hr, and a query‑then‑forge adversary adv that queries the random oracle once at ((), ()) and forges at the same point. The file includes proofs of bijPSF_correct, bijPSF_regularity, bijPSF_hForge (the forger queries its forgery point), and adv_signHashQueryBound (zero signing, one random‑oracle query). These are assembled into the conjunction gpv188_hyps_inhabited, which shows all four side conditions are simultaneously satisfiable.
• LatticeCrypto/Falcon/Security.lean: The diff modifies two theorems in LatticeCrypto/Falcon/Security.lean. In euf_cma_security, the call to GPVHashAndSign.collisionBound now takes an additional argument qHash (the number of hash queries), changing its signature from collisionBound Salt qSign to collisionBound Salt qSign qHash. The docstring of euf_cma_security_bytes40 is updated to reflect that the collision term is now (qSign + qHash)² / (2 · 2^320) instead of qSign² / (2 · 2^320), and the corresponding call to collisionBound in that theorem is similarly updated to include qHash. These changes incorporate the hash query count into the collision bound calculation, making the security bound more accurate.
• VCVio.lean: The file VCVio.lean now imports 14 new submodules from VCVio.CryptoFoundations.GPVHashAndSign, adding definitions and theorems including AppendQuery, Basic, CollisionTelescope, CombinedHandler, EmbedIndex, Factorization, FlagHandlers, GameIdentification, GameRuns, MinEntropy, SamplerTransport, Security, TapeFactorization, TrapCount, and VerificationBridge. These imports expand the available API for the GPV hash-and-sign signature scheme, enabling downstream use of the corresponding constructs and proofs.
• VCVio/CryptoFoundations/GPVHashAndSign.lean: This file was entirely restructured: instead of containing the full GPV hash-and-sign scheme definition, security reductions, and theorem statements inline, it became a thin umbrella module that imports and re-exports the content from 13 submodules (Basic, MinEntropy, CollisionTelescope, Factorization, GameRuns, TapeFactorization, FlagHandlers, CombinedHandler, GameIdentification, VerificationBridge, TrapCount, EmbedIndex, Security, AppendQuery, SamplerTransport). The PreimageSampleableFunction structure, GPVHashAndSign definition, all reduction functions (reduction, programmedPreimageReduction), the query bound predicates (hashQueryBound, signHashQueryBound), the game-hopping experiments (collisionFindingExp, programmedPreimageExp), and all security theorems (forgery_yields_collision, forgery_yields_collision_or_exact_match, euf_cma_collision_bound, euf_cma_split_bound) were moved out of this file. The module-level docstring was updated to describe the new modular layout and to note that the birthday bound now uses (qSign + qHash)² / (2 · |Salt|) (GPVHashAndSign.collisionBound) instead of the simpler qSign² / (2 · |Salt|); the authors list was extended to include Oleksandr Vovkotrub.
• VCVio/CryptoFoundations/GPVHashAndSign/AppendQuery.lean: This new file AppendQuery.lean introduces a compiler appendForgeQuery that transforms an arbitrary GPV Hash-and-Sign EUF-CMA adversary into one satisfying the ForgesQueriedPoint convention (the forger queries the random oracle at its forgery point). The file proves three key properties: forgesQueriedPoint_appendForgeQuery states the compiled adversary unconditionally meets the convention; signHashQueryBound_appendForgeQuery shows the query bound increases by one hash (qHash + 1) with unchanged signing count; advantage_appendForgeQuery proves the EUF-CMA advantage is preserved exactly, using absorption lemmas gpvRealImplFlagFresh_run_read_bind_run_read and QueryImpl.withCaching_run_bind_run_self. The final theorem euf_cma_split_bound_of_queryBound discharges the ForgesQueriedPoint hypothesis from the headline bound, yielding a corollary that applies to any adversary given only a query bound. The file contains no sorry or admit statements.
• VCVio/CryptoFoundations/GPVHashAndSign/Basic.lean: This new file introduces the GPV hash-and-sign signature framework in the random-oracle model. It defines the PreimageSampleableFunction structure (with fields eval, trapdoorSample, and isShort) together with its Correct, CorrectAt, and Regularity properties. It then defines the GPVHashAndSign signature scheme, parameterized by a PSF, a generable key relation, a salt type, and message type, as a SignatureAlg using the random oracle. The file also provides: the noncomputable runtime bundle for the oracle world; the structural query bound signHashQueryBound that separates signing-oracle and random-oracle query counts; the keyed CollisionAdversary and collisionFindingExp (with corresponding collisionFindingAdvantage); and the ProgrammedPreimageAdversary and programmedPreimageExp (with programmedPreimageAdvantage) for the exact-match programmed-preimage experiment, which are the adversary interfaces used in the EUF-CMA proof.
• VCVio/CryptoFoundations/GPVHashAndSign/CollisionTelescope.lean: This new file introduces the salt-collision telescope for the GPV Hash-and-Sign security proof, defining the reduction adversary reduction, the birthday bound collisionBound, the salt-drawing collision process saltSeq, the flag-carrying signing process signRunF, and proving coupling theorems (signRunF_tvDist_le_saltSeq, signRunF_tvDist_le_collisionBound) that bound the total variation distance between real and programmed runs by the salt-collision probability. It also includes per-draw probability lemmas (probEvent_mem_uniformSample) and the arithmetic core (sum_range_div_card_le_collisionBound) leading to the collisionBound, as well as the inclusion-exclusion identity tsum_probOutput_uniformSample_ite and the per-step coupling primitive tvDist_signStep_real_programmed_le_collision. The file is entirely new and contains no sorry or admit.
• VCVio/CryptoFoundations/GPVHashAndSign/CombinedHandler.lean: This new file introduces the combined handler progGameRunImplCombined that runs the programmed freshness game and the collision reduction in lockstep, threading the game state ((cache × signedSet) × flag) together with the reduction’s hidden preimage table (Salt × M) → Option Domain. It defines the collision‑reduction internal handler reductionImpl and the pre‑sampled‑index handler embedAtIndexImpl (with its trapdoor‑uniform sibling embedTrapImpl), along with one‑step unfolding lemmas and per‑step/run‑level equidistribution lemmas (evalDist_embedAtIndex_step_eq_embedTrap, evalDist_run_embedAtIndexImpl_eq_embedTrap, evalDist_progGameRunImplCombined_step_eq_trap, evalDist_run_progGameRunImplCombinedTrap_eq) under GPV regularity. The file also provides projection lemmas (progGameRunImplCombined_proj_table, map_run_progGameRunImplCombined_proj_table, progGameRunImplCombined_proj_reduction, map_run_progGameRunImplCombined_proj_reduction) that recover the game handler progGameRunImplNoRecFlagFresh and the reduction handler reductionImpl from the combined run. Two coherence invariants (combinedCacheTableInv, combinedCacheImpliesTableInv) and their preservation lemmas (combinedCacheTableInv_step, progGameRunImplCombined_run_inv, combinedCacheImpliesTableInv_step, progGameRunImplCombined_run_cacheImpliesTable) certify that the cache and table stay consistent throughout the simulation. Finally, the incomplete predicate combinedTableInDomainInv is introduced. No sorry or admit appear in the visible portion of the file.
• VCVio/CryptoFoundations/GPVHashAndSign/EmbedIndex.lean: This new file EmbedIndex.lean introduces signed-set-augmented variants of the index-embedding query handlers for the GPV Hash-and-Sign construction. It defines embedTrapIdxSigImpl and embedTrapFreshIdxSigImpl, which extend the existing embedTrapIdxImpl and embedTrapFreshIdxImpl with a passive Finset M signed set that is updated only on signing queries. The file provides per-query and run-level projection lemmas (embedTrapIdxSigImpl_proj, map_run_embedTrapIdxSigImpl_proj, and their Fresh counterparts) showing that dropping the signed set recovers the original handlers. It also proves equivalence lemmas between the two signed-set-augmented handlers off the winner slot (embedTrapIdxSigImpl_run_step_eq_embedTrapFreshIdxSig) and after the counter passes the winner index (evalDist_run_embedTrapIdxSigImpl_eq_embedTrapFreshIdxSig_of_lt), a front-loading lift (evalDist_frontDraw_embedTrapIdxSigImpl_eq_embedTrapFreshSigImpl and its expectation form tsum_probOutput_embedTrapFreshIdxSig_mul_eq_frontDraw), a freshness-confined winner-slot cache invariant (embedTrapIdxSigImpl_fresh_idx_cache_eq_general and its specialization embedTrapIdxSigImpl_fresh_idx_cache_eq), and a write-only trapdoor-table support invariant (progGameRunImplCombinedTrapCount_table_support).
• VCVio/CryptoFoundations/GPVHashAndSign/Factorization.lean: This new file (306 lines) formalizes the factorization of the adaptive GPV Hash-and-Sign game through fixed-step signRunF recursion. It introduces the regularity_signAnswer_agree theorem, which witnesses the distributional agreement (under PSF regularity) between the real cache-miss signing answer (uniform target, trapdoor preimage) and the programmed signing answer (forward-sample preimage, derived target). It defines the AdaptiveFactorizesSignRunF predicate as a typed Prop packaging the existence of handler states, real/programmed step handlers, a recorded-cache sequence with cardinality bound card (c j) ≤ j + qHash, and a shared post-processor such that both adaptive runs equal the corresponding signRunF distributions. The factorized_advantage_le_collisionBound theorem uses this predicate to bound the total-variation distance between adaptive real and programmed runs by collisionBound Salt qSign qHash.toReal, leveraging the data-processing inequality and the unconditional signRunF_tvDist_le_collisionBound. It then provides concrete GPV witnesses: gpvStepReal (cache-miss: uniform target, trapdoor preimage) and gpvStepProg (sign-then-hash: forward-sample, program cache), along with gpvStepReal_neverFail (never-fail guarantee given total trapdoor sampler), gpvStep_agree (distributional agreement of the two handlers under regularity), evalDist_gpvSignBody_run_eq_gpvStepReal (equality of real signing-body cache transition with gpvStepReal on a cache miss), and evalDist_gpvSignBody_run_eq_gpvStepProg (equality of programmed simulator signing-body cache transition with gpvStepProg with front-loaded salt draw). No sorry or admit are present.
• VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean: This file introduces flag-instrumented versions of the original inline-salt GPV hash-and-sign handlers and a freshness-tracking vehicle for the verify-Bool coupling. It defines gpvRealImplFlag and progGameRunImplNoRecFlag, which thread a collision flag (set when an inline-drawn signing salt collides with the random-oracle cache) through the real and programmed game runs, and proves per-query and run-level projection lemmas (gpvRealImplFlag_proj_fst, map_run_gpvRealImplFlag_eq, etc.) showing that dropping the flag recovers the original handlers. It establishes bad-monotonicity (gpvRealImplFlag_bad_mono, progGameRunImplNoRecFlag_bad_mono) and the universal off-bad per-query agreement gpvImplFlag_h_agree_good, which together with the framework lemma tvDist_simulateQ_run_le_probEvent_output_bad yields the main reduction gpv_tvDist_orig_run_le_probEvent_flag bounding the total-variation distance between the real and programmed game runs by the run-level collision-flag probability. The file then proves the cardinality-telescope bound gpv_orig_flag_le_collisionBound (via the auxiliary gpv_orig_flag_le_collisionBound_aux), showing that the flag probability is at most collisionBound Salt qSign qHash, and extends this to the verify-Bool coupling gpv_tvDist_orig_verify_le_collisionBound where a signing-free verification continuation is appended. Finally, it introduces freshness-tracking handlers gpvRealImplFlagFresh and progGameRunImplNoRecFlagFresh that additionally record the set of signed messages, providing the vehicle for the EUF-CMA freshness mask.
• VCVio/CryptoFoundations/GPVHashAndSign/GameIdentification.lean: Summary unavailable — error: Expecting value: line 1251 column 1 (char 6875)
• VCVio/CryptoFoundations/GPVHashAndSign/GameRuns.lean: This new file, GameRuns.lean, is a 1252-line addition to the GPV Hash-and-Sign formal verification project. It defines the pinned game-run distributions realGameRun and progGameRun for the sign-then-hash hop, along with several normalizations that collapse the runtime bundle and drop preimage-record components, putting both runs on the same StateT QueryCache ProbComp random-oracle surface. The file also builds GPV-specific tape-consuming handler implementations (gpvRealImplTape and progGameRunImplTape), flag-instrumented versions of these tape handlers for the identical-until-bad coupling, and provides per-query splicing lemmas relating the tape signing steps to the signRunF gpvStepReal/gpvStepProg handlers. Finally, it includes a proof of the per-query off-bad agreement of the tape handlers under a PSF regularity condition (evalDist_gpvImplTape_run_sign_miss_eq).
• VCVio/CryptoFoundations/GPVHashAndSign/MinEntropy.lean: This new file MinEntropy.lean introduces the min-entropy analysis for the programmed-preimage experiment of the GPV Hash-and-Sign construction. It defines trapdoorGuessingProbability as the supremum over honest keys and targets of the maximal pointwise output probability of psf.trapdoorSample, corresponding to 2^(-H∞) for the sampler's min-entropy. It then proves the main bound programmedPreimageAdvantage_le_trapdoorGuessingProbability, showing that any programmed-preimage adversary's advantage is at most this guessing probability, and also provides the hypothesis form programmedPreimageAdvantage_le_of_probOutput_trapdoorSample_le, which directly bounds advantage by a uniform pointwise mass bound ε on the sampler at honest keys. These results are designed to supply the exact-match branch of GPVHashAndSign.euf_cma_collision_bound with a negligible term when instantiated with a concrete bound (e.g., from a discrete-Gaussian trapdoor sampler).
• VCVio/CryptoFoundations/GPVHashAndSign/SamplerTransport.lean: This new file (SamplerTransport.lean) introduces the adaptive sampler-transport accumulation for the GPV hash-and-sign scheme. It defines lemmas establishing that swapping the probabilistic trapdoor sampler while keeping the deterministic eval/isShort components fixed leaves certain operations unchanged: gpvVerifyRead_trapdoorSwap shows verification reads are identical, and gpvRealImplFlagFresh_run_inl_trapdoorSwap shows non-signing handler steps are invariant. The per-signing-step total-variation budget is bounded by tvDist_run_gpvRealImplFlagFresh_sign_le, and the adaptive run-level accumulation is proved in tvDist_run_simulateQ_gpvRealImplFlagFresh_trapdoorSwap_le. The main theorems are probOutput_realGameVerifyFresh_le_trapdoorSwap_add (per-key game hop), advantage_le_advantage_add_of_trapdoorSample_tvDist (one-sided EUF-CMA advantage accumulation), and abs_advantage_toReal_sub_le_of_trapdoorSample_tvDist (symmetric two-sided real-form bound). No sorry or admit are present.
• VCVio/CryptoFoundations/GPVHashAndSign/Security.lean: This new file Security.lean formalizes the security proof for the GPV Hash-and-Sign signature scheme, establishing several key lemmas and theorems. Specifically, it proves: (1) evalDist_map_run_simulateQ_eq_of_query_evalDist_map_eq — a distribution-level state-projection transport theorem for oracle simulations; (2) progGameRunImplCombinedTrapCount_freshSig_proj and map_run_progGameRunImplCombinedTrapCount_freshSig_proj — per-query and run-level distributional projections from the trap-count-augmented run to the fresh-signature run; (3) freshSig_winnerSlot_deferred_le_embed — a bound relating the freshness-confined winner-slot deferred-trapdoor functional to the per-target embedding win; (4) progGameRunImplCombinedTrapCount_signedSet_grows — monotonicity of the signed set; (5) progGameRunImplCombinedTrapCount_frozen — frozenness of programmed, unsigned keys; (6) progGameRunImplCombinedTrapCount_table_indep — table-independence of expectations; (7) progGameRunImplCombinedTrapCount_table_frozen_eq — frozen-table expectation factorization; (8) progGameRunImplCombinedTrapCount_table_defer — per-step deferral of a write-only trapdoor draw; (9) trap_freshSig_le_winnerSlot_deferred — the trap-side table-defer bound; and (10) reservoir_embed_commute_winner_floorFree — the floor-free per-slot front-loading deferred-sampling coupling.
• VCVio/CryptoFoundations/GPVHashAndSign/TapeFactorization.lean: This new file introduces the "front salt-tape factorization" for the GPV Hash-and-Sign security proof. It provides two key lemmas (evalDist_gpvRealImpl_eq_drawList_gpvRealImplTape and evalDist_progGameRunImplNoRec_eq_drawList_progGameRunImplTape) that rephrase the real and programmed game runs as a single front block of drawList ($ᵗ Salt) qSign signing salts followed by a tape-consuming simulation. It then builds the bridging theorems realGameRun_eq_drawList_gpvRealImplTape and progGameRun_eq_drawList_progGameRunImplTape to express the actual game definitions in this factored form. The file also defines tapeCheck (a salt-collision predicate on a list of salts), proves drawList_tapeCheck_eq_saltSeq (relating it to the saltSeq birthday process), and establishes probEvent_tapeCheck_drawList_le_collisionBound (a birthday bound for the tape check). To support the off-bad path agreement of the tape handlers, it provides gpvImplTapeFlag_h_agree_good (a universal h_agree_good hypothesis for the flag-instrumented tape handlers) together with helper lemmas evalDist_eval_domainSample_eq_uniform, gpvImplTape_run_unif_eq, gpvImplTape_run_read_hit_eq, and evalDist_gpvImplTape_run_read_miss_eq. The reduction from the factored games to the TV distance bound is provided by tvDist_drawList_bind_le. No sorry or admit are present.
• VCVio/CryptoFoundations/GPVHashAndSign/TrapCount.lean: This file introduces the counter-augmented trap run progGameRunImplCombinedTrapCount, which extends progGameRunImplCombinedTrap with a passive (idxTable, counter) instrument that records the programming index at each cache miss or signing step. It proves the instrument is distributionally passive (map_run_progGameRunImplCombinedTrapCount_proj) and that the preimage table and insertion-index table stay in lockstep (progGameRunImplCombinedTrapCount_idx_iff_table). It establishes counter bounds (progGameRunImplCombinedTrapCount_run_count_le) and index bounds (progGameRunImplCombinedTrapCount_idx_lt_count, progGameRunImplCombinedTrapCount_idx_lt_budget). It also defines the inline-fresh embed handler embedTrapFreshImpl and proves the GPV Step-2 front-loading equality evalDist_frontDraw_embedTrapImpl_eq_embedTrapFresh, which states that averaging embedTrapImpl over an external target draw equals the inline-fresh run. Finally, it introduces index-augmented versions embedTrapIdxImpl and embedTrapFreshIdxImpl with passive insertion-index tables and proves their projection lemmas (embedTrapIdxImpl_proj, map_run_embedTrapIdxImpl_proj, embedTrapFreshIdxImpl_proj).
• VCVio/CryptoFoundations/GPVHashAndSign/VerificationBridge.lean: This new file, VerificationBridge.lean, introduces the O1 data-processing bridge connecting the GPV hash-and-sign Step-1 bound to the post-processed verification game, the forger-queries-its-forgery-point predicate, and the programmed verify-game machinery. It adds the theorem gpv_realGameVerify_le_progGameVerify_add_collisionBound, which uses the data-processing inequality to transfer the total-variation distance bound from realGameRun/progGameRun to any verification post-processor. The theorem probOutput_unforgeableExp_eq_keygen_average peels the keygen average out of the GPV unforgeability experiment via withStateOracle_evalDist_liftM_bind. The lemma simulateQ_writerImpl_verify_fold folds the verification continuation into the adversary computation, and signedSet_eq_wasQueried identifies the WriterT signing log with the reconstructed signed-set for the per-key game-identification. The main reduction theorem gpv_advantage_le_progGameVerifyFreshAvg_add_collisionBound chains the keygen-averaging peel, the per-key reconstruction, and the real↔programmed coupling hop to bound the GPV EUF-CMA advantage by the keygen-averaged programmed freshness verify-Bool game plus collisionBound. The file defines the predicate ForgesQueriedPoint and provides the lemmas collisionFindingAdvantage_reduction_eq, isShort_of_mem_support_domainSample, run_combined_gpvVerifyRead_of_cache_hit, run_combined_verifyKont_of_cache_hit, combined_cache_forge_point_ne_none, progGameVerifyFresh_eq_probEvent_combined, reduction_collision_eq_probEvent_combined, distinct_implies_collision_pointwise, combinedTableSupport, combinedTableSupport_write_card_le, combinedTableSupport_run_card_le, combined_run_table_card_le, gpv_perKey_distinct_le_collision, probOutput_reservoirStep_win, probEvent_reservoirStep_miss, reservoirWinnerIndex, reservoirWinnerIndex_succ, tsum_reservoirStep_survival, probOutput_reservoirStep_ne, and probOutput_reservoirStep_eq, which establish the forger-queries-its-forgery-point property, the table-passive nature of verification reads on cache hits, the equivalence of game success to a combined run event, the collision-reduction success as a table event, the distinct-collision pointwise transfer, and the reservoir-sampling embedding probabilities. The file introduces no sorry or admit.

---

Last updated: 2026-07-13 12:53 UTC.

[alik-eth]

The disclosed hForge caveat is now discharged: pushed GPVHashAndSign/AppendQuery.lean (additive module) formalizing the append-forgery-query compiler and the all-adversaries corollary.

• appendForgeQuery adv — the compiled adversary that re-queries its own forgery point as a final ambient RO query.
• signHashQueryBound_appendForgeQuery — sign count unchanged, hash count qHash + 1.
• forgesQueriedPoint_appendForgeQuery — the compiled adversary satisfies ForgesQueriedPoint unconditionally.
• advantage_appendForgeQuery — the compiler is advantage-preserving (equality, not a bound): the appended query is re-issued by the verification read at the same point, so the lazy-caching random oracle absorbs it without affecting the output distribution, the signing log, or the freshness mask.
• euf_cma_split_bound_of_queryBound — the headline: the split GPV PFDH bound for any adversary, with only the query-bound hypothesis — no ForgesQueriedPoint — at the price of qHash ↦ qHash + 1 in the exact-match multiplier and the salt-collision bound.

All twelve new declarations kernel-check at [propext, Classical.choice, Quot.sound]; full CI library set green, lint clean. The "append one hash query" WLOG that was previously prose in the module docstring is now a theorem.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[alik-eth]

Pushed one more generic module: GPVHashAndSign/SamplerTransport.lean — the adaptive trapdoor-sampler-swap accumulation. For any two PSFs sharing eval/isShort whose trapdoor samplers are within per-call total-variation ε on honest keys, any adversary's advantage transports between the two schemes at cost qSign · ε (advantage_le_advantage_add_of_trapdoorSample_tvDist, plus the two-sided form). Proven sorry-free by charging the signing steps through the generic tvDist_simulateQ_run_le_queryBoundP_mul telescope; uniform/RO/verification steps are proven implementation-identical. This is the engine for discharging Falcon's transport hypothesis in #466. All declarations [propext, Classical.choice, Quot.sound].

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77