mirror of https://github.com/luxfi/proofs.git synced 2026-10-30 15:21:05 +00:00

Files

T

History

zeekay 0f5352f89e proofs: sweep Corona → Corona across Lean theorems and TeX papers

Production R-LWE library is luxfi/corona. Rename all Lean identifiers
(coronaCertValid → coronaCertValid, coronaSigs → coronaSigs,
blsCorona → blsCorona, corona_robustness → corona_robustness,
CoronaSig → CoronaSig, ICoronaThreshold → ICoronaThreshold,
corona_unforgeable → corona_unforgeable, corona_security_bits
→ corona_security_bits, etc.) and TeX prose to use the production
identifier.

File rename: lean/Crypto/Corona.lean → lean/Crypto/Corona.lean,
with internal module header + lakefile reference updated.

BibTeX cite key `corona2025` retired in favour of
`boschini2024corona` as the citation handle.

The historic luxfi/nasua academic R-LWE fork is not linked from any
proof or paper.

2026-05-12 09:25:18 -07:00

README.md

proofs: README — drop Pulsar-M references (family rename)

2026-05-11 15:05:58 -07:00

strict-e2e-pq-soundness.tex

proofs: sweep Corona → Corona across Lean theorems and TeX papers

2026-05-12 09:25:18 -07:00

README.md

LUX_STRICT_E2E_PQ formal proof tree

Machine-checked counterparts to the LUX_STRICT_E2E_PQ paper (luxfi/papers/lp-stricte2epq/).

The strict-e2e-pq profile pins every byte that gates a state transition on Lux to a FIPS 203 / 204 / 205 primitive or a SHA3-family transcript. This directory carries the proofs of the underlying soundness claims, the TLA+ state machine for the profile lifecycle, and the Go property tests that exercise the canonical Go code under both strict and permissive profiles.

See LP-105 §Claims and evidence for the canonical claims/evidence table.

Files

File	Language	Purpose
`strict-e2e-pq-soundness.tex`	LaTeX	formal soundness statement (companion to lp-stricte2epq §13)
`../tla/StrictPQProfile.tla`	TLA+	profile state machine and SchemeGate invariant
`../tla/MC_StrictPQProfile.tla`	TLA+	TLC model checker config
`../lean/StrictE2EPQ/Profile.lean`	Lean 4	`IsE2EPQ profile` proposition
`../lean/StrictE2EPQ/Coverage.lean`	Lean 4	14-path PQ coverage theorem
`../property/strict_pq_test.go`	Go	property tests against `luxfi/consensus`

Build

# Lean 4
cd ../lean && lake build StrictE2EPQ

# TLA+
cd ../tla && tlc MC_StrictPQProfile.tla

# Go property tests
cd ../property && GOWORK=off go test ./...

Soundness statement

Under LUX_STRICT_E2E_PQ:

Every signed transaction is verified under ML-DSA-65 (FIPS 204).
tx_auth_root inclusion is sound under SHA3-384 Merkle.
ComputeRoundDigest is collision-resistant under SHA3-384.
Pulsar finality signatures verify under M-LWE soundness.
Profile-bumps are the only mechanism that can relax the posture; the pinned digest is the operator-visible barrier.

See strict-e2e-pq-soundness.tex for the formal statement; see Profile.lean and Coverage.lean for the Lean 4 propositions.