mirror of
https://github.com/luxfi/magnetar.git
synced 2026-07-27 02:53:47 +00:00
Hanzo AI
30e71f1271
Tier A EC theory shells mirroring Pulsar v1.0.7's structure, adapted to SLH-DSA reveal-and-aggregate. Class N1-analog byte-equality theorem magnetar_n1_byte_equality is proved against the protocol-level Magnetar_Threshold module type; the concrete extracted corollary magnetar_n1_byte_equality_extracted composes the wrapper-bridge lemmas. Entire dependency cone is admit 0/0. Files (13): Magnetar_N1.ec — protocol-level spec + theorem Magnetar_N4.ec — reshare pk-preservation Magnetar_N1_Memory.ec — byte-memory frame lemmas Magnetar_N1_Signature_Codec.ec — FIPS 205 sig codec Magnetar_N1_Combine_Layout.ec — Combine wire layout Magnetar_N1_Sign_Layout.ec — single-party Sign wire layout Magnetar_N1_Combine_Refinement.ec — Combine byte-walk (1 axiom) Magnetar_N1_Sign_Refinement.ec — single-party byte-walk (1 axiom) Magnetar_N1_Combine_Wrapper.ec — Combine wrapper bridge Magnetar_N1_Sign_Wrapper.ec — Sign wrapper bridge Magnetar_N1_Extracted.ec — concrete extracted corollary lemmas/SLHDSA_Functional.ec — in-house FIPS 205 functional lemmas/Magnetar_CT.ec — BGL leakage-model CT lemmas Structural simplification vs Pulsar: SLH-DSA SignDeterministic is straight-line (no rejection-sampling kappa loop), so Magnetar has 2 atomic byte-walk axioms (combine + sign monolithic) instead of Pulsar v8's 14-axiom cascade. The Shamir/Lagrange algebra is shared with Pulsar's bridge (cross-cited; byte-wise GF(257) is identical). Bridge doc (proofs/lean-easycrypt-bridge.md) cross-cites the 4 Pulsar Shamir axioms and adds 2 Magnetar-specific entries (mix_to_seed_first_arg_injective + derive_pk_is_slhdsa_pk_from_seed).