All issues

Replace global Injective2 in Merkle uniqueness (single + batch) with queried-domain ("Option Injective2") formulation

#486

· Abraxas1010 opened

on Jul 13, 2026

LatticeCrypto: discharging the challenge–secret norm-bound hypotheses — offering a proved no-wraparound multiplication bound

#469

· jasonsoroko opened

on Jul 6, 2026

`FPRBridge.toReal` routes through opaque `Float.ofBits`, blocking the `HasRealSemantics FPR` instance — proposal to decode the `UInt64` bits directly

#468

· aryaethn opened

on Jul 5, 2026

Add IND-CPA real-or-random variant and lor ↔ ror equivalence for DEMScheme

#412

· astefano opened

on May 26, 2026

Add deterministic symmetric encryption variant with IND$-CPA security game

#411

· astefano opened

on May 26, 2026

Add SUF-CMA (strong MAC unforgeability with pair freshness)

#410

· astefano opened

on May 26, 2026

Untracked proof obligations in the GPV / Falcon / Rényi chain (gaps from #187, #279)

#396

· dtumad opened

on May 14, 2026

Termination proofs for loop functions in `LatticeCrypto/Falcon/Concrete/NTRUSolver.lean`

#237

· quangvdao opened

on Apr 1, 2026

Proof obligation for `euf_cma_bound` in `LatticeCrypto/Falcon/Security.lean`

#236

· quangvdao opened

on Apr 1, 2026

Proof obligation for `verify_sign_correct` in `LatticeCrypto/Falcon/Security.lean`

#235

· quangvdao opened

on Apr 1, 2026

Proof obligation for `expm_p63_error` in `LatticeCrypto/Falcon/Concrete/FPRBridge.lean`

#233

· quangvdao opened

on Apr 1, 2026

Proof obligation for `sqrt_error` in `LatticeCrypto/Falcon/Concrete/FPRBridge.lean`

#232

· quangvdao opened

on Apr 1, 2026