mirror of https://github.com/luxfi/magnetar.git synced 2026-09-24 00:25:23 +00:00

Files

T

zeekay 798b9f653b magnetar v1.1: restore EasyCrypt + Lean proof track for strict-atom path

Closes MAGNETAR-PROOF-TRACK-V11.

Theory files (proofs/easycrypt/):
  - Magnetar_N1_StrictAtom.ec --- Class N1-analog strict-atom byte-
    equality theorem. Headline statement:

      forall m pkSeed pkRoot msg ctx picks lambdas,
        valid_quorum picks =>
        lagrange_basis_at_zero picks = lambdas =>
        assemble_signature_bytes m pkSeed pkRoot msg ctx picks lambdas
          = slh_sign_deterministic m
              (sk_from_seed m (lagrange_sum lambdas picks)) msg ctx.

    Discharged via combine_assemble_axiom (Go extraction trust
    boundary).

  - Magnetar_N1_SHAKE_Expand.ec --- FIPS 205 sec 10.1 SHAKE expansion
    lemmas. Cross-cites shake256_functional (Lean Crypto.Lux.SHA3).

  - Magnetar_N1_Atom_Refinement.ec --- Magnetar-internal sec 5-8 walk
    refines circl FIPS 205 dispatch. Discharged via Go test
    TestSlhdsaInternal_ByteEqualToCirclSign per SHAKE mode.

  - Magnetar_N4_KeyDeriveStable.ec --- same-master-yields-same-pk
    lemma for reshare/rotation analysis. 0 admits.

  - lemmas/SLHDSA_Functional.ec --- FIPS 205 sec 11.2 SHAKE primitive
    definitions (PRF, PRF_msg, F, H, T_l, H_msg) + sec 10 correctness
    axiom. 4 admits (black-box specs).

  - lemmas/Magnetar_CT.ec --- Bernstein-Garcia-Levy leakage-model CT
    lemma. 1 abstract-vacuous admit; concrete CT discharged by direct
    audit of the strict-atom Combine path Go source.

Lean bridge (proofs/lean/Crypto/Magnetar/StrictAtom.lean):
  - byte_wise_shamir_lagrange_at_zero_identity (shared with
    Crypto.Pulsar.Shamir).
  - shake256_functional (shared with Crypto.Lux.SHA3).
  - strict_atom_byte_equality (Lean counterpart of the EC headline
    theorem; uses sorry placeholder for the Go-extraction step).
  - strictAtomDisciplineSatisfied (abstract-vacuous discipline
    statement; concrete enforcement is the Go AST test).

Axiom budget: 5 substantive + 1 abstract-vacuous CT admit (down from
the v0.4 cascade's 14-axiom cone). Per proofs/README.md.

Bridge doc (proofs/lean-easycrypt-bridge.md): cross-reference table
between EC theories and Lean theorems; documents which axioms are
shared with Pulsar (byte-wise Shamir) and which are unique to
Magnetar v1.1 (the strict-atom discipline statement).

2026-06-01 17:13:24 -07:00

easycrypt

magnetar v1.1: restore EasyCrypt + Lean proof track for strict-atom path

2026-06-01 17:13:24 -07:00

lean

magnetar v1.1: restore EasyCrypt + Lean proof track for strict-atom path

2026-06-01 17:13:24 -07:00

lean-easycrypt-bridge.md

magnetar v1.1: restore EasyCrypt + Lean proof track for strict-atom path

2026-06-01 17:13:24 -07:00

README.md

magnetar v1.1: restore EasyCrypt + Lean proof track for strict-atom path

2026-06-01 17:13:24 -07:00

README.md

Magnetar --- machine-checked proof track

Magnetar v1.1 closes MAGNETAR-STRICT-ATOM-V11 and lands the mechanised proof track for the strict-atom Combine path. Both primitives (per-validator standalone + THBS-SE strict-atom) are covered.

What ships at v1.1

Layer	Path
EasyCrypt theory shells	`proofs/easycrypt/`
Lean bridge (algebraic)	`proofs/lean/Crypto/Magnetar/`
Bridge doc	`proofs/lean-easycrypt-bridge.md`

The construction shape covered by the proof track:

The strict-atom emitter assembleSignatureBytes (ref/go/pkg/magnetar/thbsse_assemble.go).
The Magnetar-internal FIPS 205 sec 5/6/7/8 walk slhSignAtom (ref/go/pkg/magnetar/slhdsa_internal.go).
The byte-wise Shamir over GF(257) + Lagrange interpolation at x=0 (ref/go/pkg/magnetar/thbsse_field.go).
The byte-identity claim that ties the strict-atom Combine output to cloudflare/circl/sign/slhdsa.SignDeterministic on the same input.

Axiom budget

The strict-atom theory has 5 admits across the dependency cone:

Axiom	File	Discharge mechanism
`combine_assemble_axiom`	`Magnetar_N1_StrictAtom.ec`	Go extraction trust boundary; audit reads `assembleSignatureBytes` line-for-line against the abstract `AssembleAbs` model.
`shake256_functional`	`Magnetar_N1_SHAKE_Expand.ec`	FIPS 202 functional spec. Cross-cited from Lean `Crypto.Lux.SHA3`.
`magnetar_internal_refines_circl`	`Magnetar_N1_Atom_Refinement.ec`	Discharged by Go test `TestSlhdsaInternal_ByteEqualToCirclSign` per SHAKE mode.
`slhdsa_correctness`	`lemmas/SLHDSA_Functional.ec`	FIPS 205 sec 10 NIST verification.
`lagrange_recovers_master`	`Magnetar_N1_StrictAtom.ec`	Algebraic; Lean-bridged to `Crypto.Magnetar.StrictAtom.byte_wise_shamir_lagrange_at_zero_identity`.
(CT) abstract-level vacuous	`lemmas/Magnetar_CT.ec`	Concrete CT discharged by direct audit of strict-atom Combine path Go source.

Total: 6 admits (5 substantive + 1 abstract-vacuous), corresponding to the trust footprint enumerated in proofs/easycrypt/README.md. This is the same shape as the v0.4 EC track (1 byte-walk + 1 codec + 3 protocol-level + 1 FIPS 205) but specialised to the strict-atom construction.

v1.0 -> v1.1 delta

The v0.x EC scaffolding (modelled the abandoned reveal-and-aggregate construction) was removed at v1.0; the v1.1 track is built directly against the strict-atom Combine path.

The Lean side carries the abstract-model discipline statement strict_atom_discipline (vacuous at the abstract level; the concrete discipline is enforced by the Go test TestThbsSE_StrictAtom_NoTransientSeed).

Per-push gate

The scripts/check-high-assurance.sh orchestrator runs:

scripts/checks/go-tests.sh (v1.0 scope; carries forward unchanged).
scripts/checks/strict-atom-ast.sh (NEW at v1.1): runs the TestThbsSE_StrictAtom_NoTransientSeed AST + grep invariant gate per-push. The AST gate is a fast check that the strict-atom discipline holds on the file.
scripts/checks/easycrypt.sh (NEW at v1.1): smoke-checks the EC theory shells for syntax / require / import consistency. Full EasyCrypt re-run is a release-time gate, not per-push, because EC is heavy to bring up (the per-push gate runs in <60s; full EC takes the EC project's standard hour to run).