mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
1e9e63de51
Tier A formalization paper for the Lux TFHE stack:
- PBS correctness theorem (Section 3): closure routed through
four named functional hypotheses imported from
luxfi/lattice/v7.
- Threshold-DKG correctness theorem (Section 4) composing
Mouchet-Bossuat-Hubaux PoPETS 2021 BSK derivation with
Shamir-Lagrange reconstruction (hoisted to Lean).
- Noise-budget book-keeping (Section 5) with per-PBS noise
floor under the production parameter sets PN10QP27 /
PN11QP54 / PN9QP28_STD128 / PN9QP27_STD128Q.
- Constant-time obligations (Section 6) on Encrypt / Decrypt /
BlindRotate / ExternalProduct / Bootstrap with EC declare-axiom
sections + Jasmin + dudect.
- Machine-checked-proof traceability table.
- Gates and open work cross-linked to CRYPTOGRAPHER-SIGN-OFF.md.
PDF: 9 pages, compiled by pdflatex 2025.
Cites existing LaTeX at ~/work/lux/proofs/fhe/ without restating.