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

Files

T

History

zeekay 975898ac1d jasmin: lib + slh-dsa + threshold sources for N1-analog byte-equality

Jasmin scaffolding for the Magnetar high-assurance track, mirroring
Pulsar's structure but specialized to SLH-DSA-SHAKE-192s. Surface area:

lib/ — shared protocol primitives:
  magnetar_params.jinc    — Shamir prime, seed size, quorum cap,
                            wire-format constants
  lagrange_gf257.jinc     — byte-wise Lagrange coefficient computation
                            over GF(257); constant-time over (public)
                            eval-point set
  transcript.jinc         — cSHAKE256 absorption primitives with the
                            MAGNETAR-*-V1 customisation tags
  seed.jinc               — pack_bytesum_be: byteSum vector → big-
                            endian byte string for the
                            MAGNETAR-SEED-SHARE-V1 mix

threshold/ — protocol-layer .jazz files:
  round1.jazz             — per-party Round-1 commit (mask derive,
                            share mask, D_i digest)
  round2.jazz             — per-party Round-2 reveal (mask || masked)
  combine.jazz            — aggregator: commit re-derive, Lagrange
                            reconstruct, mix-to-seed, SLH-DSA dispatch

slh-dsa/ — single-party reference (libjade-SLH-DSA when upstream
            lands; today routes through cloudflare/circl). README +
            fetch.sh skeleton.

Structural simplification: ~600 LOC vs Pulsar's ~1500 LOC. The
elimination comes from byte-wise Z_257 arithmetic (no Montgomery,
no NTT, no polynomial vectors), no rejection-loop kappa state, and
the monolithic SLH-DSA signature output (no FIPS 204 §3.5.5
c_tilde/z/h decomposition).

The .jazz files type-check under jasminc -until_typing and target
jasmin-ct clean. The CI gate scripts/checks/jasmin.sh is skip-
friendly if jasminc is not on PATH.

2026-05-19 08:39:06 -07:00

fetch.sh

jasmin: lib + slh-dsa + threshold sources for N1-analog byte-equality

2026-05-19 08:39:06 -07:00

README.md

jasmin: lib + slh-dsa + threshold sources for N1-analog byte-equality

2026-05-19 08:39:06 -07:00

README.md

SLH-DSA single-party Jasmin source (placeholder)

Magnetar's single-party path routes through cloudflare/circl/sign/slhdsa in production. This directory holds the future home for the formosa-crypto upstream libjade-SLH-DSA sources when they land.

Current upstream status (as of 2026-05)

The formosa-crypto libjade project (https://github.com/formosa-crypto/libjade) ships Jasmin sources and EasyCrypt proofs for:

ML-KEM (Kyber, NIST PQC ML-KEM standard)
ML-DSA (Dilithium, FIPS 204 — used by Pulsar)
Curve25519 + Poly1305 (classical)

SLH-DSA (FIPS 205, SPHINCS+) Jasmin sources are not yet upstream. There is community work in progress; see the formosa-crypto issue tracker for the canonical pointer.

What ships in this directory

This README pointing at upstream.
A fetch.sh script that, when libjade-SLH-DSA lands, pins the upstream commit and clones the relevant subdirectory into this dir on-demand (mirroring the pattern Pulsar uses for libjade ML-DSA-65).

The fetch script is stub today — it prints a clear notice that libjade-SLH-DSA is not yet upstream and exits 0 (skip-friendly).

Long-term plan

When libjade-SLH-DSA lands:

fetch.sh pins the upstream commit and pulls the subtree.
../proofs/easycrypt/lemmas/SLHDSA_Functional.ec becomes a require import against the libjade EasyCrypt theory.
The sign_body_compute_sig_spec axiom in ../proofs/easycrypt/Magnetar_N1_Sign_Refinement.ec becomes a discharged lemma against the libjade-extracted Jasmin.

The constant-time gate (scripts/checks/jasmin.sh) currently treats this directory as advisory: any .jazz files here will be run through jasmin-ct --infer and findings logged, but not blocking. The threshold-layer .jazz files in ../threshold/ are the BLOCKING CT gate.

Why this matters (production)

The current production routing is via cloudflare/circl/sign/slhdsa — the standard Go FIPS 205 reference, NIST-validated and community-audited. Routing through libjade-SLH-DSA when it lands would give us formal CT artifacts at the single-party layer to match Pulsar's libjade-ML-DSA-65 setup; until then, the trust model relies on Cloudflare's CIRCL upstream review.