feat(Falcon): idealized-model EUF-CMA via GPV, down to NTRU-SIS (#188)

[alik-eth]

Closes #188.

Instantiates the generic GPV hash-and-sign EUF-CMA bounds (now PR #478) for Falcon, reducing forgery to the NTRU-PSF collision problem and onward to short NTRU-SIS kernel vectors.

Stacked on #478 — the generic GPV framework was extracted into its own PR per review. Until #478 lands, this PR's diff also shows those commits; once it merges, a rebase shrinks the diff to the Falcon layer (LatticeCrypto/Falcon/ + LatticeCrypto.lean).

Note on the issue's decl name: #188 tracks euf_cma_bound; no declaration ships under that literal name. The obligation is discharged by GPVHashAndSign.euf_cma_split_bound / euf_cma_collision_bound (#478) and their Falcon instantiations here.

Falcon layer (LatticeCrypto/Falcon/{Security,SISBridge,NonVacuity,Scheme}.lean)

• Falcon.euf_cma_security / euf_cma_security_bytes40 — EUF-CMA of the Falcon signature scheme reduced to ntruPSFCollisionProblem + the explicit programmed-preimage residual + the salt birthday bound (qSign + qHash)² / (2 · |Salt|) + a transport term samplerLoss. The GPV laws are carried on an ideal PSF sharing Falcon's eval/isShort; the concrete→ideal transport (hTransport) is assumed as a single hypothesis, the way MLWE/SIS hardness is assumed. Decomposing it into a per-call sampler-approximation bound with a proven adaptive accumulation is the intended refinement (the unused Rényi API scaffolding was dropped from this PR).
• NTRU-SIS bridge (SISBridge.lean): euf_cma_security_ntruSIS extends the reduction one hop further — a PSF collision (s₁,s₂) ≠ (s₁',s₂') with h·s₁ + s₂ = h·s₁' + s₂' yields a nonzero kernel vector of length² ≤ 4·betaSquared (ntruSISProblem_isValid_sub, via coefficientwise negacyclic-convolution arithmetic and centered-representative norm bounds). ntruSISProblemKeyed states the honest-key variant; the gap to uniform h is decisional NTRU, documented rather than assumed silently.
• collisionFindingAdvantage_eq_ntruPSF — definitional bridge: the GPV collision experiment is the NTRU-PSF collision search problem.
• Examples.FalconNonVacuity.falcon_eufcma_hyps_inhabited — the full hypothesis set of euf_cma_security witnessed jointly at a toy parameter set with a genuinely NTRU-valid key (fG − gF = q). Presented as a logical-consistency (inhabitance) witness only — no quantitative security content.
• Scope (documented in a dedicated module-docstring section): an idealized proof-level model — full (s₁,s₂) preimages, exact arithmetic, no cost model. The unfinished sorry-backed correctness cluster (sign, keyGenFromSeed, verify_sign_correct) is deleted; verification correctness routes through floating-point inverse-FFT rounding and is complementary work (see Falcon faithfulness & soundness remediation — concrete keygen, verify_sign_correct, verify bridge #471).

Verification

• lake build of the full CI library set at this tip on leanprover/lean4:v4.31.0: green, zero non-sorry warnings.
• #print axioms on all headline theorems (including euf_cma_security_ntruSIS and the six SIS-bridge declarations) and both consistency witnesses: [propext, Classical.choice, Quot.sound] — no sorryAx, no custom axioms.

Review follow-ups tracked

• hForge append-query WLOG compiler (GPV side, planned follow-up on feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds #478).
• hTransport decomposition into per-call sampler bounds.
• Ideal-Gaussian min-entropy bound for the exact-match term.

[github-actions]

🤖 PR Summary

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

Mathematical Formalization

• Falcon EUF‑CMA security proof (LatticeCrypto/Falcon/Security.lean):

  • Falcon.euf_cma_security reduces forgeability to NTRU‑PSF collision + programmed‑preimage residual + salt birthday bound + sampler transport term. The theorem is parameterized by an idealPSF sharing Falcon’s eval/isShort, and assumes correctness, regularity, never‑fail, and a transport hypothesis (hTransport). Derivation via GPVHashAndSign.euf_cma_split_bound.
  • collisionFindingAdvantage_eq_ntruPSF equates the GPV collision‑finding advantage with the NTRU‑PSF collision search problem.
  • Per‑call transport decomposition: samplerTransport, samplerTransport_one, euf_cma_security_of_samplerTransport, euf_cma_security_of_samplerTransport_queryBound.
  • Min‑entropy exact‑match term: idealSamplerGuessBound, euf_cma_collision_security (discharges the exact‑match residual under a per‑call guessing‑probability bound).

• NTRU‑SIS bridge (LatticeCrypto/Falcon/SISBridge.lean):

  • ntruSISProblem_isValid_sub: a PSF collision (s₁,s₂) ≠ (s₁',s₂') with h·s₁ + s₂ = h·s₁' + s₂' yields a nonzero kernel vector of length² ≤ 4·betaSquared.
  • ntruSISProblemKeyed: honest‑key variant (gap to uniform h is decisional NTRU, documented).
  • collisionToKernelAdv, advantage_le_ntruSISProblemKeyed, euf_cma_security_ntruSIS: end‑to‑end bound replacing collision term with keyed NTRU‑SIS advantage.

• Non‑vacuity witnesses (LatticeCrypto/Falcon/NonVacuity.lean):

  • falcon_eufcma_hyps_inhabited (and variants for decomposed transport / min‑entropy) – logical‑consistency witnesses for a toy degree‑one parameter set with a valid NTRU key.

Proof Completion (sorries removed)

• Deleted from LatticeCrypto/Falcon/Scheme.lean: keyGenFromSeed, sign, verify_sign_correct – all previously sorry‑backed. Removed SamplerQuality structure.
• No sorry or admit introduced anywhere in the Falcon layer or the GPV submodules. All headline theorems (euf_cma_security, euf_cma_security_ntruSIS, the six SIS‑bridge declarations, both consistency witnesses) are axiom‑free (#print axioms yields only [propext, Classical.choice, Quot.sound]).

Refactoring

• LatticeCrypto/Falcon/Scheme.lean: scope narrowed to key types, signAttempt, verify, and the GPV bridge; docstring updated. Concrete key generation and retry‑loop signer moved to LatticeCrypto.Falcon.Concrete.
• VCVio/CryptoFoundations/GPVHashAndSign.lean: refactored from a monolithic module with sorry‑filled proofs into an umbrella importing ≈15 submodules under GPVHashAndSign/. The submodules (e.g., Basic, CollisionTelescope, CombinedHandler, EmbedIndex, FlagHandlers, GameIdentification, TrapCount, Security, VerificationBridge, etc.) contain the complete GPV proof infrastructure with no sorry.

Infrastructure / CI

• lake build of the full CI library set on leanprover/lean4:v4.31.0 passes with zero non‑sorry warnings.

Documentation

• Module docstrings updated in Scheme.lean and GPVHashAndSign.lean to reflect the new scope and module layout.

Notes on the diff

This PR is stacked on #478 (generic GPV framework). The diff currently includes the GPV submodule additions; once #478 lands, a rebase will shrink the diff to the Falcon‑specific files (LatticeCrypto/Falcon/ + LatticeCrypto.lean). The overview above covers the Falcon‑layer changes; the GPV submodule changes are part of the stacked base and are not repeated here in detail.

---

Statistics

Metric	Count
📝 Files Changed	24
✅ Lines Added	14281
❌ Lines Removed	555

---

Lean Declarations

✏️ Removed: 22 declaration(s)

LatticeCrypto/Falcon/Scheme.lean (2)

• noncomputable def keyGenFromSeed (_seed : List Byte) : PublicKey p × SecretKey p
• noncomputable def sign (pk : PublicKey p) (sk : SecretKey p) (msg : List Byte) :

LatticeCrypto/Falcon/Security.lean (2)

• def HasUniformSamplerLoss (samplerLoss : ENNReal) : Prop
• theorem verify_sign_correct (pk : PublicKey p) (sk : SecretKey p)

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: 419 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 :

LatticeCrypto/Falcon/NonVacuity.lean (40)

• lemma toy_step_caches (ds : PublicKey toyP → ProbComp (Rq toyP.n × Rq toyP.n))
• noncomputable def toyAdv :
• noncomputable def toyAdv' :
• noncomputable def toyAdvQ :
• noncomputable def toyDomainSample (_pk : PublicKey toyP) : ProbComp (Rq toyP.n × Rq toyP.n)
• noncomputable def toyHr :
• noncomputable def toyIdealPSF :
• noncomputable def toyP : Params
• noncomputable def toyPk : PublicKey toyP
• noncomputable def toyPrims : Primitives toyP
• noncomputable def toySk : SecretKey toyP
• noncomputable def toyTree : FalconTree toyP.fftDepth
• theorem falcon_eufcma_hyps_inhabited :
• theorem falcon_eufcma_samplerTransport_hyps_inhabited :
• theorem intPolyConst_get_n1 (c : ℤ) : (intPolyConst (n
• theorem intPolyMul_const_const (a b : ℤ) :
• theorem intPolyMul_eq_pure (a b : IntPoly 1) :
• theorem negacyclicMulPure_get_n1 (a b : Poly ℤ 1) :
• theorem negacyclicMul_zero_left {n : ℕ} (h : Rq n) : negacyclicMul (0 : Rq n) h = 0
• theorem negacyclicMul_zero_right {n : ℕ} (a : Rq n) : negacyclicMul a (0 : Rq n) = 0
• theorem poly_sub_get_n1 (a b : Poly ℤ 1) : (a - b).get 0 = a.get 0 - b.get 0
• theorem schoolbook_eq_pure_n1 (f g : Poly ℤ 1) :
• theorem toRq_intPolyConst_zero : (IntPoly.toRq (intPolyConst (n
• theorem toy_ForgesQueriedPoint (ds : PublicKey toyP → ProbComp (Rq toyP.n × Rq toyP.n)) :
• theorem toy_advantage_bound :
• theorem toy_correctAt (pk : PublicKey toyP) (sk : SecretKey toyP) :
• theorem toy_euf_cma_collision_security :
• theorem toy_euf_cma_security_of_samplerTransport :
• theorem toy_eval_pair_zero (pk : PublicKey toyP) (c : Rq toyP.n) :
• theorem toy_hEval (pk : PublicKey toyP) (x : Rq toyP.n × Rq toyP.n) :
• theorem toy_hReg (pk : PublicKey toyP) (sk : SecretKey toyP) :
• theorem toy_hShort (x : Rq toyP.n × Rq toyP.n) :
• theorem toy_idealSamplerGuessBound :
• theorem toy_isShort (x : Rq toyP.n × Rq toyP.n) : toyIdealPSF.isShort x = true
• theorem toy_l2NormSq_le (s : Rq toyP.n) : LatticeCrypto.l2NormSq s ≤ 37748736
• theorem toy_neverFail (pk : PublicKey toyP) (sk : SecretKey toyP) (c : Rq toyP.n) :
• theorem toy_samplerTransport :
• theorem toy_signHashQueryBound (pk : PublicKey toyP) :
• theorem toy_trapdoorSample_probOutput_self (pk : PublicKey toyP) (sk : SecretKey toyP)
• theorem toy_validKeyPair : validKeyPair toyP toyPk toySk = true

LatticeCrypto/Falcon/SISBridge.lean (11)

• lemma centeredRepr_sub_natAbs_le {q : ℕ} [NeZero q] (x y : ZMod q) :
• lemma negacyclicConvCoeff_sub_left {R : Type*} [CommRing R] {n : ℕ}
• lemma negacyclicMul_coeff {n : ℕ} (f g : Rq n) (i : Fin (polyBackend n).degree) :
• lemma negacyclicMul_sub_left {n : ℕ} (f₁ f₂ g : Rq n) :
• lemma pairL2NormSq_sub_le {n : ℕ} (a₁ a₂ b₁ b₂ : Rq n) :
• lemma polyL2NormSq_sub_le {n : ℕ} (f g : Rq n) :
• noncomputable def collisionToKernelAdv [SampleableType (Rq p.n)]
• noncomputable def ntruSISProblemKeyed [SampleableType (Rq p.n)]
• theorem advantage_le_ntruSISProblemKeyed [SampleableType (Rq p.n)]
• theorem euf_cma_security_ntruSIS
• theorem ntruSISProblem_isValid_sub [SampleableType (Rq p.n)]

LatticeCrypto/Falcon/Security.lean (8)

• def idealSamplerGuessBound
• def samplerTransport
• theorem collisionFindingAdvantage_eq_ntruPSF
• theorem euf_cma_collision_security
• theorem euf_cma_security_of_samplerTransport_queryBound
• theorem euf_cma_security_of_samplerTransport
• theorem idealSamplerGuessBound_one
• theorem samplerTransport_one

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) :

…and 269 more not listed.

---

sorry Tracking

✅ Removed: 8 `sorry`(s)

LatticeCrypto/Falcon/Scheme.lean (2)

• noncomputable def keyGenFromSeed (_seed : List Byte) : PublicKey p × SecretKey p (L121)
• noncomputable def sign (pk : PublicKey p) (sk : SecretKey p) (msg : List Byte) : (L225)

LatticeCrypto/Falcon/Security.lean (2)

• theorem euf_cma_security (L321)
• theorem verify_sign_correct (pk : PublicKey p) (sk : SecretKey p) (L119)

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: The change adds an import of Examples.GPVNonVacuity. This makes the module Examples.GPVNonVacuity available for use, which likely contains formalization or proofs related to the non-vacuity of the GPV (Goldreich–Goldwasser–Micali) construction.
• Examples/GPVNonVacuity.lean: Adds Examples/GPVNonVacuity.lean, a new file that provides a concrete consistency (inhabitance) witness for the GPV hash-and-sign EUF‑CMA bounds (GPVHashAndSign.forgery_yields_collision_or_exact_match and its corollaries). It defines a canonical bijective PSF bijPSF over Bool with PK = SK = Unit, a trivial generable relation hr, and a query‑then‑forge adversary adv that makes exactly one random‑oracle query at its forgery point. The file proves bijPSF_correct (the PSF is correct), bijPSF_regularity (the PSF is regular, with domainSample = $ᵗ Bool), bijPSF_hForge (the adversary queries its forgery point, establishing ForgesQueriedPoint), and adv_signHashQueryBound (the adversary makes 0 signing and 1 random‑oracle query). These are combined in the theorem gpv188_hyps_inhabited, which asserts that all four side conditions are simultaneously satisfiable, ruling out vacuity of the conditional bounds. No sorry or admit appears in the file.
• LatticeCrypto.lean: Added imports for LatticeCrypto.Falcon.NonVacuity and LatticeCrypto.Falcon.SISBridge. These imports were added to the main import block, which suggests that the Falcon module now depends on the NonVacuity and SISBridge files, likely to use definitions or theorems from them (e.g., non-vacuity proofs or SIS-based security reductions).
• LatticeCrypto/Falcon/NonVacuity.lean: This new file provides logical consistency witnesses for the conditional theorem Falcon.euf_cma_security and its variants. It defines a trivial degree-one (n=1) toy parameter set toyP, a valid NTRU key pair (toyPk, toySk) satisfying validKeyPair, and an ideal preimage-sampleable function toyIdealPSF (with deterministic eval/isShort inherited from Falcon and a trapdoor sampler trapdoorSample pk sk c := pure (c, 0)). The file establishes the GPV laws (toy_correctAt, toy_hReg, toy_neverFail), the shared eval/isShort definitions (toy_hEval, toy_hShort), and a transport adversary toyAdv' (a no-query forger) satisfying ForgesQueriedPoint, signHashQueryBound, and an advantage bound. The main result falcon_eufcma_hyps_inhabited states that all hypotheses of Falcon.euf_cma_security are simultaneously satisfiable for this toy instance. The file also provides analogous witnesses for the decomposed samplerTransport and idealSamplerGuessBound frontiers (falcon_eufcma_samplerTransport_hyps_inhabited, toy_euf_cma_security_of_samplerTransport, toy_euf_cma_collision_security), demonstrating end-to-end applicability of the derived theorems at the toy instance. The file contains no sorry or admit.
• LatticeCrypto/Falcon/SISBridge.lean: This new file LatticeCrypto/Falcon/SISBridge.lean formalizes the reduction from Falcon's collision-finding problem (ntruPSFCollisionProblem) to the NTRU-SIS kernel-vector problem (ntruSISProblem). It introduces several supporting lemmas: centeredRepr_sub_natAbs_le (bounding the centered representative of a difference), polyL2NormSq_sub_le and pairL2NormSq_sub_le (norm inequalities for differences of ring elements), and negacyclicMul_sub_left (linearity of negacyclic multiplication). The main theorem ntruSISProblem_isValid_sub proves that the componentwise difference of a valid collision pair yields a valid NTRU-SIS solution. The file then defines ntruSISProblemKeyed (NTRU-SIS with honest key distribution), collisionToKernelAdv (adversary transform), and advantage_le_ntruSISProblemKeyed (advantage transfer). Finally, euf_cma_security_ntruSIS restates the EUF-CMA security bound with the collision term replaced by the keyed NTRU-SIS advantage. No sorry or admit are present.
• LatticeCrypto/Falcon/Scheme.lean: This commit refactors LatticeCrypto/Falcon/Scheme.lean by removing the keyGenFromSeed and sign definitions (both left as sorry) and their surrounding documentation, and relocating key generation and the fresh-salt retry-loop signer to LatticeCrypto.Falcon.Concrete. The module-level docstring is updated to reflect this narrower scope, now describing only key types and validity, the one-shot signing core signAttempt, and verification verify, alongside the GPV bridge via PreimageSampleableFunction. The docstring for signAttempt is also reworded to clarify that it isolates the one-shot trapdoor-sampling core and norm-check abort from the retry loop.
• LatticeCrypto/Falcon/Security.lean: This diff restructures Falcon's security proof by replacing a sorry-based correctness theorem (verify_sign_correct) and a SamplerQuality structure with an idealized GPV model. ntruSISProblem now targets 4·betaSquared (from betaSquared) to reflect collision differences, and ntruPSFCollisionProblem gains an explicit hr argument. A new theorem collisionFindingAdvantage_eq_ntruPSF equates GPV collision-finding advantage to NTRU‑PSF advantage under shared eval/isShort. The main euf_cma_security theorem is rewritten: it accepts an idealPSF with correctness, regularity, never-fail, and transport hypotheses (replacing hSamplerLoss and a different hQ) and derives its bound from GPVHashAndSign.euf_cma_split_bound and collisionFindingAdvantage_eq_ntruPSF. New per‑call transport machinery (samplerTransport, samplerTransport_one) and the theorems euf_cma_security_of_samplerTransport, euf_cma_security_of_samplerTransport_queryBound decompose the monolithic transport into an adaptive accumulation from total‑variation distance bounds. The min‑entropy section adds idealSamplerGuessBound and euf_cma_collision_security, which discharges the exact‑match term under a per‑call guessing‑probability bound, leaving NTRU‑PSF collision as the sole cryptographic residual. All versions of the bound now use GPVHashAndSign.collisionBound Salt qSign qHash (two arguments).
• VCVio.lean: The file VCVio.lean now imports fifteen new submodules of VCVio.CryptoFoundations.GPVHashAndSign, including Basic, CollisionTelescope, CombinedHandler, GameIdentification, Security, MinEntropy, SamplerTransport, TapeFactorization, TrapCount, VerificationBridge, AppendQuery, EmbedIndex, Factorization, FlagHandlers, and GameRuns. These imports make the definitions and theorems from those submodules available in the current file, likely to support further formalization of the GPV hash-and-sign scheme or its security analysis.
• VCVio/CryptoFoundations/GPVHashAndSign.lean: The file is refactored from a monolithic module containing all definitions, theorems, and partial proofs (with several sorry placeholders) into an umbrella module that imports and re‑exports a set of submodules under VCVio/CryptoFoundations/GPVHashAndSign/. The old definitions (PreimageSampleableFunction, GPVHashAndSign, reduction, programmedPreimageReduction, collisionBound, forgery_yields_collision, euf_cma_collision_bound, etc.) and their associated sorry‑filled proofs are no longer present in this file – they have been moved to the new submodules. The docstring is updated to describe the new module layout and to clarify that the formalized salt‑collision bound uses (qSign + qHash)² / (2 · |Salt|) (GPVHashAndSign.collisionBound) rather than the earlier qSign² / (2 · |Salt|). The copyright and authors list are extended to include Oleksandr Vovkotrub.
• VCVio/CryptoFoundations/GPVHashAndSign/AppendQuery.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This file adds `appendFo...bound on the adversary.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• VCVio/CryptoFoundations/GPVHashAndSign/Basic.lean: The new file GPVHashAndSign/Basic.lean introduces the preimage‑sampleable function (PSF) abstraction (PreimageSampleableFunction), its correctness (Correct, CorrectAt) and regularity (Regularity) properties, and the GPV hash‑and‑sign signature scheme (GPVHashAndSign) in the random‑oracle model. It also provides the scheme's runtime bundle (runtime), a structural query bound (signHashQueryBound), and the adversary interfaces and experiments for collision‑finding (CollisionAdversary, collisionFindingExp, collisionFindingAdvantage) and programmed‑preimage (ProgrammedPreimageAdversary, programmedPreimageExp, programmedPreimageAdvantage) that are used in the EUF‑CMA proof. No sorry or admit appear in the diff.
• VCVio/CryptoFoundations/GPVHashAndSign/CollisionTelescope.lean: This new file CollisionTelescope.lean adds the GPV Hash-and-Sign salt-collision telescope: a proof infrastructure for bounding the probability of a salt collision in the GPV FDH-with-salt signature scheme. It defines the reduction adversary (a CollisionAdversary that simulates the CMA experiment using sign-then-hash and returns a collision candidate), the birthday bound collisionBound and supporting lemmas (probEvent_mem_uniformSample, sum_range_div_card_le_collisionBound, probEvent_salt_collision_le_collisionBound), and the salt-averaged collision telescope built from the saltSeq process. The file also introduces the salt-inclusive signRunF process (a flag-carrying sequenced signing process with explicit salt draws) and establishes the identical-until-bad coupling theorems signRunF_tvDist_le_saltSeq and signRunF_tvDist_le_collisionBound, which bound the total-variation distance between real and programmed signing runs by the salt-collision probability. The file adds tsum_probOutput_uniformSample_ite (a tsum identity for uniform draws with an indicator weight), probEvent_saltSeq_succ (the exact one-step recursion of the salt-collision probability), and tvDist_bind_le_of_forall_le (a uniform per-fibre TV bound for a shared base). No sorry or admit are present.
• VCVio/CryptoFoundations/GPVHashAndSign/CombinedHandler.lean: This new file (1103 lines) introduces the combined programmed-game and collision-reduction handler for the GPV Hash-and-Sign proof in VCVio/CryptoFoundations/GPVHashAndSign/. It defines progGameRunImplCombined, a single oracle handler that threads both the programmed freshness-game state ((cache × signedSet) × flag) and the collision reduction's hidden preimage table ((Salt × M) → Option Domain) in lockstep, drawing each short preimage s ← domainSample pk once and updating all components identically. The file proves two projection lemmas (map_run_progGameRunImplCombined_proj_table, map_run_progGameRunImplCombined_proj_reduction) showing that dropping the table recovers the existing progGameRunImplNoRecFlagFresh handler and dropping the signed-set and flag recovers reductionImpl. It also defines a "trapdoor-recording" sibling handler progGameRunImplCombinedTrap which draws a uniform image v ← $ᵗ Range and records psf.trapdoorSample pk sk v instead of the forward-sampled preimage, and proves evalDist_run_progGameRunImplCombinedTrap_eq (using per-step lemma evalDist_progGameRunImplCombined_step_eq_trap and the distributional simulation engine evalDist_simulateQ_run_congr) that the two handlers produce identical output distributions under GPV regularity, establishing the write-only-table deferral that re-expresses the recorded preimage as a trapdoor preimage of the cached image. Finally, the file defines and proves preservation of three invariants (combinedCacheTableInv, combinedCacheImpliesTableInv, combinedTableInDomainInv) throughout the combined simulation via progGameRunImplCombined_run_inv, progGameRunImplCombined_run_cacheImpliesTable, and the partially defined combinedTableInDomainInv — the first two are stated in full, while the third is only declared (the lemma statements are not yet provided).
• VCVio/CryptoFoundations/GPVHashAndSign/EmbedIndex.lean: This new file introduces signed‑set‑augmented index‑embed handlers embedTrapIdxSigImpl and embedTrapFreshIdxSigImpl (counterparts of the existing embedTrapIdxImpl and embedTrapFreshIdxImpl) that thread a passive signed‑set (Finset M) through the state. It provides projection lemmas (embedTrapIdxSigImpl_proj, map_run_embedTrapIdxSigImpl_proj, and their fresh‑idx analogues) showing that dropping the signed set recovers the original handlers. The key lemmas embedTrapIdxSigImpl_fresh_idx_cache_eq (and its general form) establish that on a key whose message was never signed, a recorded insertion index of j forces the cached image to be the embedded target y — this is the load‑bearing freshness recovery for GPV Step‑2. The file also proves the front‑loading lift (evalDist_frontDraw_embedTrapIdxSigImpl_eq_embedTrapFreshSigImpl), the expected‑functional corollary (tsum_probOutput_embedTrapFreshIdxSig_mul_eq_frontDraw), and the trapdoor‑table support invariant progGameRunImplCombinedTrapCount_table_support.
• VCVio/CryptoFoundations/GPVHashAndSign/Factorization.lean: This new file Factorisation.lean introduces the adaptive-to-signRunF factorisation for the GPV hash-and-sign scheme. It defines the predicate AdaptiveFactorizesSignRunF asserting that two game runs (real and programmed) can be presented as fixed‑step signRunF runs, and proves factorized_advantage_le_collisionBound that under this predicate the total‑variation distance between the runs is bounded by the collision bound. Concrete per‑step handlers gpvStepReal and gpvStepProg are given for the GPV signing oracle’s cache‑miss and programmed branches, together with theorems gpvStepReal_neverFail (trapdoor sampler totality implies never‑fail), gpvStep_agree (distributional agreement under PSF regularity), evalDist_gpvSignBody_run_eq_gpvStepReal, and evalDist_gpvSignBody_run_eq_gpvStepProg (exact recasting of each signing body as a signRunF step). No sorry or admit appears in the file.
• VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean: This new file introduces flag-instrumented versions of the original inline-salt GPV real and programmed handlers (gpvRealImplFlag, progGameRunImplNoRecFlag) that thread a collision‑flag through the state, and proves the identical‑until‑bad reduction gpv_tvDist_orig_run_le_probEvent_flag bounding the total‑variation distance between the two original game runs by the run‑level flag probability. It establishes the universal off‑bad per‑query agreement gpvImplFlag_h_agree_good and the cardinality‑telescope bound gpv_orig_flag_le_collisionBound that charges each inline signing salt against the running cache slice, yielding the collisionBound without upfront‑tape re‑interleaving. The file then extends both handlers with a passive Finset M signed‑set (gpvRealImplFlagFresh, progGameRunImplNoRecFlagFresh) and proves gpv_tvDist_orig_verify_le_collisionBound that the verify‑Bool coupling stays within the same collision bound because the verification continuation issues no signing queries. No sorry or admit appear in the code.
• VCVio/CryptoFoundations/GPVHashAndSign/GameIdentification.lean: This new file establishes game-identification results for the GPV hash-and-sign scheme, providing the cross-monad reconstruction of the WriterT signing log as a signed set (Finset M) via lemmas such as gpvOuter_writerTMapBase_implW, flattenAppendLog_proj_gpvRealImplFresh, and map_simulateQ_gpvOuter_writerLog_eq_gpvRealImplFresh. It defines verify-Bool games on the freshness-tracking vehicle (gpvVerifyRead, realGameVerifyFresh, progGameVerifyFresh) and proves gpv_realGameVerifyFresh_le_progGameVerifyFresh_add_collisionBound bounding the real game probability by the programmed one plus a collision bound. The file supplies a state-threading bridge from the GPV runtime to the bare random oracle (runtime_evalDist_liftComp), and presents U2 (sign-then-hash ≡ real) total-variation bounds: the up-to-bad core tvDist_runtime_real_programmed_le_bad, its collision-bound package tvDist_runtime_real_programmed_le_collisionBound, and a salt-inclusive restatement tvDist_runtime_real_programmed_le_collisionBound_saltInclusive that avoids the unsound fire-on-miss flag. Finally, gpv_tvDist_real_programmed_le_collisionBound chains the original-run flag coupling to bound the TV distance between real and programmed GPV game runs by (collisionBound Salt qSign qHash).toReal, wiring Step 1 to the headline bounds.
• VCVio/CryptoFoundations/GPVHashAndSign/GameRuns.lean: This new file, GameRuns.lean, defines the core game runs for the GPV hash-and-sign signature scheme's sign-then-hash hop, along with tape-based and flag-instrumented handler stacks required for the formal coupling argument. It introduces two key distributions: realGameRun, which models the real EUF-CMA game under the lazy random oracle and real signing oracle, and progGameRun, which models the programmed (simulator) sign-then-hash game under a forward-sampled random oracle. The file provides structural normalizations (e.g., realGameRun_eq_simulateQ_run, realGameRun_eq_withStateOracle_implNoLog, progGameRun_eq_run'_implNoRec, realGameRun_eq_run'_implReal) that collapse the runtime indirection and discard the preimage-record component, putting both game runs on the same StateT QueryCache ProbComp surface. It then constructs tape-consuming handlers (gpvRealImplTape, progGameRunImplTape) that draw salts from a pre-drawn tape rather than inline, along with per-query unfolding lemmas (e.g., gpvRealImplTape_run_sign_cons, progGameRunImplTape_run_sign_cons). The file also introduces saltKeyed, the per-step collision predicate, and flag-instrumented handlers (gpvRealImplTapeFlag, progGameRunImplTapeFlag) that thread a collision flag through the state, with lemmas establishing flag projection (gpvRealImplTapeFlag_proj_fst, map_run_gpvRealImplTapeFlag_eq) and bad-monotonicity (gpvRealImplTapeFlag_bad_mono) that the framework identical-until-bad coupling (tvDist_simulateQ_run_le_probEvent_output_bad) consumes. A theorem evalDist_gpvImplTape_run_sign_miss_eq proves per-query off-bad agreement of the two tape signing steps under the PSF regularity condition hreg.
• VCVio/CryptoFoundations/GPVHashAndSign/MinEntropy.lean: This new file MinEntropy.lean defines the guessing probability of a trapdoor sampler and proves two generic bounds linking it to the advantage in the programmed-preimage experiment from GPVHashAndSign. The noncomputable definition trapdoorGuessingProbability takes the supremum over honest keys and all targets of the largest pointwise output mass of psf.trapdoorSample. The theorem programmedPreimageAdvantage_le_trapdoorGuessingProbability shows that any adversary's chance of exactly reproducing the hidden preimage is at most this guessing probability. The second theorem programmedPreimageAdvantage_le_of_probOutput_trapdoorSample_le provides a hypothesis form of the bound: if the sampler's pointwise masses at honest keys are uniformly bounded by some ε, then the adversary's advantage is at most ε; this is the shape consumed by the exact-match hypothesis of euf_cma_collision_bound.
• VCVio/CryptoFoundations/GPVHashAndSign/SamplerTransport.lean: The file SamplerTransport.lean adds the adaptive sampler-transport accumulation for GPV Hash-and-Sign. It introduces lemmas gpvVerifyRead_trapdoorSwap, gpvRealImplFlagFresh_run_inl_trapdoorSwap, and tvDist_run_gpvRealImplFlagFresh_sign_le that establish per-step invariance and total-variation bounds under a trapdoor-sampler swap. The main theorems are tvDist_run_simulateQ_gpvRealImplFlagFresh_trapdoorSwap_le (adaptive run-level accumulation for any computation with ≤ qSign signing queries), probOutput_realGameVerifyFresh_le_trapdoorSwap_add (per-key game hop bound), advantage_le_advantage_add_of_trapdoorSample_tvDist (one-sided EUF-CMA advantage accumulation), and abs_advantage_toReal_sub_le_of_trapdoorSample_tvDist (two-sided real-form bound). These results show that keeping deterministic eval/isShort fixed, swapping the trapdoor sampler costs at most qSign·ε in advantage whenever the two samplers are within total-variation distance ε per call, which is essential for relating concrete and ideal samplers in security proofs.
• VCVio/CryptoFoundations/GPVHashAndSign/Security.lean: This new file adds the core security‑bounds lemmas for the GPV Hash‑and‑Sign scheme. It defines a series of distributional projections and deferral lemmas that relate the trap‑count‑augmented game run to the fresh‑signature and embedded‑index runs: evalDist_map_run_simulateQ_eq_of_query_evalDist_map_eq (state projection at distribution level), progGameRunImplCombinedTrapCount_freshSig_proj and its run‑level counterpart map_run_progGameRunImplCombinedTrapCount_freshSig_proj (trap‑count to fresh‑sig projection), freshSig_winnerSlot_deferred_le_embed (step‑2 embed‑side reduction), and a chain of lemmas about the trap‑count run — progGameRunImplCombinedTrapCount_signedSet_grows (signed‑set monotonicity), progGameRunImplCombinedTrapCount_frozen (frozen cache/table for programmed unsigned keys), progGameRunImplCombinedTrapCount_table_indep (table‑independence of expectations), progGameRunImplCombinedTrapCount_table_frozen_eq (frozen‑table expectation), progGameRunImplCombinedTrapCount_table_defer (deferral of the write‑only trapdoor draw), and trap_freshSig_le_winnerSlot_deferred (trap‑side table‑defer bound). The file culminates in the floor‑free per‑slot coupling reservoir_embed_commute_winner_floorFree, establishing the deferred‑sampling content needed for the EUF‑CMA security bound.
• VCVio/CryptoFoundations/GPVHashAndSign/TapeFactorization.lean: Adds the file VCVio/CryptoFoundations/GPVHashAndSign/TapeFactorization.lean, which formalizes the front salt-tape factorization of the real and programmed game runs for the GPV hash-and-sign scheme, enabling a direct derivation of the Step‑1 total-variation bound. It introduces the lemmas drawList_salt_succ and the core theorems evalDist_gpvSignStep_commute_real, evalDist_gpvRealImpl_eq_drawList_gpvRealImplTape, and their programmed duals evalDist_gpvSignStep_commute_prog, evalDist_progGameRunImplNoRec_eq_drawList_progGameRunImplTape, which show that each game run distributes as a single front drawList ($ᵗ Salt) qSign of signing salts followed by a tape‑consuming run (gpvRealImplTape / progGameRunImplTape). The pinned bridge theorems realGameRun_eq_drawList_gpvRealImplTape and progGameRun_eq_drawList_progGameRunImplTape connect the actual game runs to this front‑tape form. The file then derives the bound gpv_tvDist_real_programmed_le_collisionBound by defining the collision check tapeCheck, proving drawList_tapeCheck_eq_saltSeq and probEvent_tapeCheck_drawList_le_collisionBound, and using the data‑processing lemma tvDist_drawList_bind_le. Finally, it establishes the off‑bad per‑query agreement lemmas (gpvImplTape_run_unif_eq, gpvImplTape_run_read_hit_eq, evalDist_gpvImplTape_run_read_miss_eq) and the universal h_agree_good hypothesis gpvImplTapeFlag_h_agree_good needed for the flag‑instrumented identical‑until‑bad coupling.
• VCVio/CryptoFoundations/GPVHashAndSign/TrapCount.lean: This new file (TrapCount.lean) introduces the counter-augmented trap run (N5) with a passive insertion-index table and running counter, and develops the core tools for the GPV Step-2 trap-mass index partition. It defines the augmented handler progGameRunImplCombinedTrapCount, proves its passive projection back to the untagged run (map_run_progGameRunImplCombinedTrapCount_proj), the lockstep domain invariant (progGameRunImplCombinedTrapCount_idx_iff_table), and bounds on the counter and recorded indices (progGameRunImplCombinedTrapCount_run_count_le, progGameRunImplCombinedTrapCount_idx_lt_count, progGameRunImplCombinedTrapCount_idx_lt_budget). The file also defines the inline-fresh embed handler embedTrapFreshImpl, the index-augmented embed handlers embedTrapIdxImpl and embedTrapFreshIdxImpl, and proves the front-loading lemma evalDist_frontDraw_embedTrapImpl_eq_embedTrapFresh (equating the externally-averaged trap-sibling embed run with the inline-fresh run) along with per-step independence and post-winner coincidence lemmas (embedTrapImpl_run_step_indep_of_target, embedTrapImpl_frontDraw_commute, evalDist_run_embedTrapImpl_eq_embedTrapFresh_of_lt). No sorry or admit are present.
• VCVio/CryptoFoundations/GPVHashAndSign/VerificationBridge.lean: Added the new file VerificationBridge.lean (1399 lines) which formalizes the O1 data-processing bridge for the GPV Hash-and-Sign security proof. It introduces the theorem gpv_realGameVerify_le_progGameVerify_add_collisionBound transferring the collision-bound TV-distance bound from Step‑1 through any verification post‑processor, the keygen‑averaging probOutput_unforgeableExp_eq_keygen_average and signedSet_eq_wasQueried lemmas that identify the per‑key WriterT‑log unforgeability experiment with the freshness verify‑Bool game, and the final bound gpv_advantage_le_progGameVerifyFreshAvg_add_collisionBound. It also defines the ForgesQueriedPoint predicate, provides lemmas for cache‑hit verification (run_combined_gpvVerifyRead_of_cache_hit, run_combined_verifyKont_of_cache_hit), establishes the table‑size bound combined_run_table_card_le, and proves the per‑key distinct‑collision transfer gpv_perKey_distinct_le_collision. Additionally, it introduces the pure reservoir‑winner‑index process reservoirWinnerIndex and its per‑step probability lemmas (probOutput_reservoirStep_win, probEvent_reservoirStep_miss, probOutput_reservoirStep_eq, probOutput_reservoirStep_ne).

---

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

[alik-eth]

Rebased onto main now that #465 is merged — the diff is down to this PR's own commits. The file split requested above is in e5a8fd0e (now 9d0f7dfe tip after rebase): twelve phase modules under GPVHashAndSign/ with the original module path kept as an umbrella, all names and consumers unchanged, full CI set green locally.

[alexanderlhicks]

I have a local branch with some Flacon stuff on it, let me check what progress I'd made and whether there's anything complementary.

[alik-eth]

@alexanderlhicks Happy to coordinate — here's a quick map to make diffing your branch easy.

What this PR covers: the generic GPV/PFDH EUF-CMA bounds (GPVHashAndSign.euf_cma_split_bound / euf_cma_collision_bound, sorry-free) and the Falcon instantiation Falcon.euf_cma_security — a conditional reduction terminating at ntruPSFCollisionProblem (two distinct short preimages with equal image), plus joint non-vacuity witnesses for both hypothesis sets. Heads-up if your branch touches the old GPVHashAndSign.lean monolith: it was just split into twelve modules under VCVio/CryptoFoundations/GPVHashAndSign/ (the old module path remains as an umbrella, so imports and fully-qualified names are unchanged — conflicts would be textual only).

Deliberately out of scope here — i.e. the complementary slots:

• the ntruPSFCollisionProblem → ntruSISProblem kernel-vector bridge (x ≠ x' ↦ nonzero x − x' with ‖·‖₂² ≤ 4·betaSquared); ntruSISProblem ships as a documented dormant target, so this is small and self-contained if you have it;
• signing/keygen correctness (verify_sign_correct and the retry-loop signer) — removed here as unfinished; it routes through the floating-point inverse-FFT rounding (FPRBridge/ApproxArith);
• discharging the hTransport hypothesis via SamplerQuality/renyiDiv (the [FGdG+25]/[Jia+26] Rényi finite-precision analysis — the structure is in Security.lean, currently unconsumed);
• NTRU key generation (Concrete/NTRUSolver.lean still carries sorries on main).

Anything of yours in those slots composes with this PR rather than colliding. If you did touch the same files, happy to coordinate a rebase order.

[quangvdao]

Thank you for the substantial work here. The generic GPV game-hopping development is valuable, sorry-free, and much easier to review after the split into phase modules. I am requesting changes because the Falcon-facing theorem currently claims more than its assumptions establish. I do not expect this PR to prove security of every concrete Falcon implementation detail (compression, floating point, exact sampler implementation, etc.). A meaningful theorem for a reasonably faithful idealized Falcon model—exact real arithmetic and an ideal Gaussian sampler are fine—is a good target.

The main changes I need are:

1. State the scope as an idealized Falcon/GPV model. falconSignatureAlg is currently the generic GPVHashAndSign scheme with the full (s₁,s₂) preimage, rather than the concrete Falcon.Signature/sign/verify path. This can still be a reasonable abstraction, but the theorem and documentation need to say precisely which Falcon features are modeled and which are idealized. Concrete encoding/compression and floating-point implementation security are not blockers for this PR.

2. Replace hTransport with materially weaker assumptions and prove the adaptive composition. As written, hTransport assumes the central concrete/approximate-sampler-to-ideal-adversary step wholesale: it directly supplies an ideal adversary with the desired advantage inequality, queried-point property, and query bound. The declared SamplerQuality/Rényi infrastructure is not used. Please formulate a local sampler approximation hypothesis (or another appropriately weak per-key/per-call condition) and prove how it accumulates across adaptive signing queries and retries. If the Rényi API is not the right route, remove it from this PR rather than presenting it as the justification.

3. Finish or accurately expose the two remaining cryptographic residuals. The current result stops at ntruPSFCollisionProblem, which is the GPV collision predicate repackaged as a problem, while the standard algebraic NTRU-SIS/kernel-vector bridge is not established. The exact-match/programmed-preimage term is also left unbounded. Please either:

   • prove the collision-to-standard-NTRU relation and an appropriate min-entropy/regularity bound for the exact-match term; or
   • export a deliberately intermediate theorem whose name and documentation expose both residual assumptions without calling it Falcon security “down to NTRU.”

   The latter is acceptable if it gives us a clean, meaningful staging point. The important thing is that the assumptions be strictly weaker than the conclusion we want, rather than restatements of the hard reduction steps.

4. Formalize the queried-forgery WLOG step. ForgesQueriedPoint currently restricts every supported adversary output, including losing outputs. Please implement the standard transformation that appends the final RO query and account for the extra query, or clearly keep the generic theorem restricted and provide the unrestricted corollary through that transformation.

5. Reframe the non-vacuity example. The degree-one, unit-salt, samplerLoss = 1 witness proves logical inhabitance of the hypothesis type, not meaningful Falcon security. Please label it explicitly as a consistency/inhabitance witness and avoid quantitative “non-vacuity” language.

6. Small correctness/maintenance items. The prose mentions a qSign²/(2|Salt|) collision term while the theorem uses (qSign+qHash)²/(2|Salt|); please reconcile this. Some generic WriterT/state-projection and query-bound lemmas should eventually live below the GPV namespace, though that extraction can be a follow-up if moving them now creates unnecessary proof churn.

There is also no formal PPT/cost preservation yet. Please mention this limitation briefly rather than trying to solve it here. #460 is dtumad's ongoing work toward the machine/PPT infrastructure; until that lands, reviewers should manually check that the constructed reductions are plausibly efficient and do not use exhaustive/noncomputable steps in the cryptographic path.

Finally, #477 is already merged, so please update this branch to current main and rerun CI.

My preferred landing shape is: first the generic GPV theorem with its exact restrictions; then a carefully named idealized Falcon instantiation with the weakest assumptions we can reasonably achieve. Concrete implementation fidelity can remain future work.

[alik-eth]

@quangvdao Thank you for the careful review — itemized response:

1. Idealized-model scope: agreed; documenting now that falconSignatureAlg is the abstract GPV scheme over the full (s₁,s₂) preimage with an ideal sampler and exact arithmetic, with an explicit list of what is modeled vs. idealized.
2. hTransport decomposition: agreed this is the substantive gap. Plan: a local per-call sampler-approximation hypothesis with a proven accumulation across adaptive signing queries and retries, replacing the wholesale assumption. The unused SamplerQuality/Rényi declarations come out of this PR until they are actually consumed. This is the main remaining campaign (est. multi-week) and I'd sequence it after item 4.
3. Residuals: (a) pushing LatticeCrypto/Falcon/SISBridge.lean — the collision→kernel-vector translation is now proven: ntruSISProblem_isValid_sub (witness level: nonzero from distinctness, kernel from linearity, 4·betaSquared from the centered-representative bound), ntruSISProblemKeyed + advantage_le_ntruSISProblemKeyed (advantage transfer at the honest key distribution), and euf_cma_security_ntruSIS. The residual honest-key↔uniform-challenge distance is documented as exactly a decisional-NTRU assumption — the deliberately-staged intermediate you describe. (b) Taking the honest-naming route now; an ideal-Gaussian min-entropy bound for the exact-match term as follow-up.
4. Queried-forgery WLOG: in progress — design done (the generic theorem keeps its restriction; an unrestricted corollary goes through the append-final-RO-query transform with qHash + 1 accounting). Est. 1–2 weeks.
5. Witness reframing: agreed — relabeling as consistency/inhabitance witnesses, removing quantitative language.
6. Docstring qSign² → (qSign+qHash)² reconciliation, PPT-limitation note, and the 4.31 rebase: all in the next push.

Proposal on landing shape, per your preference: extract the generic GPV development (the GPVHashAndSign/ modules + its hypothesis-witness example) into its own PR for prompt landing, and let this PR become the idealized-Falcon instantiation stacked on it, carrying items 2/3b/4. If that works for you I'll do the split with the next push.

[quangvdao]

sounds good please do the split. more pre each with self contained slice for review is better

[alik-eth]

Will do — extracting the generic GPV development (the GPVHashAndSign/ modules + the hypothesis-consistency example) into its own self-contained PR, with this one rebased on top carrying the idealized-Falcon layer. Scope/witness/docstring items from the review are already staged and will land with the split.

[alik-eth]

Split executed as promised: the generic GPV framework is now #478 (self-contained, builds standalone, headlines kernel-checked axiom-clean), and this PR is rebased on top of it carrying only the idealized-Falcon layer — retitled and body rewritten accordingly. Until #478 merges, the diff here still shows the GPV commits; it shrinks to LatticeCrypto/Falcon/ after a rebase once it lands.

Also addressed in this round, per the review:

• Scope section added to Falcon/Security.lean ("an idealized Falcon/GPV model": full (s₁,s₂) preimages, exact arithmetic, hTransport as a single assumed hypothesis, no cost model).
• Unused Rényi API dropped (SamplerQuality/HasUniformSamplerLoss); the hTransport docstring now states the per-call decomposition as intended refinement rather than pointing at dead scaffolding.
• Witnesses reframed as logical-consistency (inhabitance) witnesses only — the docstrings now say explicitly they carry no quantitative security content.
• Birthday bound documented uniformly as (qSign + qHash)² / (2 · |Salt|).
• Toolchain: branch adapted to Lean v4.31.0, full CI set green, zero non-sorry warnings, all headline axioms re-verified.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[alik-eth]

Review point 4 (hForge WLOG) is closed on the base branch: #478 now contains the append-forgery-query compiler and the all-adversaries corollary euf_cma_split_bound_of_queryBound (no ForgesQueriedPoint hypothesis; details in the #478 comment). This branch is rebased on top — the Falcon layer is unchanged.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[alik-eth]

Review point 2 (hTransport decomposition) is done — the "intended refinement" promised in the docstring is now formalized, sorry-free:

• samplerTransport ε_step — the per-call bound: on honestly generated keys, the concrete and ideal trapdoor samplers are within total-variation ε_step at every challenge. Named, inspectable, satisfiable (samplerTransport_one proves the ε_step = 1 witness); its concrete discharge routes through the IEEE/opaque-float layer and is documented as such, per the FPRBridge scope.
• The adaptive accumulation is proven, not assumed (in feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds #478's new SamplerTransport module): swapping the sampler across the whole EUF-CMA experiment costs qSign · ε_step, by charging exactly the signing steps of the game's simulateQ seam.
• Falcon.euf_cma_security_of_samplerTransport — the original theorem's frontier with hTransport replaced by the per-call bound; samplerLoss becomes the derived qSign · ε_step.
• Falcon.euf_cma_security_of_samplerTransport_queryBound — the same via feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds #478's append-query compiler, dropping ForgesQueriedPoint entirely: the Falcon frontier is now honest-key correctness/regularity/never-fail, a query bound, and the named per-call sampler idealization, at the usual qHash + 1 accounting.
• The toy witness now inhabits the full decomposed frontier end-to-end (toy_euf_cma_security_of_samplerTransport), consistency-only framing as before.

Honest accounting note (in the docstrings): the TV-additive qSign · ε_step bound is looser than the multiplicative Rényi accumulation of [FGdG+25] for large qSign — this is the Rényi term read at total-variation distance. The original euf_cma_security with the abstract transport hypothesis remains available and unchanged.

All new declarations [propext, Classical.choice, Quot.sound]; full CI set green.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[alik-eth]

Review point 3(b) — the exact-match/min-entropy residual — is closed (the 3(a) NTRU-SIS bridge landed earlier via SISBridge.lean):

• Generic (feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds #478, new GPVHashAndSign/MinEntropy.lean): programmedPreimageAdvantage ≤ trapdoorGuessingProbability — any programmed-preimage adversary is bounded by the trapdoor sampler's pointwise-maximum mass over honest keys and challenges (the guessing probability 2^(−H∞)). This is tight: the game's challenge is challenger-drawn uniform and the bound is met with equality by an argmax-guessing adversary.
• Falcon: idealSamplerGuessBound εpp — the named per-call min-entropy assumption (a genuine distributional property of the ideal sampler, strictly weaker than the discharged conclusion, per the review's criterion), with the trivial witness proven and the literature value documented (GPV08 Lemma 2.10: 2^(−H∞) of the coset Gaussian, negligible at Falcon parameters). Composed as Falcon.euf_cma_collision_security on the strongest frontier — the collision-only bound SIS + (qSign + qHash + 1)·εpp + birthday + qSign·ε_step, with no ForgesQueriedPoint, decomposed transport, and the exact-match existential collapsed away.
• Recon outcome disclosed: the current DiscreteGaussian module has no pointwise-mass upper bound, so the concrete numeric εpp awaits that theory; the two missing lemmas are specified precisely in the docstring rather than assumed silently.
• The toy witness inhabits the full corollary frontier end-to-end; its deterministic sampler makes εpp = 1 exactly tight there (zero min-entropy), which the docstring notes as the honest degenerate case.

With this, every item from the review is addressed: 1 (headline soundness via the split bound), 2 (transport decomposed), 3(a) (SIS bridge), 3(b) (this), 4 (hForge WLOG formalized). All new declarations [propext, Classical.choice, Quot.sound]; full CI set green.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77