Falcon faithfulness & soundness remediation — concrete keygen, verify_sign_correct, verify bridge

[alexanderlhicks]

Draft — opened for visibility/coordination, not for merge yet. cc @alik-eth (#466). This is the complementary half of the Falcon work: where #466 proves EUF-CMA via the abstract GPV → NTRU-collision route and deletes the sorry-backed correctness cluster (sign / keyGenFromSeed / verify_sign_correct), this branch builds out and proves that concrete correctness layer and audits byte-level faithfulness. The two are largely orthogonal and should inform each other — flagging early so we don't diverge or duplicate.

Canonical working doc: docs/agents/falcon-review.md (session log + findings). Paired re-runnable adversarial-review harness: scripts/falcon_review.mjs.

Scope & baselines

Three baselines judged separately (no single authoritative spec): Falcon v1.2, FN-DSA / FIPS 206, Falcon+ / c-fn-dsa. The repo targets c-fn-dsa / FN-DSA (FFI uses FNDSA_HASH_ID_RAW); divergences from v1.2 (pk-bound hash, fresh salt per retry, L2-only) are intended and documented (matrix M1–M9 in the doc).

Proven (standard-axioms-only: propext, Classical.choice, Quot.sound)

• verify_sign_correct (Security.lean) — a non-aborting signature always verifies, conditional only on the abstract h_laws.compress_decompress law (not the concrete codec).
• toRq_rqToIntPolyCentered = id (F8, Scheme.lean).
• Verify bridge concrete_verify_eq_verify (Concrete/FPRBridge.lean) — the byte-level verifier provably equals the spec verifier with no semantic hypotheses (B6 U32-kernel equalities + both codec round-trips sigDecode/pkDecode discharged inline; remaining side-conditions are purely structural/numeric).
• sign implemented as a fuel-bounded Option rejection loop (Scheme.lean).
• B9/ENC-3 fix: decompress rejects non-canonical-length signatures (over-length malleability), the one genuine wire bug found.
• KG-quickwin: NTRUSolver now uses the real Concrete/FXR.lean + PolyBigInt.lean (deleted 9 stub sorrys); check_ortho_norm is sorry-free and executable.

Open (WIP — why this is a draft)

• keyGenFromSeed (Scheme.lean) — sorry.
• NTRU solver ascent: solve_NTRU_intermediate / solve_NTRU_depth0 — sorry. A full port of c-fn-dsa solve_NTRU_depth0 was written but fails end-to-end validation (reverted to sorry; implementation + diagnostics preserved in docs/agents/falcon-ntru-depth0-wip.lean). Prime suspect: solve_NTRU_deepest's deeper-(F,G) convention, never runtime-validated. Next step: differential-trace against the c-fn-dsa backend.
• euf_cma_security + the generic GPV chain (VCVio/CryptoFoundations/GPVHashAndSign.lean ×4) — this is exactly what feat(Falcon): idealized-model EUF-CMA via GPV, down to NTRU-SIS (#188) #466 addresses; coordination point.

Sorry count: 14 (9 Falcon + 4 GPV + 1 ToMathlib/RenyiDivergence). Full LatticeCrypto build green at v4.30.0. #print axioms confirmed standard-only on every proven result above.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Falcon faithfulness & soundness remediation — concrete keygen, verify_sign_correct, verify bridge

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

Falcon faithfulness & soundness remediation — concrete keygen, verify_sign_correct, verify bridge

This PR addresses a major gap in the Falcon formalization by building out the concrete correctness layer (sign, keyGenFromSeed, verify_sign_correct) and auditing byte-level faithfulness, complementing the abstract EUF-CMA proof in PR #466.

Mathematical Formalization

• Correctness proof: LatticeCrypto/Falcon/Correctness.lean proves verify_sign_correct — a non-aborting signature always verifies. The theorem is conditional only on the abstract h_laws.compress_decompress law (not the concrete codec), and is proven by induction on maxAttempts using PSF trapdoor sampling correctness (falconPSF_eval_trapdoorSample).
• Key generation deferred: keyGenFromSeed remains a sorry in Scheme.lean; key generation is moved to LatticeCrypto.Falcon.Concrete.
• PSF trapdoor sample fix: fromFFTPreimage now takes an additional pk : PublicKey p argument and recomputes s₁ from s₂ and the public key (via s₁ = c - s₂ · h), ensuring the PSF identity s₁ + s₂ · h = c holds exactly. The falconPSF instance is updated to pass pk to fromFFTPreimage in trapdoorSample. A new theorem falconPSF_eval_trapdoorSample proves every output of trapdoorSample is an exact preimage for eval.
• ℓ₂ norm bound lemmas: LatticeCrypto/Ring/Norms.lean adds three theorems: centeredRepr_sub_natAbs_le, add_sq_le_two_mul_add_sq, l2NormSq_sub_le_two_mul_add, and pairL2NormSq_sub_le_two_mul_add — bounding differences of centered-representation ℓ₂ norms, used in security proofs.
• NTRU-SIS problem definitions: Security.lean introduces ntruSISProblemWithSample, ntruKeyedSISProblem, a helper collisionToNTRUSISSolution, and a reduction ntruPSFCollisionToKeyedSISAdversary from Falcon-PSF collisions to a keyed NTRU-SIS adversary at bound 4*betaSquared.
• Main security theorem rewritten: euf_cma_security in Security.lean now expects an ideal preimage‑sampleable function with explicit laws (hEval, hShort, hCorrect, hReg, hNeverFail, hTransport) and its proof is no longer a sorry. The bound includes samplerLoss and uses collisionBound with both qSign and qHash. A new theorem euf_cma_security_ntruSIS composes this with the collision→keyed‑SIS bridge.
• Tree sampling refactored: Primitives.lean changes the FalconTree leaf constructor from a single σ to four ℝ arguments (σ₀, σ₁, l01Re, l01Im) representing the bottom 2×2 LDL block. The ffSampling leaf case (κ=0) now implements the full bottom-2×2 LDL sampling algorithm.
• Compression/decompression roundtrip: Scheme.lean adds rqToIntPolyCentered and theorem toRq_rqToIntPolyCentered to support roundtripping.
• Signature function no longer a stub: sign is now defined as a fuel-bounded rejection loop retrying with fresh salts up to maxAttempts, returning Option Signature.

Protocols / Soundness

• GPV hash-and-sign refactored: The monolithic GPVHashAndSign.lean is split into 11 submodules (Basic, CollisionTelescope, Factorization, GameRuns, TapeFactorization, FlagHandlers, CombinedHandler, GameIdentification, VerificationBridge, TrapCount, EmbedIndex, Security). All previously sorry-filled definitions and theorems are now proven.
• Verify bridge: Concrete/FPRBridge.lean — concrete_verify_eq_verify is simplified: the previous hypotheses hsigDecode, hpkDecode, hmul, and hnorm are removed, replaced by hn_ovf (a UInt64 overflow bound) and hn4 (4 ∣ p.n). The proof now directly uses the lemmas sigDecode_sigEncode, pkDecode_pkEncode, negacyclicMulU32_eq_negacyclicMul (unconditional), and pairL2NormSqU32_eq_pairL2NormSq (under hn_ovf).
• Concrete arithmetic kernel equalities: Instance.lean adds negacyclicMulU32_eq_negacyclicMul and pairL2NormSqU32_eq_pairL2NormSq certifying that the UInt32/Int64 fast kernels compute exactly the abstract specification-level operations.
• Signature malleability fix (B9/ENC-3): Encoding.lean tightens decompress to reject inputs whose length differs from dlen (not just shorter ones), preventing over-length malleability.

Proof Completion (sorries removed)

• verify_sign_correct in Security.lean: Removed (was a sorry); docstring redirects to LatticeCrypto.Falcon.Correctness.
• GPV forgery theorems: forgery_yields_collision_or_exact_match and its corollaries are now fully proven in the GPV submodule structure.
• euf_cma_security in Security.lean: No longer a sorry; proof is provided.
• Concrete arithmetic equality proofs: negacyclicMulU32_eq_negacyclicMul and pairL2NormSqU32_eq_pairL2NormSq are proven without sorry.
• Encoding roundtrip proofs: sigDecode_sigEncode and pkDecode_pkEncode are fully proven in Encoding.lean.
• NTC solver stubs replaced: NTRUSolver.lean replaces stubs for FXR arithmetic and poly_big_to_small with real imports from Falcon.Concrete.FXR and Falcon.Concrete.PolyBigInt. check_ortho_norm is sorry-free and executable.

Open / Work-in-Progress (why this is a draft)

• keyGenFromSeed (Scheme.lean): Still a sorry.
• solve_NTRU_depth0 (NTRUSolver.lean): Remains a sorry. A full port of c-fn-dsa's solve_NTRU_depth0 was written but fails end-to-end validation (preserved in docs/agents/falcon-ntru-depth0-wip.lean). Prime suspect: output convention mismatch from solve_NTRU_deepest.
• euf_cma_security + generic GPV chain: Addressed by PR feat(Falcon): idealized-model EUF-CMA via GPV, down to NTRU-SIS (#188) #466 (coordination point).

Infrastructure / CI

• New top-level imports: LatticeCrypto.lean extends its import list with LatticeCrypto.Falcon.Correctness and LatticeCrypto.Falcon.NonVacuity. VCVio.lean adds imports for 11 new GPV submodules.
• Non-vacuity witnesses: New files Examples/GPVNonVacuity.lean, LatticeCrypto/Falcon/NonVacuity.lean provide concrete witnesses showing the GPV EUF-CMA bounds and the Falcon security theorem are non-vacuous.
• Build status: Full LatticeCrypto build green at v4.30.0. #print axioms confirmed standard-only on every proven result.

Documentation

• docs/agents/falcon-review.md: Canonical working doc for the branch, tracking session log, spec divergences, and critical-path checklist.
• docs/agents/falcon-hpkdecode-wip.lean: Reference scaffolding for pkDecode_pkEncode round-trip (not part of build).
• docs/agents/falcon-ntru-depth0-wip.lean: Non-merged, buggy port of solve_NTRU_depth0 with failure analysis.

Refactoring

• GPVHashAndSign.lean split into 11 submodules, organized by proof phase.
• Scheme.lean: keyGenFromSeed removed to Concrete; sign implemented; fromFFTPreimage signature changed.
• Encoding.lean: pkEncode/pkDecode refactored from while loops to for-range syntax.
• Security.lean: Correctness theorem moved to Correctness.lean; security theorem signature changed.

Critical: Sorry count — 14 (9 Falcon + 4 GPV + 1 ToMathlib/RenyiDivergence). These are enumerated explicitly in the PR body and the review doc. The keyGenFromSeed and solve_NTRU_depth0 sorrys are the primary blockers.

The structure of the change is broad: the core mathematical changes concentrate in Scheme.lean, Security.lean, Correctness.lean, and the GPV submodules; the remaining files are either mechanical refactoring, non-vacuity scaffolding, or supporting lemmas.

---

Statistics

Metric	Count
📝 Files Changed	34
✅ Lines Added	15444
❌ Lines Removed	583

---

Lean Declarations

✏️ Removed: 35 declaration(s)

LatticeCrypto/Falcon/Concrete/NTRUSolver.lean (15)

• @[inline] def add (x y : FXR) : FXR
• @[inline] def lt (x y : FXR) : Bool
• @[inline] def ofInt (j : Int32) : FXR
• @[inline] def ofScaled32 (x : UInt64) : FXR
• @[inline] def sqr (_x : FXR) : FXR
• @[inline] def zero : FXR
• abbrev FXR
• private def poly_big_to_small (_logn : Nat) (_s : Array UInt32) (_off : Nat)
• private def vect_FFT (_logn : Nat) (_f : Array FXR) : Array FXR
• private def vect_adj_fft (_logn : Nat) (_a : Array FXR) : Array FXR
• private def vect_iFFT (_logn : Nat) (_f : Array FXR) : Array FXR
• private def vect_invnorm_fft (_logn : Nat) (_a _b : Array FXR) (_e : Nat) :
• private def vect_mul_realconst (_logn : Nat) (_a : Array FXR) (_c : FXR) :
• private def vect_mul_selfadj_fft (_logn : Nat) (_a _b : Array FXR) :
• private def vect_set (_logn : Nat) (_f : Array Int8) : Array FXR

LatticeCrypto/Falcon/Scheme.lean (1)

• noncomputable def keyGenFromSeed (_seed : List Byte) : PublicKey p × SecretKey p

LatticeCrypto/Falcon/Security.lean (1)

• 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: 471 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/Concrete/Encoding.lean (33)

• private def E (n : ℕ) (h : Rq n) (m : ℕ) : ByteArray
• private def decBody (n : ℕ) (g : ByteArray) :
• private def decReject (g : ByteArray) (b : ℕ) : Prop
• private def decVal (g : ByteArray) (b s : ℕ) : Coeff
• private def encStep (n : ℕ) (h : Rq n) (out : ByteArray) (b : ℕ) : ByteArray
• private def gblock (n : ℕ) (h : Rq n) (b : ℕ) : ByteArray
• private theorem E_getElem (n : ℕ) (h : Rq n) (m : ℕ) :
• private theorem E_size (n : ℕ) (h : Rq n) (m : ℕ) : (E n h m).size = 7 * m
• private theorem E_succ (n : ℕ) (h : Rq n) (m : ℕ) :
• private theorem and3fff (a : Nat) : a &&& 0x3FFF = a % 2^14
• private theorem byteArray_getElem!_data (a : ByteArray) (i : ℕ) : a[i]! = a.data[i]!
• private theorem byteArray_toList_eq (a : ByteArray) : a.toList = a.data.toList
• private theorem decVal_pkEncode (n : ℕ) (h : Rq n) (hn4 : n % 4 = 0)
• private theorem decode_loop_invariant (n : ℕ) (g : ByteArray) :
• private theorem encStep_eq_append (n : ℕ) (h : Rq n) (out : ByteArray) (b : ℕ) :
• private theorem encStep_size (n : ℕ) (h : Rq n) (out : ByteArray) (b : ℕ) :
• private theorem gblock_byte (n : ℕ) (h : Rq n) (b : ℕ) :
• private theorem gblock_data_size (n : ℕ) (h : Rq n) (b : ℕ) : (gblock n h b).data.size = 7
• private theorem gblock_size (n : ℕ) (h : Rq n) (b : ℕ) : (gblock n h b).size = 7
• private theorem getD_set!_ne' (out : Array Coeff) (k k' : ℕ) (v : Coeff) (h : k ≠ k') :
• private theorem getD_set!_self' (out : Array Coeff) (k : ℕ) (v : Coeff) (h : k < out.size) :
• private theorem group_roundtrip (c0 c1 c2 c3 : Nat)
• private theorem lor_add (a b k : Nat) (hb : b < 2 ^ k) (hd : 2 ^ k ∣ a) : a ||| b = a + b
• private theorem pkEncode_eq_E (n : ℕ) (h : Rq n) (hn : n % 4 = 0) :
• private theorem pkEncode_group_byte (n : ℕ) (h : Rq n) (hn4 : n % 4 = 0)
• private theorem pkEncode_group_decode (n : ℕ) (h : Rq n) (hn4 : n % 4 = 0)
• private theorem pkEncode_not_reject (n : ℕ) (h : Rq n) (hn4 : n % 4 = 0)
• private theorem pkEncode_size (n : ℕ) (h : Rq n) (hn4 : n % 4 = 0) :
• private theorem toList_loop_eq (a : ByteArray) :
• private theorem toU8 (a : Nat) : a.toUInt8.toNat = a % 256
• theorem pkDecode_pkEncode (n : ℕ) (h : Rq n) (hn4 : 4 ∣ n) :
• theorem publicKeyBytes_extract (logn : Nat) {n : ℕ} (h : Rq n) :
• theorem sigDecode_sigEncode (salt : Bytes 40) (compSig : List UInt8) (logn : ℕ)

LatticeCrypto/Falcon/Concrete/Instance.lean (33)

• private def colVal (n : ℕ) (fa ga : Array UInt32) (i j : ℕ) : ZMod modulus
• private def innerStep {n : ℕ} (fa ga : Array UInt32) (i : ℕ) (r : Array UInt32) (j : ℕ) :
• private def loopG {n : ℕ} (s : Rq n) (a : ℕ) : UInt64
• private def outerStep {n : ℕ} (fa ga : Array UInt32) (r : Array UInt32) (i : ℕ) :
• private theorem addCellU32 (cur prod : UInt32) (hc : cur.toNat < modulus)
• private theorem bmod_two_pow_64_eq_self (z : ℤ) (hlo : -(2 ^ 63) < z) (hhi : z < 2 ^ 63) :
• private theorem cast_natSub {a b : ℕ} (h : b ≤ a) :
• private theorem fa_bound {n : ℕ} (f : Rq n) (i : ℕ) (hi : i < n) :
• private theorem fa_cast {n : ℕ} (f : Rq n) (i : ℕ) (hi : i < n) :
• private theorem fa_getD {n : ℕ} (f : Rq n) (i : ℕ) (hi : i < n) :
• private theorem foldl_range_succ {α} (fn : α → ℕ → α) (x : α) (m : ℕ) :
• private theorem foldl_uint64_add_toNat {α : Type*} (g : α → UInt64) (l : List α)
• private theorem getD_eq_get {n : ℕ} (s : Rq n) (i : ℕ) (hi : i < n) :
• private theorem getD_set!_ne (out : Array UInt32) (k k' : ℕ) (v : UInt32) (h : k ≠ k') :
• private theorem getD_set!_self (out : Array UInt32) (k : ℕ) (v : UInt32) (h : k < out.size) :
• private theorem innerStep_size {n : ℕ} (fa ga : Array UInt32) (i : ℕ) (r : Array UInt32) (j : ℕ) :
• private theorem inner_invariant {n : ℕ} (fa ga : Array UInt32) (i : ℕ) (hi : i < n)
• private theorem kernelC_toInt (x : ZMod modulus) :
• private theorem loopG_prefix_sum_le {n : ℕ} (s : Rq n) (pre : List ℕ)
• private theorem loopG_toNat {n : ℕ} (s : Rq n) (a : ℕ) (ha : a < n) :
• private theorem loopG_toNat_le {n : ℕ} (s : Rq n) (a : ℕ) (ha : a < n) :
• private theorem mulU32_eq_foldl {n : ℕ} (f g : Rq n) :
• private theorem outerStep_spec {n : ℕ} (fa ga : Array UInt32) (i : ℕ) (hi : i < n)
• private theorem outer_invariant {n : ℕ} (fa ga : Array UInt32)
• private theorem prodU32 (a b : UInt32) (ha : a.toNat < modulus) (hb : b.toNat < modulus) :
• private theorem q_toNat : (modulus.toUInt32).toNat = 12289
• private theorem subCellU32 (cur prod : UInt32) (hc : cur.toNat < modulus)
• private theorem sum_map_range_eq_sum_fin {n : ℕ} (f : ℕ → ℕ) :
• private theorem toInt_modulus : modulus.toUInt64.toInt64.toInt = (modulus : ℤ)
• private theorem toInt_uint32_toInt64 (v : UInt32) (h : v.toNat < 12289) :
• private theorem val_toUInt32_toNat (x : ZMod modulus) :
• theorem negacyclicMulU32_eq_negacyclicMul {n : ℕ} (f g : Rq n) :
• theorem pairL2NormSqU32_eq_pairL2NormSq {n : ℕ} (hn : 2 * n * (modulus / 2) ^ 2 < 2 ^ 64)

LatticeCrypto/Falcon/Correctness.lean (1)

• theorem verify_sign_correct (pk : PublicKey p) (sk : SecretKey p)

LatticeCrypto/Falcon/NonVacuity.lean (33)

• lemma toy_step_caches (ds : PublicKey toyP → ProbComp (Rq toyP.n × Rq toyP.n))
• noncomputable def toyAdv :
• noncomputable def toyAdv' :
• 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 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_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_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_signHashQueryBound (pk : PublicKey toyP) :
• theorem toy_validKeyPair : validKeyPair toyP toyPk toySk = true

LatticeCrypto/Falcon/Scheme.lean (3)

• def rqToIntPolyCentered {n : ℕ} (f : Rq n) : IntPoly n
• theorem falconPSF_eval_trapdoorSample (pk : PublicKey p) (sk : SecretKey p) (c : Rq p.n) :
• theorem toRq_rqToIntPolyCentered {n : ℕ} (f : Rq n) :

LatticeCrypto/Falcon/Security.lean (9)

• def collisionToNTRUSISSolution
• noncomputable def ntruKeyedSISProblem
• noncomputable def ntruPSFCollisionToKeyedSISAdversary
• noncomputable def ntruSISProblemWithSample (sampleH : ProbComp (Rq p.n)) (bound : ℕ) :
• private theorem negacyclicMul_sub_left {n : ℕ} (a b c : Rq n) :
• theorem collisionFindingAdvantage_eq_ntruPSF
• theorem euf_cma_security_ntruSIS
• theorem ntruPSFCollision_advantage_le_keyedSIS
• theorem ntruPSFCollision_to_keyedSIS_valid

LatticeCrypto/Ring/Norms.lean (4)

• theorem add_sq_le_two_mul_add_sq (a b : ℕ) :
• theorem centeredRepr_sub_natAbs_le (x y : ZMod q) :
• theorem l2NormSq_sub_le_two_mul_add (p₁ p₂ : Poly (ZMod q) n) :
• theorem pairL2NormSq_sub_le_two_mul_add (x y : Poly (ZMod q) n × Poly (ZMod q) n) :

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]

…and 321 more not listed.

✏️ Affected: 1 declaration(s) (line number changed)

• noncomputable def fromFFTPreimage (c : Rq p.n) (pk : PublicKey p) (sk : SecretKey p) in LatticeCrypto/Falcon/Scheme.lean moved from L155 to L147

---

sorry Tracking

✅ Removed: 17 `sorry`(s)

LatticeCrypto/Falcon/Concrete/NTRUSolver.lean (9)

• @[inline] def sqr (_x : FXR) : FXR (L73)
• private def poly_big_to_small (_logn : Nat) (_s : Array UInt32) (_off : Nat) (L87)
• private def vect_FFT (_logn : Nat) (_f : Array FXR) : Array FXR (L90)
• private def vect_adj_fft (_logn : Nat) (_a : Array FXR) : Array FXR (L94)
• private def vect_iFFT (_logn : Nat) (_f : Array FXR) : Array FXR (L91)
• private def vect_invnorm_fft (_logn : Nat) (_a _b : Array FXR) (_e : Nat) : (L93)
• private def vect_mul_realconst (_logn : Nat) (_a : Array FXR) (_c : FXR) : (L96)
• private def vect_mul_selfadj_fft (_logn : Nat) (_a _b : Array FXR) : (L98)
• private def vect_set (_logn : Nat) (_f : Array Int8) : Array FXR (L89)

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 (+1101/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean (+1394/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/GameRuns.lean (+1252/-0)
• VCVio/CryptoFoundations/GPVHashAndSign/Security.lean (+1959/-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: Adds import Examples.GPVNonVacuity, making the module and its contents available within the Examples.lean file. This effectively includes the new file into the project's compilation.
• Examples/GPVNonVacuity.lean: Added Examples/GPVNonVacuity.lean, a new file that provides a concrete witness to show the GPV EUF-CMA bounds (GPVHashAndSign.forgery_yields_collision_or_exact_match and its corollaries) are non-vacuous. 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). The file proves four theorems: bijPSF_correct (the PSF is correct), bijPSF_regularity (the PSF is regular with a uniform domain sampler domainSample), bijPSF_hForge (the forger satisfies ForgesQueriedPoint), and adv_signHashQueryBound (the adversary makes 0 signing and 1 random-oracle query). Finally, gpv188_hyps_inhabited bundles all four conditions to confirm the side hypotheses of the GPV bounds are jointly inhabited.
• LatticeCrypto.lean: The file's import list is extended with two new modules: LatticeCrypto.Falcon.Correctness and LatticeCrypto.Falcon.NonVacuity. These additions make available the correctness proofs and the non-vacuity statements for the Falcon scheme, ensuring that the top-level library re-exports these foundational verification components.
• LatticeCrypto/Falcon/Concrete/Encoding.lean: Tightened decompress to reject inputs whose length differs from dlen (not just shorter ones), preventing signature malleability (B9/ENC-3; docstring updated accordingly). Refactored pkEncode and pkDecode from explicit while loops to for‑range syntax. Added a substantial formal verification block: private theorems toU8, lor_add, and3fff, and group_roundtrip (with set_option maxHeartbeats 1000000) prove the four bit‑packing identities; definitions gblock, encStep, E and theorems pkEncode_eq_E, gblock_byte, pkEncode_size characterize the encoder output; sigDecode_sigEncode certifies signature round‑trip for non‑empty compressed payloads; byteArray_toList_eq, byteArray_getElem!_data provide list‑ and byte‑level lemmas; pkEncode_group_byte, pkEncode_group_decode, pkEncode_not_reject, decVal_pkEncode support the round‑trip theorem pkDecode_pkEncode. No sorry or admit are introduced.
• LatticeCrypto/Falcon/Concrete/FFI.lean: The documentation comment in LatticeCrypto/Falcon/Concrete/FFI.lean was updated to correct the path of the C-side SCU amalgamation from csrc/falcon/fndsa_native.c to csrc/falcon/fndsa.c, aligning the comment with the actual file name used in the project.
• LatticeCrypto/Falcon/Concrete/FPRBridge.lean: The theorem concrete_verify_eq_verify was simplified: the previous hypotheses hsigDecode, hpkDecode, hmul, and hnorm (which required the user to supply proofs of signature/public-key round-trips and equality of concrete arithmetic kernels with their abstract counterparts) were removed. They are replaced by hn_ovf (a UInt64 overflow bound: 2 * p.n * (modulus / 2)^2 < 2^64) and hn4 (4 ∣ p.n). The proof now directly uses the lemmas Falcon.Concrete.sigDecode_sigEncode, Falcon.Concrete.pkDecode_pkEncode (with publicKeyBytes_extract), Falcon.Concrete.negacyclicMulU32_eq_negacyclicMul (unconditional), and Falcon.Concrete.pairL2NormSqU32_eq_pairL2NormSq (under hn_ovf). The docstring was updated to reflect that the arithmetic kernel equalities are now discharged by those lemmas rather than assumed.
• LatticeCrypto/Falcon/Concrete/Instance.lean: Added two correctness theorems negacyclicMulU32_eq_negacyclicMul and pairL2NormSqU32_eq_pairL2NormSq that certify the UInt32/Int64 fast kernels compute exactly the abstract specification-level operations, plus supporting private lemmas (e.g., inner_invariant, outer_invariant, loopG_toNat, foldl_uint64_add_toNat). The negacyclic multiplier proof establishes a Finset-sum invariant in ZMod modulus over the double loop and ties each output cell to negacyclicConvCoeff. The squared ℓ₂-norm proof shows the UInt64 accumulator never overflows under the hypothesis 2 * n * (modulus/2)² < 2⁶⁴ (true for all Falcon degrees) and bridges the kernel's centered‑representation computation to centeredRepr and pairL2NormSq. No sorry or admit appear.
• LatticeCrypto/Falcon/Concrete/NTRUSolver.lean: This diff replaces NTRUSolver.lean's stubs for FXR arithmetic (FXR, fxr_*, vect_*) and poly_big_to_small with imports from the now-implemented Falcon.Concrete.FXR and Falcon.Concrete.PolyBigInt modules, opening them so the descent/ascent and check_ortho_norm paths use the real routines. The check_ortho_norm function is updated to call the real fxr_* functions and to map Int8 to Int32 before calling vect_set. The solve_NTRU function changes its two poly_big_to_small calls from returning Option (Array Int8) to returning a pair (Array Int8, Bool), now extracting subarrays from buf and checking the boolean okF/okG before returning the solution. The solve_NTRU_depth0 function remains sorry with a detailed comment noting that a line-by-line port of the C code compiles but fails end-to-end validation at logn=1 due to an unresolved buffer-format or sign-convention mismatch in the deepest solver, and the sorry will be kept until the bug is localized via differential tracing against the C backend.
• LatticeCrypto/Falcon/Correctness.lean: The new file LatticeCrypto/Falcon/Correctness.lean proves the abstract correctness theorem verify_sign_correct for the Falcon signature scheme, showing that if the signer produces a signature (does not abort) then the verifier accepts. The proof proceeds by induction on maxAttempts, using the compress/decompress roundtrip, the PSF trapdoor sampling correctness lemma falconPSF_eval_trapdoorSample, and the isShort norm check. The theorem is conditional on the key pair validity and the laws of the primitives, but the proof notes that key validity is not actually needed.
• LatticeCrypto/Falcon/NonVacuity.lean: This new file provides a non-vacuity witness for the Falcon.euf_cma_security theorem by constructing a concrete instance (degree n=1, squared‑norm bound 75497472) where all hypotheses of the theorem hold. It defines toy parameters toyP, a genuinely NTRU‑valid key pair (toy_validKeyPair), an ideal PSF toyIdealPSF sharing Falcon’s eval/isShort, and proves the GPV laws (toy_correctAt, toy_hReg, toy_neverFail). A transport adversary toyAdv' and supporting lemmas (toy_ForgesQueriedPoint, toy_signHashQueryBound, toy_advantage_bound) are also given. The central theorem falcon_eufcma_hyps_inhabited conjoins all six hypothesis bundles, confirming that the conditional security bound is not vacuous.
• LatticeCrypto/Falcon/Primitives.lean: The FalconTree inductive type was refactored: its leaf constructor now takes four ℝ arguments (σ₀, σ₁, l01Re, l01Im) representing the bottom 2×2 LDL block, replacing the single σ argument. The ffSampling function's leaf case (κ=0) was updated to implement the full bottom-2×2 LDL sampling algorithm: it first samples the t₁-coordinate at σ₁ into z₁, computes the correction term l01·(t₁-z₁), adds it to t₀, and then samples the corrected t₀-coordinate at σ₀. The hashToPoint_welldefined law was removed from Primitives.Laws. The module documentation comments were updated to reflect these changes and to explain the rationale for needing four parameters per leaf.
• LatticeCrypto/Falcon/Scheme.lean: In LatticeCrypto/Falcon/Scheme.lean, the change reworks the Falcon signature scheme implementation. keyGenFromSeed is removed (key generation is deferred to LatticeCrypto.Falcon.Concrete). fromFFTPreimage is modified to take an additional pk : PublicKey p argument and now recomputes s₁ from s₂ and the public key (via s₁ = c - s₂ · h), ensuring the PSF identity s₁ + s₂ · h = c holds exactly. The falconPSF PSF instance is updated to pass pk to fromFFTPreimage in trapdoorSample. A new theorem falconPSF_eval_trapdoorSample is added proving that every output of trapdoorSample is an exact preimage for eval. A new function rqToIntPolyCentered and a theorem toRq_rqToIntPolyCentered are added to support compression/decompression roundtripping. The sign function, previously a stub (sorry), is now defined as a fuel-bounded rejection loop that retries with fresh salts up to maxAttempts; it returns Option Signature and uses rqToIntPolyCentered with the compression bound p.sbytelen. Additionally, signAttempt's docstring is updated to clarify its role as the one-shot core separated from retry logic, and the file header is updated to reflect the new decomposition.
• LatticeCrypto/Falcon/Security.lean: This file underwent a major refactor: the correctness theorem verify_sign_correct (which was a sorry) has been removed and its docstring redirects to LatticeCrypto.Falcon.Correctness. New parameterized NTRU-SIS problem definitions were introduced (ntruSISProblemWithSample, ntruKeyedSISProblem) alongside a helper collisionToNTRUSISSolution and a reduction ntruPSFCollisionToKeyedSISAdversary from Falcon-PSF collisions to a keyed NTRU-SIS adversary at bound 4*betaSquared, validated by the theorem ntruPSFCollision_to_keyedSIS_valid and the inequality ntruPSFCollision_advantage_le_keyedSIS. The main security theorem euf_cma_security was rewritten: its signature now expects an ideal preimage‑sampleable function idealPSF with explicit laws (hEval, hShort, hCorrect, hReg, hNeverFail, hTransport) instead of the previous HasUniformSamplerLoss; its proof is now given (it was a sorry), and the bound includes samplerLoss and uses collisionBound with both qSign and qHash. A new theorem euf_cma_security_ntruSIS composes this with the collision→keyed‑SIS bridge to give a reduction directly to ntruKeyedSISProblem. The concrete 40‑byte salt instance euf_cma_security_bytes40 was updated to match the new signature.
• LatticeCrypto/Ring/Norms.lean: This diff adds three new theorems in LatticeCrypto/Ring/Norms.lean. The theorem centeredRepr_sub_natAbs_le proves that the absolute value of the centered representative of a difference in ZMod q is at most the sum of the absolute values of the individual centered representatives, using ZMod.valMinAbs and the existing lemmas ZMod.natAbs_valMinAbs_add_le and ZMod.natAbs_valMinAbs_neg. The theorem add_sq_le_two_mul_add_sq establishes the inequality (a + b)² ≤ 2*(a² + b²) for natural numbers a, b. The theorem l2NormSq_sub_le_two_mul_add proves that the squared ℓ₂ norm of the difference of two polynomials p₁, p₂ : Poly (ZMod q) n is bounded by 2*(l2NormSq p₁ + l2NormSq p₂), applying centeredRepr_sub_natAbs_le, add_sq_le_two_mul_add_sq, and the existing Vector.getElem_sub lemma. Finally, pairL2NormSq_sub_le_two_mul_add extends this bound to pairs of polynomials, using l2NormSq_sub_le_two_mul_add for each component.
• VCVio.lean: Added imports for the new modules Basic, CollisionTelescope, CombinedHandler, EmbedIndex, Factorization, FlagHandlers, GameIdentification, GameRuns, Security, TapeFactorization, TrapCount, and VerificationBridge under VCVio.CryptoFoundations.GPVHashAndSign. This makes the definitions and theorems from these modules available project-wide, supporting the integration of the GPV hash-and-sign framework.
• VCVio/CryptoFoundations/GPVHashAndSign.lean: This file was refactored from a monolithic module containing the full GPV hash-and-sign construction, reductions, and theorem statements (with several sorry placeholders in reduction, programmedPreimageReduction, forgery_yields_collision, and forgery_yields_collision_or_exact_match) into an umbrella module that imports and re-exports eleven submodules (Basic, CollisionTelescope, Factorization, GameRuns, TapeFactorization, FlagHandlers, CombinedHandler, GameIdentification, VerificationBridge, TrapCount, EmbedIndex, Security). The definitions previously in this file (e.g., PreimageSampleableFunction, GPVHashAndSign, runtime, query bounds, collision-finding adversaries, reductions, and the euf_cma_* theorems) have been moved to the submodules, which are organized by proof phase. The module docstring has been updated to describe the new layout, and the copyright and authors now include Oleksandr Vovkotrub.
• VCVio/CryptoFoundations/GPVHashAndSign/Basic.lean: This new file GPVHashAndSign/Basic.lean introduces the GPV hash-and-sign signature scheme in the random-oracle model. It defines the PreimageSampleableFunction (PSF) structure with an evaluation map, a probabilistic trapdoor sampler, and a shortness predicate; declares correctness properties Correct and CorrectAt for PSFs; formulates the Regularity property (preimage-sampleability) as an equality of joint distributions; and constructs the GPVHashAndSign signature algorithm specifying key generation, signing, and verification using a random oracle and PSF. The file also provides the runtime bundle for the random-oracle world, a structural signHashQueryBound predicate tracking signing and hashing queries, and adversary interfaces (CollisionAdversary and ProgrammedPreimageAdversary) together with their corresponding experiments (collisionFindingExp, programmedPreimageExp) and advantage definitions.
• VCVio/CryptoFoundations/GPVHashAndSign/CollisionTelescope.lean: This new file introduces the salt-collision telescope for the GPV Hash-and-Sign proof. It defines:
• reduction, a collision-adversary construction that simulates the CMA experiment with a programmable random oracle and hidden preimage table.
• collisionBound, the GPV birthday bound (qSign+qHash)²/(2·|Salt|), and supporting lemmas (probEvent_mem_uniformSample, sum_range_div_card_le_collisionBound, probEvent_salt_collision_le_collisionBound) that compute and bound the salt-collision union probability.
• A salt-averaged combined draw-then-check process saltSeq and its key probability identities: probEvent_saltSeq_le (running sum bound), probEvent_saltSeq_succ (tight recursion via inclusion-exclusion), and probEvent_saltSeq_le_collisionBound (final bound via Gauss sum).
• The stateful, flag-carrying signing process signRunF and the core 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-averaged collision probability (and thence by collisionBound).
• Helper results: tvDist_signStep_real_programmed_le_collision (per-step identical-until-bad coupling), signRunF_neverFail, evalDist_signRunF_bind_const, tvDist_bind_le_of_forall_le, and the salt-split identity tsum_probOutput_uniformSample_ite.

The file also contains extensive documentation explaining why the salt-averaged telescope is necessary (the salt draws are invisible at the hash-only oracle granularity) and how the content splits into proof decomposition, salt-collision bounds, and salt-inclusive coupling primitives. There are no sorry or admit in the diff; all theorems are fully proven.

• VCVio/CryptoFoundations/GPVHashAndSign/CombinedHandler.lean: This file introduces the 'combined handler' for the GPV Hash-and-Sign security proof, merging the programmed freshness game handler and the collision reduction's internal handler into a single query handler progGameRunImplCombined. It defines the reduction's internal handler reductionImpl and the pre-sampled-index handlers embedAtIndexImpl and embedTrapImpl, along with their step-wise and run-level distributional equality lemmas (evalDist_embedAtIndex_step_eq_embedTrap, evalDist_run_embedAtIndexImpl_eq_embedTrap). The file adds the trapdoor-recording sibling handler progGameRunImplCombinedTrap and proves per-step and run-level equidistribution with the combined handler under GPV regularity (evalDist_progGameRunImplCombined_step_eq_trap, evalDist_run_progGameRunImplCombinedTrap_eq). Two projections are established: dropping the hidden table recovers the programmed game handler (map_run_progGameRunImplCombined_proj_table), and dropping the signed-set and flag recovers the reduction handler (map_run_progGameRunImplCombined_proj_reduction). Finally, it defines and proves preservation of cache/table coherence invariants (combinedCacheTableInv, combinedCacheImpliesTableInv, combinedTableInDomainInv) throughout the combined simulation.
• VCVio/CryptoFoundations/GPVHashAndSign/EmbedIndex.lean: This new file (EmbedIndex.lean) introduces signed-set-augmented index‑embed query implementations embedTrapIdxSigImpl and embedTrapFreshIdxSigImpl, which extend the existing embedTrapIdxImpl / embedTrapFreshIdxImpl with a passive Finset M that tracks which messages have been signed. It proves per‑step and run‑level projection lemmas (embedTrapIdxSigImpl_proj, map_run_embedTrapIdxSigImpl_proj, and their FreshIdx analogues) showing that dropping the signed set recovers the original handlers; off‑winner equality (embedTrapIdxSigImpl_run_step_eq_embedTrapFreshIdxSig); a post‑winner coincidence lemma (evalDist_run_embedTrapIdxSigImpl_eq_embedTrapFreshIdxSig_of_lt); a front‑loading lift (evalDist_frontDraw_embedTrapIdxSigImpl_eq_embedTrapFreshSigImpl) and its expected‑functional form (tsum_probOutput_embedTrapFreshIdxSig_mul_eq_frontDraw); and two critical invariants — embedTrapIdxSigImpl_fresh_idx_cache_eq (freshness‑confined winner‑slot cache recovery) and progGameRunImplCombinedTrapCount_table_support (write‑only trapdoor‑table support invariant).
• VCVio/CryptoFoundations/GPVHashAndSign/Factorization.lean: This new file VCVio/CryptoFoundations/GPVHashAndSign/Factorization.lean sets up the adaptive-to-signRunF factorization for the GPV hash-and-sign signature scheme. It defines the typed predicate AdaptiveFactorizesSignRunF (which asserts that the adaptive real and programmed game runs equal in distribution to corresponding signRunF runs over a common cache sequence) and proves factorized_advantage_le_collisionBound, showing that if this predicate holds then the total variation distance between the two adaptive runs is bounded by collisionBound. It also provides concrete GPV step handlers gpvStepReal and gpvStepProg (for the lazy random oracle cache), and proves supporting lemmas: regularity_signAnswer_agree (PSF regularity equates the real and programmed per‑step distributions), gpvStepReal_neverFail (the real handler never fails under a total trapdoor sampler), gpvStep_agree (distributional agreement between the two handlers under regularity), evalDist_gpvSignBody_run_eq_gpvStepReal (a per‑body cache‑miss splice for the real run), and evalDist_gpvSignBody_run_eq_gpvStepProg (its programmed‑side dual). No sorry or admit appear.
• VCVio/CryptoFoundations/GPVHashAndSign/FlagHandlers.lean: This new file introduces flag-instrumented versions of the original inline-salt GPV Hash-and-Sign handlers — gpvRealImplFlag and progGameRunImplNoRecFlag — which add a collision flag to the state to bound total-variation distance via an identical-until-bad lemma. It provides per-query and run-level projection lemmas, bad monotonicity, and a universal off-bad agreement theorem (gpvImplFlag_h_agree_good) that feeds into the framework's tvDist_simulateQ_run_le_probEvent_output_bad. The main reduction gpv_tvDist_orig_run_le_probEvent_flag bounds the TV distance between realGameRun and progGameRun by the run-level collision-flag probability, and the cardinality-telescope theorem gpv_orig_flag_le_collisionBound bounds that probability by collisionBound using the salt-averaged birthday term. A second family of handlers (gpvRealImplFlagFresh, progGameRunImplNoRecFlagFresh) extends the state with a Finset M tracking signed messages, enabling the EUF-CMA forgery condition to read freshness; their flag probability and off-bad agreement are inherited from the base flag handlers.
• VCVio/CryptoFoundations/GPVHashAndSign/GameIdentification.lean: This new file GameIdentification.lean adds the game-identification infrastructure for the GPV hash-and-sign unforgeability proof. It defines the cross-monad bridge (map_simulateQ_gpvOuter_writerLog_eq_gpvRealImplFresh) that reconstructs the WriterT signing log as a Finset M signed-set, identifying the WriterT-based unforgeability experiment with the freshness-tracking vehicle gpvRealImplFresh. It introduces the verify-Bool games realGameVerifyFresh and progGameVerifyFresh on that vehicle, together with the verification read gpvVerifyRead and the key coupling lemma gpv_realGameVerifyFresh_le_progGameVerifyFresh_add_collisionBound relating them. The file also provides the state-threading bridge runtime_evalDist_liftComp (reducing the runtime's sum-spec semantics to the bare random oracle), the U2 sign-then-hash hop in two forms (tvDist_runtime_real_programmed_le_bad and the salt-inclusive tvDist_runtime_real_programmed_le_collisionBound_saltInclusive), and the final Step-1 TV bound gpv_tvDist_real_programmed_le_collisionBound.
• VCVio/CryptoFoundations/GPVHashAndSign/GameRuns.lean: This new file (GameRuns.lean) is the core of the GPV hash-and-sign security proof's coupling argument. It defines the two game runs (realGameRun and progGameRun) for the adversary's main computation, normalizes them to a common StateT-based simulateQ shape by peeling apart runtime indirection and dropping passive state components, then introduces tape-consuming versions of both handlers (gpvRealImplTape, progGameRunImplTape) and flag-instrumented variants carrying a collision flag. Key supporting lemmas establish per-step distributional bridges for the real and programmed tape handlers (e.g., evalDist_gpvRealImplTape_sign_cache_eq_gpvStepReal, evalDist_progGameRunImplTape_sign_cache_eq_gpvStepProg, evalDist_gpvImplTape_run_sign_miss_eq) and prove that the flag is passive and monotone. The file contains no sorry or admit.
• VCVio/CryptoFoundations/GPVHashAndSign/Security.lean: This new file, VCVio/CryptoFoundations/GPVHashAndSign/Security.lean, establishes the security bounds for the GPV hash-and-sign signature scheme by proving several key lemmas and theorems. It introduces evalDist_map_run_simulateQ_eq_of_query_evalDist_map_eq, a distribution-level state-projection transport theorem, and uses it to prove map_run_progGameRunImplCombinedTrapCount_freshSig_proj, which shows that the trap-count-augmented run projects to the fresh-signature run at the distribution level. The file then proves progGameRunImplCombinedTrapCount_table_defer, demonstrating that the write-only trapdoor draw at a forged key can be deferred to the end of the run's adaptive fold. These results are used to establish trap_freshSig_le_winnerSlot_deferred, which bounds the trap event on the counter-augmented run by an expectation over the fresh-signature run, and reservoir_embed_commute_winner_floorFree, the floor-free form of the per-slot front-loading deferred-sampling coupling.
• VCVio/CryptoFoundations/GPVHashAndSign/TapeFactorization.lean: Adds a new file TapeFactorization.lean that establishes the front salt-tape factorization for the GPV hash-and-sign scheme. It defines tapeCheck and proves lemmas drawList_salt_succ, evalDist_gpvSignStep_commute_real, evalDist_gpvRealImpl_eq_drawList_gpvRealImplTape and their programmed-side duals (evalDist_gpvSignStep_commute_prog, evalDist_progGameRunImplNoRec_eq_drawList_progGameRunImplTape), which decompose each game run into a front draw of signing salts followed by a tape-consuming run. Pinned bridge theorems realGameRun_eq_drawList_gpvRealImplTape and progGameRun_eq_drawList_progGameRunImplTape connect the actual game runs to this form. The file then derives the Step-1 TV bound directly via tvDist_drawList_bind_le and probEvent_tapeCheck_drawList_le_collisionBound. It also provides off-bad agreement lemmas (gpvImplTape_run_unif_eq, gpvImplTape_run_read_hit_eq, evalDist_gpvImplTape_run_read_miss_eq, evalDist_eval_domainSample_eq_uniform, and gpvImplTapeFlag_h_agree_good) that support the per-tape identical-until-bad coupling. No sorry or admit are present. This file is a central component of the GPV security proof, reducing the run-level coupling to a birthday bound on salt collisions.
• VCVio/CryptoFoundations/GPVHashAndSign/TrapCount.lean: This file introduces the counter-augmented trap run progGameRunImplCombinedTrapCount – a passive (idxTable, counter) instrument on top of progGameRunImplCombinedTrap – and proves projection lemmas (progGameRunImplCombinedTrapCount_proj, map_run_progGameRunImplCombinedTrapCount_proj), a lockstep invariant (progGameRunImplCombinedTrapCount_idx_iff_table), and bounds on the counter and recorded index (progGameRunImplCombinedTrapCount_run_count_le, progGameRunImplCombinedTrapCount_idx_lt_count, progGameRunImplCombinedTrapCount_idx_lt_budget). It also provides embedTrapFreshImpl (a plain lazy random oracle with a passive counter) and proves the GPV Step‑2 front‑loading lift evalDist_frontDraw_embedTrapImpl_eq_embedTrapFresh via per‑step independence lemmas (embedTrapImpl_run_step_indep_of_target, embedTrapImpl_run_step_eq_embedTrapFresh, evalDist_run_embedTrapImpl_eq_embedTrapFresh_of_lt) and the commutation theorem embedTrapImpl_frontDraw_commute. Finally, it defines index‑augmented handlers embedTrapIdxImpl and embedTrapFreshIdxImpl (passive insertion‑index tables) and their projection lemmas (embedTrapIdxImpl_proj, map_run_embedTrapIdxImpl_proj, embedTrapFreshIdxImpl_proj) to support trap‑mass index partitioning via the auxiliary lemma probEvent_eq_tsum_probEvent_index_aux. No sorries or admits are present.
• VCVio/CryptoFoundations/GPVHashAndSign/VerificationBridge.lean: This new file VCVio/CryptoFoundations/GPVHashAndSign/VerificationBridge.lean (1399 lines) introduces the formal verification bridge for the GPV Hash-and-Sign signature scheme. It contains the following key theorems, definitions, and lemmas:

• gpv_realGameVerify_le_progGameVerify_add_collisionBound: a data-processing inequality transferring the Step‑1 total-variation bound to any verification post-processor.
• probOutput_unforgeableExp_eq_keygen_average: keygen-averaging peel of the GPV unforgeability experiment, commuting the key generation out of the withStateOracle semantics.
• simulateQ_writerImpl_verify_fold: a lemma folding the verification continuation into the WriterT run.
• signedSet_eq_wasQueried: per‑key game-identification equating the WriterT-log experiment with the freshness verify‑Bool game realGameVerifyFresh.
• gpv_advantage_le_progGameVerifyFreshAvg_add_collisionBound: the main advantage bound, chaining the above to reduce the GPV EUF‑CMA advantage to the keygen-averaged programmed freshness game plus collisionBound.
• ForgesQueriedPoint: a predicate stating that the forger’s output point is always cached (standard ROM well‑formedness).
• collisionFindingAdvantage_reduction_eq: unfolds the collision‑finding advantage to a plain probability of a distinct-collision event.
• isShort_of_mem_support_domainSample: a lemma that forward-sampled preimages satisfy the shortness predicate under PSF correctness and regularity.
• run_combined_gpvVerifyRead_of_cache_hit and run_combined_verifyKont_of_cache_hit: lemmas establishing that the verification read is table‑passive on a cache hit.
• combined_cache_forge_point_ne_none: transports hForge to the combined run.
• progGameVerifyFresh_eq_probEvent_combined and reduction_collision_eq_probEvent_combined: express the programmed game success and collision‑reduction success as events on the combined run.
• distinct_implies_collision_pointwise: pointwise transfer from distinct‑preimage winning to a table collision.
• combinedTableSupport, combinedTableSupport_write_card_le, combinedTableSupport_run_card_le, combined_run_table_card_le: definitions and bounds on the hidden‑preimage table’s cardinality (the reservoir size).
• gpv_perKey_distinct_le_collision: probability‑level transfer of the distinct‑collision bound.
• probOutput_reservoirStep_win, probEvent_reservoirStep_miss, reservoirWinnerIndex, reservoirWinnerIndex_succ, tsum_reservoirStep_survival, probOutput_reservoirStep_ne, probOutput_reservoirStep_eq: reservoir‑sampling analysis for the programmed‑preimage reduction (the Step‑2 extraction).

The file contains no sorry or admit; all theorems are proven. It establishes the probabilistic and combinatorial infrastructure needed to connect the GPV unforgeability experiment to the collision‑finding advantage, forming the core of the verification bridge.

• docs/agents/falcon-hpkdecode-wip.lean: Added docs/agents/falcon-hpkdecode-wip.lean, a new WIP scaffolding file that provides proven lemmas and definitions toward proving the pkDecode_pkEncode round-trip property. The file defines helpers such as group_roundtrip (showing 7-byte encoding/decoding of four coefficients), gblock, E (the iterative encoding), and pkEncode_eq_E (relating the existing pkEncode to E). It also includes size lemmas (E_size) and an element-access theorem (E_getElem). All declarations are marked as proven and compile against the refactored Encoding.lean, and the file is not part of any build target, serving as a reference for future integration.
• docs/agents/falcon-ntru-depth0-wip.lean: This diff introduces a new file docs/agents/falcon-ntru-depth0-wip.lean containing a non-merged, buggy port of the solve_NTRU_depth0 function from the C reference implementation (kgen_ntru.c:1575–1766) into Lean, intended to replace a sorry placeholder in LatticeCrypto/Falcon/Concrete/NTRUSolver.lean. The file documents the port's status: it compiles without sorry or admit, and its internal verify gate (x != rv → none) ensures it returns none rather than incorrect output, but end-to-end validation fails for all tested inputs at logn=1 because the Babai reduction leaves (F,G) unreduced or the output convention from solve_NTRU_deepest mismatches solve_NTRU_depth0's lift expectations. The diff includes the full Lean implementation (commented out under example : True := trivial), a detailed failure analysis identifying four prime suspects (output convention of solve_NTRU_deepest, mp_NTT index reuse, FXR division scaling, and verify gate's Montgomery conventions), and a recommended debugging strategy (compare buffer contents against a C harness).
• docs/agents/falcon-review.md: This document is a new working doc (docs/agents/falcon-review.md) that serves as the canonical bootstrap for the falcon-faithfulness-review branch. It defines a session protocol for adversarial review of the Falcon implementation against three baselines (Falcon v1.2, FN-DSA/FIPS 206, and c-fn-dsa), tracks the status of a critical-path checklist (with items like verify_sign_correct proven, KG-quickwin done, and B9/ENC-3 fixed), and records detailed findings, resolved issues, unresolved sorries (9 live Falcon sorries + 4 GPV + 1 ToMathlib = 14 total), intended spec divergences, a session log (s0–s13), a drift-check snippet, and a spec-of-record matrix cross-referencing behaviors M1–M9. It also documents the uninitialized third_party/c-fn-dsa submodule prerequisite and the unresolved solve_NTRU_depth0 attempt reverted to sorry, along with a verified-faithful section confirming several concrete-level constants and parameters.
• scripts/falcon_review.mjs: Added a new read-only adversarial review harness script (scripts/falcon_review.mjs) for the Falcon formal verification project. The script implements a phased, automated audit pipeline that evaluates LatticeCrypto/Falcon's formalization against three baselines (Falcon v1.2 spec, FN-DSA/FIPS 206, and the c-fn-dsa reference implementation) across nine configurable dimensions (HashToPoint, Verify, Sign+ffSampling, KeyGen+NTRUSolve, SamplerZ, Encoding, Parameters, Theorem-soundness, Trust-boundary). It includes an embedded spec-of-record baseline matrix (M1-M9) documenting known divergences between these three sources, a configurable baseline sorry count mechanism (default 14 live sorrys) for detecting drift, and a structured output schema for findings and adversarial verification. The script is designed to be re-runnable via Claude Code Workflow with optional parameters to control review scope, source refetching, and change-specific regression focus.
• 2 file(s) filtered as noise (lockfiles, generated, or trivial): AGENTS.md, csrc/falcon/gen_testvectors.c

---

Last updated: 2026-07-10 11:12 UTC.

[alexanderlhicks]

@alik-eth I'd started doing some work on Falcon after someone asked me about it but it didn't seem necessary in the end (cc https://github.com/kobigurk ?) so I left it unfinished; since you have an active PR looking at this, feel free to re-use anything valuable here (add me as co-author to any PR I guess).
I primarily followed https://falcon-sign.info/ rather than the NIST submission, assuming this would be a more up to date reference, with an intention to experiment with FFI into the reference C code but didn't reach that stage.

[github-actions]

Build Timing Report

• Commit: 6ef7476
• Message: Merge 0538916 into 24fe01d
• Ref: falcon-faithfulness-review
• Comparison baseline: 24fe01d from the latest successful main run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets Interop; warm rebuild lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets Interop; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	795.23	787.94	-7.29	ok
Warm rebuild	6.20	4.94	-1.26	ok
Smoke test	3.25	3.42	+0.17	ok

Incremental Rebuild Signal

• Warm rebuild saved 783.00s vs clean (159.50x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
68.00	72.00	-4.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
63.00	70.00	-7.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
41.00	44.00	-3.00	VCVio/CryptoFoundations/ReplayFork.lean
39.00	31.00	+8.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
32.00	37.00	-5.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
30.00	27.00	+3.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
29.00	30.00	-1.00	Interop/Hax/Barrett.lean
29.00	30.00	-1.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
28.00	28.00	+0.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
26.00	27.00	-1.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
24.00	30.00	-6.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
23.00	23.00	+0.00	VCVio/CryptoFoundations/SecExp.lean
23.00	21.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
21.00	25.00	-4.00	VCVio/OracleComp/Coercions/Add.lean
21.00	23.00	-2.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
20.00	24.00	-4.00	VCVio/OracleComp/QueryTracking/Birthday.lean
20.00	21.00	-1.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
19.00	14.00	+5.00	Examples/CommitmentScheme/Hiding/CountBounds.lean
18.00	21.00	-3.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
18.00	24.00	-6.00	Examples/SimpleTwoServerPIR.lean

[alik-eth]

@alexanderlhicks This is exactly the missing half — nice catch on ENC-3, that's a genuine wire bug. Mapped the interaction with #466 precisely:

Conflict surface is just two files — Falcon/Scheme.lean and Falcon/Security.lean — and it's decl-level clean: #466 removes the sorry-backed sign/keyGenFromSeed/verify_sign_correct and rewrites Security.lean around the EUF-CMA chain; your branch re-adds those same decls properly proven. Everything else here (Concrete/*, Primitives, FFI, the review harness) is disjoint from #466.

Proposed sequencing: #466 lands first (it's deep in review and unblocks the sorry-free GPV chain — 4 of your 14 sorries disappear on rebase), then this rebases on top and your correctness cluster slots back in additively. One suggestion for the rebase: consider landing verify_sign_correct + the fuel-bounded sign in their own module (e.g. Falcon/Correctness.lean, or next to your verify bridge in Concrete/) so Security.lean stays security-only — keeps future churn between our branches near zero. Happy to help with that rebase; I know both trees well.

Synergy after both land: your correctness layer is the natural discharge route for part of #466's hypothesis surface (hCorrect/hNeverFail on honest keys, eventually hTransport via SamplerQuality/renyiDiv). Also: does your local work cover the ntruPSFCollisionProblem → ntruSISProblem kernel-vector bridge? It's small and self-contained; if yours doesn't, I'll pick it up after your rebase so we don't cross in Security.lean.

[alexanderlhicks]

Proposed sequencing: #466 lands first

Agreed. I'll aim to rebase asap as I'll be bus with other priorities later this month and want to ensure my partial work is useful rather than a blocker.

One suggestion for the rebase: consider landing verify_sign_correct + the fuel-bounded sign in their own module (e.g. Falcon/Correctness.lean, or next to your verify bridge in Concrete/) so Security.lean stays security-only

Yep, can do.

ntruPSFCollisionProblem → ntruSISProblem

I only have the definition, stated as

/-- The NTRU-SIS problem: given `h ∈ R_q` (the Falcon public key), find short
`(s₁, s₂) ∈ R_q²` satisfying `s₁ + s₂ · h = 0 mod q` with
`‖(s₁, s₂)‖₂² ≤ ⌊β²⌋`.

This is the lattice problem underlying Falcon's security. It is an instance of
the generic SIS problem where the matrix is the single-row matrix `[I | h]`
over the cyclotomic ring `R_q = ℤ_q[x]/(x^n + 1)`. -/
noncomputable def ntruSISProblem [SampleableType (Rq p.n)] :
    SIS.Problem (Rq p.n) (Rq p.n × Rq p.n) where
  sampleChallenge := $ᵗ (Rq p.n)
  isValid h x :=
    decide (x ≠ (0, 0)) &&
    decide (pairL2NormSq x.1 x.2 ≤ p.betaSquared) &&
    decide (x.1 + negacyclicMul x.2 h = 0)

I may have a bit of time to look at it further but if you don't see anything by sometime next week you can assume I've been prioritising other work and feel free to pick it up from there. (edit: started on this)

[alexanderlhicks]

Rebased this onto #466.

This adds

• Correctness split: verify_sign_correct moved into LatticeCrypto/Falcon/Correctness.lean, so Security.lean stays security-only (per @dtumad's file-organization steer / your suggestion).
• collision → keyed-SIS bridge: shipped the two follow-ups from the design note above —
  • ntruPSFCollision_to_keyedSIS_valid: a valid Falcon-PSF collision differences to a valid keyed NTRU-SIS solution at bound 4·betaSquared (kernel by negacyclicMul_sub_left; norm by new centered-residue triangle lemmas in Ring/Norms.lean — the valMinAbs min-representative inequality, so no no-wraparound hypothesis is needed);
  • ntruPSFCollision_advantage_le_keyedSIS: the reduction adversary wins with ≥ the collision advantage;
  • euf_cma_security_ntruSIS: your euf_cma_security, composed with the bridge, so the bound now terminates at ntruKeyedSISProblem (4·betaSquared) — the standard [I | h] kernel-vector target.
  • The SIS problem is parameterized (ntruSISProblemWithSample by sampler + bound); the idealized uniform-h/betaSquared ntruSISProblem is kept separate. The uniform-h step (NTRU decisional) is the remaining piece, deliberately not assumed here.

The sorry count is 8 (down from 14): FPRBridge ×5 (FPR error bounds behind the disabled HasRealSemantics), NTRUSolver ×2 (the NTRU-solver ascent), and the ToMathlib Rényi sorry — your GPV chain resolved the other six.

Credited you as co-author on the bridge commit since it builds directly on your euf_cma_security / ntruPSFCollisionProblem.

Review is encouraged as always of course, but I think this is a good handover point otherwise.

[aryaethn]

Coordination note on the Concrete/FPRBridge.lean real-semantics layer — this touches the same file, so flagging early per your "don't diverge or duplicate."

Your concrete_verify_eq_verify bridge discharges the verify path with no semantic hypotheses, which is great — and it deliberately stops short of the real-semantics arithmetic layer in that same file: toReal and the add/mul/div/sqrt/expm_p63_error bounds (#229–233), plus the commented-out HasRealSemantics FPR instance in ApproxArith.lean. That's what #468 is about.

The blocker there is that def toReal x := (Float.ofBits x).toRat0 routes through opaque @[extern] Float, invisible to the kernel — which the ApproxArith.lean instance docstring already documents ("Not provable as stated."), proposing two fixes. Option 2 — "a verified pure-Lean IEEE-754 decoder that replaces the opaque Float path" — is exactly the toRatBits decoder I proposed in #468, and I have it working: decoding the UInt64 bits directly (sign / biased-exp / mantissa → ℚ → ℝ) makes interp_zero, interp_one, and neg_exact kernel-provable with no extra axioms (#print axioms = [propext, Classical.choice, Quot.sound]); sub_error then follows from add_error + neg_exact. The four core rounding-error bounds stay genuine work (a formalization of Pornin's integer-only emulation), but become well-posed instead of inaccessible.

Blast radius is a drop-in swap of the def toReal body — the five theorem statements are textually unchanged, and toReal is noncomputable so nothing evaluates it. Since you're live in this file, I'd sequence a small PR (decoder swap + interp_zero/interp_one/neg_exact + uncomment the HasRealSemantics FPR instance, leaving the four error bounds as tracked #229–232 sorries) behind or alongside #471 — whatever avoids a collision. Does that split work for you? cc @quangvdao.

---

Written by aryaethn's Claude Code Agent (Approved by aryaethn)

[alik-eth]

@alexanderlhicks Heads-up for your planned rebase: #466's Falcon surface moved substantially this round, all additive to Security.lean's security-only scope (which should keep your correctness cluster conflict-free as discussed):

• SISBridge.lean — the collision→NTRU-SIS kernel-vector bridge (euf_cma_security_ntruSIS).
• samplerTransport + euf_cma_security_of_samplerTransport(_queryBound) — the finite-precision transport hypothesis decomposed into a per-call sampler bound with a proven qSign · ε accumulation; the _queryBound variant also drops ForgesQueriedPoint via the append-query compiler that landed in feat(GPV): generic GPV hash-and-sign framework with EUF-CMA collision bounds #478.
• idealSamplerGuessBound + euf_cma_collision_security — the exact-match term discharged under a named min-entropy assumption (1-D discrete-Gaussian mass bounds backing it are feat(LatticeCrypto): discrete Gaussian mass bounds (mode, sum, guessing probability) #485, off main).

Scheme.lean is untouched beyond what you saw at review time. If any of this crosses wires with the faithfulness work, happy to coordinate sequencing again.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77