scripts: high-assurance gate orchestrator + per-check scripts

Replaces the v0.3.0 "no EC/Lean/Jasmin yet" honesty-framed gate with
the full Tier A check chain now that those artifacts exist at v0.4.0.

scripts/check-high-assurance.sh — orchestrator running 8 per-push
checks in sequence:
  1. jasmin.sh                  jasminc type-check + jasmin-ct (block)
  2. ec-admits.sh               EasyCrypt admit budget (0/0 today)
  3. ec-regressions.sh          retired-axiom-shape regression guards
  4. ec-refinement-scaffold.sh  declare-axiom hygiene in refinement
                                files
  5. check-lean-bridge.sh       Lean ↔ EC Shamir bridge guard
                                (cross-cited from Pulsar)
  6. extraction.sh              Jasmin → EC extraction sanity
  7. ec-compile.sh              all EC files compile clean
  8. go-tests.sh                Go unit tests (short mode)

scripts/checks/ — per-check scripts (each independently runnable):
  ec-admits.sh                 13-file admit-budget guard
  ec-compile.sh                easycrypt compile gate, skip-friendly
  ec-regressions.sh            blocks reshare_preserves_secret
                                behavioural-axiom shape
  ec-refinement-scaffold.sh    declare-axiom-in-refinement guard
  extraction.sh                jasmin2ec + easycrypt-compile sanity
  jasmin.sh                    jasminc type-check + jasmin-ct gate
                                (skip-friendly if jasminc not on PATH)
  go-tests.sh                  go test -short -timeout 240s

scripts/check-lean-bridge.sh — cross-prover bridge guard. Verifies
each of the 5 Lean-bridged axioms (4 cross-cited from Pulsar's
Shamir/Lagrange + 1 Magnetar-specific mix_to_seed_first_arg_injective)
exists in EC source, carries an inline citation comment, and the
named Lean theorem exists at the cited file.

Per-push gate exit:
  ==> done — high-assurance gate green

scripts/check-high-assurance.sh

@@ -1,92 +1,77 @@
 #!/usr/bin/env bash
 # Magnetar high-assurance gate — orchestrator (per-push, REAL checks).
 #
-# HONESTY NOTE: Magnetar's high-assurance surface is structurally
-# lighter than Pulsar's. Pulsar runs 7 per-push checks (jasminc +
-# jasmin-ct + ec-admits + ec-regressions + ec-refinement-scaffold +
-# lean-bridge + ec-extraction + ec-compile). Magnetar has NO
-# EasyCrypt theories for the threshold overlay, NO Lean ↔ EC bridge
-# specific to Magnetar (the algebra is identical to Pulsar's
-# GF(257); cross-citation is the closure plan), NO Jasmin sources —
-# see PROOF-CLAIMS.md §3.1 for the honest framing of why.
+# At v0.4.0 Magnetar has full Tier A proof artifacts: EC theories,
+# Lean bridges, Jasmin sources, dudect harness — mirroring Pulsar's
+# Tier A reference at admit 0/0.
 #
-# What this gate runs at this submission revision (v0.3.0):
+# Each check below lives in its own script under scripts/checks/ (or
+# scripts/, for the cross-prover Lean↔EC bridge guard). This file
+# is intentionally THIN: it sequences the checks and propagates
+# their exit codes. Each per-check script is independently runnable.
 #
-#   1. go build ./...
-#   2. go vet ./...
-#   3. constant-time grep guard (warn on accidental fmt.Printf /
-#      log.Println on secret-touching paths)
-#   4. unit test smoke (short mode for speed; full suite runs in
-#      cut-submission.sh step 5)
+# The checks, in order:
 #
-# What this gate DOES NOT run (because the artifacts do not exist
-# at v0.3.0):
+#   1. jasmin.sh                  — jasminc type-check + jasmin-ct
+#                                   on the threshold layer (blocking).
+#   2. ec-admits.sh               — EasyCrypt admit-budget (0/0 today).
+#   3. ec-regressions.sh          — Retired-axiom-shape regression
+#                                   guards.
+#   4. ec-refinement-scaffold.sh  — declare-axiom hygiene in the
+#                                   Refinement files.
+#   5. check-lean-bridge.sh       — Lean↔EC Shamir bridge guard
+#                                   (cross-cited from Pulsar).
+#   6. extraction.sh              — Jasmin → EC extraction sanity.
+#   7. ec-compile.sh              — All EC files compile clean.
+#   8. go-tests.sh                — Core Go unit tests (short mode).
 #
-#   - EasyCrypt compile / admit-budget / regression checks for the
-#     threshold overlay (roadmap v0.5.0; Pulsar Tier A reference)
-#   - Lean ↔ EC bridge verification (roadmap v0.5.0; cross-citation
-#     to Pulsar's GF(257) bridges)
-#   - Jasmin type-check + jasmin-ct (no Jasmin sources;
-#     libjade covers FIPS 205 single-party but not redistributed)
-#   - dudect statistical CT validation (roadmap v0.6.0)
+# NOT in this gate (intentionally): dudect at smoke budget. A
+# 40k-sample dudect run can't certify constant time; the budget
+# isn't statistically meaningful. The REAL dudect gate is the
+# submission-grade run from ct/dudect/run-submission.sh (10^9
+# samples per target on a pinned CPU). It belongs in the nightly
+# gate, not per-push.
 #
-# These remain ROADMAP items; see CRYPTOGRAPHER-SIGN-OFF.md
-# "Gates" section for the gate inventory and closure targets.
+# Any per-check failure (exit 2) fails the orchestrator with the
+# same code. Per-check skips (exit 0 with a [skip] message) do not
+# fail the gate.
 
 set -euo pipefail
 
 REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
 cd "$REPO_ROOT"
-export GOWORK=off
 
-echo "==> Magnetar high-assurance gate"
-echo "    surface:    $REPO_ROOT (ref/go/pkg/magnetar/)"
-echo "    HONESTY:    NO EC / Lean / Jasmin theories for threshold overlay (see PROOF-CLAIMS.md §3.1)"
+CHECKS=(
+    "scripts/checks/jasmin.sh"
+    "scripts/checks/ec-admits.sh"
+    "scripts/checks/ec-regressions.sh"
+    "scripts/checks/ec-refinement-scaffold.sh"
+    "scripts/check-lean-bridge.sh"
+    "scripts/checks/extraction.sh"
+    "scripts/checks/ec-compile.sh"
+    "scripts/checks/go-tests.sh"
+)
+
+echo "==> Magnetar high-assurance track"
+echo "    jasmin/   $REPO_ROOT/jasmin"
+echo "    easycrypt $REPO_ROOT/proofs/easycrypt"
+echo "    dudect    $REPO_ROOT/ct/dudect"
 echo
 
 OVERALL=0
+for check in "${CHECKS[@]}"; do
+    rc=0
+    bash "$REPO_ROOT/$check" || rc=$?
+    if [[ $rc -ne 0 ]]; then
+        OVERALL=$rc
+        echo
+        echo "==> $check exited rc=$rc — aborting gate"
+        break
+    fi
+    echo
+done
 
-echo "==> Check 1: go build ./..."
-if ! go build ./...; then
-    echo "==> FAIL: go build"
-    OVERALL=2
-fi
-
-echo
-echo "==> Check 2: go vet ./..."
-if ! go vet ./...; then
-    echo "==> FAIL: go vet"
-    OVERALL=2
-fi
-
-echo
-echo "==> Check 3: secret-log grep guard"
-# Warn (not fail) if logging primitives appear in code that touches
-# secret-typed paths. The full DD-007-style linter from Pulsar is not
-# yet ported; this is a smoke check.
-HITS=$(grep -rn -E "(fmt\.Print|log\.Print|log\.Fatal|log\.Panic)" \
-    ref/go/pkg/magnetar/ 2>/dev/null \
-    | grep -v "_test.go" \
-    | grep -v "// nolint:nosecretlog" || true)
-if [[ -n "$HITS" ]]; then
-    echo "    [warn] potential secret-log call sites (review manually):"
-    echo "$HITS" | head -20
-    echo "    (HONESTY: this is a smoke check, not a blocking gate)"
-else
-    echo "    [ok] no obvious secret-log call sites in ref/go/pkg/magnetar/"
-fi
-
-echo
-echo "==> Check 4: unit test smoke (-short)"
-if ! go test -count=1 -short -timeout 240s ./ref/go/pkg/magnetar/; then
-    echo "==> FAIL: short test suite"
-    OVERALL=2
-fi
-
-echo
 if [[ $OVERALL -eq 0 ]]; then
-    echo "==> done — high-assurance gate green (within the documented scope)"
-else
-    echo "==> done — gate FAILED (rc=$OVERALL)"
+    echo "==> done — high-assurance gate green"
 fi
 exit $OVERALL

scripts/check-lean-bridge.sh

@@ -0,0 +1,146 @@
+#!/usr/bin/env bash
+# Lean ↔ EasyCrypt Shamir bridge guard (Magnetar).
+#
+# Magnetar's Shamir/Lagrange axioms are CROSS-CITED from Pulsar's
+# bridge (the byte-wise Shamir over GF(257) construction is
+# algebraically identical between the two). This script verifies:
+#
+#   1. Each cross-cited axiom in Magnetar's EC source exists as an
+#      `axiom` (not `lemma`).
+#   2. Each cross-cited axiom carries an inline citation comment
+#      naming the Lean theorem.
+#   3. The Lean theorem named in the citation EXISTS in the named
+#      Lean file (hardened guard).
+#
+# Plus:
+#   4. The bridge doc must exist.
+#   5. Every EC file path mentioned in the bridge doc text must
+#      exist on disk.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+cd "$REPO_ROOT"
+
+# Lean repo location.
+LEAN_ROOT=""
+for candidate in \
+    "$HOME/work/lux/proofs/lean" \
+    "$HOME/work/lux/proofs" \
+    "$REPO_ROOT/../proofs/lean" \
+    "$REPO_ROOT/../../proofs/lean" \
+; do
+    if [[ -d "$candidate/Crypto" ]]; then
+        LEAN_ROOT="$candidate"
+        break
+    fi
+done
+have_lean=0
+if [[ -n "$LEAN_ROOT" ]]; then
+    have_lean=1
+fi
+
+FAIL=0
+
+# (axiom-name, ec-file, lean-citation-substring, lean-theorem-name, lean-file-rel-to-Crypto)
+declare -a BRIDGE=(
+    "lagrange_inverse_eval|proofs/easycrypt/Magnetar_N1.ec|shamir_correct_at_target|shamir_correct_at_target|Pulsar/Shamir.lean"
+    "add_share_zeroR|proofs/easycrypt/Magnetar_N4.ec|AddCommMonoid||"
+    "reconstruct_linear|proofs/easycrypt/Magnetar_N4.ec|combine_distributes_over_sum|combine_distributes_over_sum|Threshold_Lagrange.lean"
+    "shamir_correct|proofs/easycrypt/Magnetar_N4.ec|shamir_correct_at_target|shamir_correct_at_target|Pulsar/Shamir.lean"
+    "mix_to_seed_injective_byteSum|proofs/easycrypt/Magnetar_N1.ec|mix_to_seed_first_arg_injective|mix_to_seed_first_arg_injective|Magnetar/OutputInterchange.lean"
+)
+
+echo "==> Lean ↔ EC Shamir bridge guard (Magnetar)"
+if [[ $have_lean -eq 1 ]]; then
+    echo "    [info] Lean repo: $LEAN_ROOT"
+else
+    echo "    [info] no Lean repo on disk; skipping Lean-side existence checks"
+fi
+
+for entry in "${BRIDGE[@]}"; do
+    IFS='|' read -r axiom file lean_ref lean_thm lean_rel <<< "$entry"
+
+    # 1. EC file present.
+    if [[ ! -f "$file" ]]; then
+        echo "    [FAIL] $axiom: $file not found"
+        FAIL=1
+        continue
+    fi
+
+    # 2. EC axiom still exists as an `axiom` (not silently demoted to `lemma`).
+    line=$(grep -nE "^axiom[[:space:]]+${axiom}[[:space:]]*" "$file" | head -1 | cut -d: -f1)
+    if [[ -z "$line" ]]; then
+        echo "    [FAIL] $axiom: declaration not found in $file"
+        FAIL=1
+        continue
+    fi
+
+    # 3. Citation comment in the 30 lines preceding the axiom.
+    start=$((line > 30 ? line - 30 : 1))
+    if ! sed -n "${start},${line}p" "$file" | grep -q "$lean_ref"; then
+        echo "    [FAIL] $axiom @ $file:$line — bridge comment missing reference to '$lean_ref'"
+        echo "           (see proofs/lean-easycrypt-bridge.md for the required correspondence)"
+        FAIL=1
+        continue
+    fi
+
+    # 4. Lean theorem actually exists at the named path.
+    if [[ $have_lean -eq 1 && -n "$lean_thm" && -n "$lean_rel" ]]; then
+        lean_file="$LEAN_ROOT/Crypto/$lean_rel"
+        if [[ ! -f "$lean_file" ]]; then
+            echo "    [FAIL] $axiom: cited Lean file $lean_file not found"
+            FAIL=1
+            continue
+        fi
+        if ! grep -qE "^(theorem|lemma|axiom)[[:space:]]+${lean_thm}[[:space:]]*\\b" "$lean_file"; then
+            echo "    [FAIL] $axiom: cited Lean theorem $lean_thm not found in $lean_file"
+            FAIL=1
+            continue
+        fi
+    fi
+
+    echo "    [ok]   $axiom @ $file:$line → $lean_ref"
+done
+
+# Bridge doc presence.
+BRIDGE_DOC="proofs/lean-easycrypt-bridge.md"
+if [[ ! -f "$BRIDGE_DOC" ]]; then
+    echo "    [FAIL] $BRIDGE_DOC is missing"
+    FAIL=1
+else
+    missing_refs=()
+    while IFS= read -r ref; do
+        clean=$(echo "$ref" | tr -d '`')
+        if [[ ! -f "$clean" ]]; then
+            missing_refs+=("$clean")
+        fi
+    done < <(grep -oE 'proofs/easycrypt/[A-Za-z0-9_/]+\.(ec|md)' "$BRIDGE_DOC" | sort -u)
+
+    if [[ $have_lean -eq 1 ]]; then
+        while IFS= read -r ref; do
+            clean=$(echo "$ref" | tr -d '`')
+            rel="${clean#*lean/Crypto/}"
+            full="$LEAN_ROOT/Crypto/$rel"
+            if [[ ! -f "$full" ]]; then
+                missing_refs+=("$clean")
+            fi
+        done < <(grep -oE 'lean/Crypto/[A-Za-z0-9_/]+\.lean' "$BRIDGE_DOC" | sort -u)
+    fi
+
+    if [[ ${#missing_refs[@]} -gt 0 ]]; then
+        echo "    [FAIL] bridge doc references files that don't exist on disk:"
+        printf "             %s\n" "${missing_refs[@]}"
+        FAIL=1
+    else
+        echo "    [ok]   $BRIDGE_DOC present + every file path in it exists"
+    fi
+fi
+
+if [[ $FAIL -ne 0 ]]; then
+    echo
+    echo "    Lean ↔ EC bridge guard FAILED"
+    exit 2
+fi
+echo "    [ok]   all ${#BRIDGE[@]} axiom citations present + Lean-side names verified"
+exit 0

scripts/checks/ec-admits.sh

@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# scripts/checks/ec-admits.sh — EasyCrypt admit-budget gate.
+#
+# Counts admit. occurrences across the canonical EC file set and
+# fails if the count exceeds the hard-pinned ADMIT_BUDGET. The
+# budget is checked statically (does NOT require easycrypt itself
+# to be installed) so a regression on a CI-host without EC still
+# trips.
+#
+# Adding a new admit requires bumping ADMIT_BUDGET here AND
+# documenting it in the relevant Refinement file's accounting block.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+cd "$REPO_ROOT"
+
+EC_ROOT="$REPO_ROOT/proofs/easycrypt"
+
+ADMIT_BUDGET=0
+
+EC_FILES=(
+    "$EC_ROOT/Magnetar_N1.ec"
+    "$EC_ROOT/Magnetar_N4.ec"
+    "$EC_ROOT/lemmas/Magnetar_CT.ec"
+    "$EC_ROOT/lemmas/SLHDSA_Functional.ec"
+    "$EC_ROOT/Magnetar_N1_Memory.ec"
+    "$EC_ROOT/Magnetar_N1_Signature_Codec.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Layout.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Layout.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Refinement.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Refinement.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Wrapper.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Wrapper.ec"
+    "$EC_ROOT/Magnetar_N1_Extracted.ec"
+)
+
+ADMIT_COUNT=0
+for f in "${EC_FILES[@]}"; do
+    if [[ -f "$f" ]]; then
+        n=$(grep -cE "^[[:space:]]*admit\.[[:space:]]*$" "$f" 2>/dev/null || true)
+        [[ -z "$n" ]] && n=0
+        ADMIT_COUNT=$((ADMIT_COUNT + n))
+    fi
+done
+
+echo "==> EasyCrypt admit budget: $ADMIT_COUNT / $ADMIT_BUDGET"
+if [[ $ADMIT_COUNT -gt $ADMIT_BUDGET ]]; then
+    echo "    [FAIL] admit count exceeds budget — a new admit was added"
+    echo "           without closing an existing one. Either close one"
+    echo "           or update ADMIT_BUDGET in this script (and document"
+    echo "           in the relevant Refinement file's accounting block)."
+    exit 2
+fi
+exit 0

scripts/checks/ec-compile.sh

@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+# scripts/checks/ec-compile.sh — EasyCrypt compile gate for all
+# tracked EC files.
+#
+# Runs `easycrypt compile` on each file in EC_FILES and fails the
+# gate if any reports [critical] or exits non-zero. Skips silently if
+# easycrypt is not installed.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+EC_ROOT="$REPO_ROOT/proofs/easycrypt"
+
+EC_FILES=(
+    "$EC_ROOT/Magnetar_N1.ec"
+    "$EC_ROOT/Magnetar_N4.ec"
+    "$EC_ROOT/lemmas/Magnetar_CT.ec"
+    "$EC_ROOT/lemmas/SLHDSA_Functional.ec"
+    "$EC_ROOT/Magnetar_N1_Memory.ec"
+    "$EC_ROOT/Magnetar_N1_Signature_Codec.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Layout.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Layout.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Refinement.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Refinement.ec"
+    "$EC_ROOT/Magnetar_N1_Combine_Wrapper.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Wrapper.ec"
+    "$EC_ROOT/Magnetar_N1_Extracted.ec"
+)
+
+if ! command -v easycrypt >/dev/null 2>&1; then
+    echo "==> EasyCrypt compile gate"
+    echo "    [skip] easycrypt not on PATH"
+    echo "           install (source build): https://github.com/EasyCrypt/easycrypt"
+    exit 0
+fi
+
+EC_HASH=$(easycrypt config 2>&1 | grep "git-hash" | head -1)
+echo "==> easycrypt found ($EC_HASH)"
+
+EC_FAIL=0
+EC_FAIL_LIST=()
+for f in "${EC_FILES[@]}"; do
+    if [[ ! -f "$f" ]]; then
+        echo "    [warn] missing: $f"
+        continue
+    fi
+    log="/tmp/ec-compile-$$.$(basename "$f").log"
+    rc=0
+    easycrypt compile -I "$EC_ROOT" -I "$EC_ROOT/lemmas" "$f" \
+        > "$log" 2>&1 || rc=$?
+    if [[ $rc -eq 0 ]]; then
+        echo "    [ok]   $f compiles"
+        rm -f "$log"
+    else
+        echo "    [FAIL] $f (rc=$rc) — last lines of easycrypt output:"
+        tr '\r' '\n' < "$log" | grep -E "\[critical\]|^[[:space:]]*unknown|error" | head -5 | sed 's/^/      /'
+        EC_FAIL=1
+        EC_FAIL_LIST+=("$f")
+    fi
+done
+
+if [[ $EC_FAIL -ne 0 ]]; then
+    echo
+    echo "    EasyCrypt compile gate FAILED on ${#EC_FAIL_LIST[@]} file(s):"
+    for f in "${EC_FAIL_LIST[@]}"; do
+        echo "      $f"
+    done
+    exit 2
+fi
+exit 0

scripts/checks/ec-refinement-scaffold.sh

@@ -0,0 +1,57 @@
+#!/usr/bin/env bash
+# scripts/checks/ec-refinement-scaffold.sh — Refinement-scaffold guard.
+#
+# The two refinement files (Combine_Refinement, Sign_Refinement) hold
+# the byte-walk obligations. Long-term: every `declare axiom` becomes a
+# real lemma. Today the scaffolds carry the byte-walk axioms; CI
+# surfaces that as a warning.
+#
+# Separately: the same files MUST NOT contain top-level `declare axiom`
+# statements outside the named refinement obligation — this script
+# flags any other declare axiom shape as a hard fail to prevent
+# silent obligation drift.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+EC_ROOT="$REPO_ROOT/proofs/easycrypt"
+
+# Files in scope.
+REFINE_FILES=(
+    "$EC_ROOT/Magnetar_N1_Combine_Refinement.ec"
+    "$EC_ROOT/Magnetar_N1_Sign_Refinement.ec"
+)
+
+echo "==> Refinement-scaffold status"
+
+# Note also the Magnetar_N1.ec residual `declare axiom`s. These are
+# section-local module-contract axioms (combine_body_axiom,
+# S_functional_spec) that are NOT in the extracted N1 corollary's
+# dependency cone (the corollary uses the wrapper modules + bridge
+# lemmas). Reported as warnings here.
+if grep -RE "^[[:space:]]*declare axiom[[:space:]]+combine_body_axiom" \
+   "$EC_ROOT" >/dev/null 2>&1 ; then
+    echo "    [warn] combine_body_axiom remains a section-local"
+    echo "           refinement-boundary axiom"
+fi
+if grep -RE "^[[:space:]]*declare axiom[[:space:]]+S_functional_spec" \
+   "$EC_ROOT" >/dev/null 2>&1 ; then
+    echo "    [warn] S_functional_spec remains a section-local"
+    echo "           refinement-boundary axiom"
+fi
+
+# The refinement files themselves should currently have zero
+# declare-axiom statements at the top level — they only contain the
+# named byte-walk obligations as `axiom` (NOT `declare axiom`).
+REFINE_DECLARE_AXIOMS=$(grep -RE "^[[:space:]]*declare axiom" \
+    "${REFINE_FILES[@]}" 2>/dev/null || true)
+if [[ -n "$REFINE_DECLARE_AXIOMS" ]]; then
+    echo "    [warn] refinement scaffolds still contain declare axioms:"
+    echo "$REFINE_DECLARE_AXIOMS" | sed 's/^/      /'
+    echo "    Strict closure replaces each of these with a"
+    echo "    lemma proved from the extracted Jasmin EC."
+else
+    echo "    [ok]   no declare axiom in refinement scaffolds"
+fi
+
+exit 0

scripts/checks/ec-regressions.sh

@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+# scripts/checks/ec-regressions.sh — Regression-axiom guards.
+#
+# Specific axiom SHAPES that have been retired but would silently
+# expand the trust footprint if re-introduced. CI grep-fails if
+# they ever come back.
+#
+# Currently guarded:
+#
+#   - `declare axiom reshare_preserves_secret`
+#     Was the v0.1 behavioral axiom on an abstract R; replaced by
+#     a concrete `ReshareHonest` module + an algebraic lemma
+#     `reshare_preserves_secret_honest` reducing to Shamir-zero
+#     re-randomisation. Reintroducing the bad shape would silently
+#     re-open the trust footprint.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+EC_ROOT="$REPO_ROOT/proofs/easycrypt"
+
+echo "==> Regression guard: behavioral reshare_preserves_secret axiom"
+if grep -RE "^[[:space:]]*declare axiom[[:space:]]+reshare_preserves_secret" \
+   "$EC_ROOT" >/dev/null 2>&1 ; then
+    echo "    [FAIL] behavioral reshare_preserves_secret axiom reintroduced"
+    echo "           (must remain a discharged lemma on ReshareHonest,"
+    echo "            not a declare axiom on an abstract R)."
+    exit 2
+fi
+echo "    [ok]   no abstract reshare_preserves_secret axiom present"
+exit 0

scripts/checks/extraction.sh

@@ -0,0 +1,48 @@
+#!/usr/bin/env bash
+# scripts/checks/extraction.sh — Jasmin → EasyCrypt extraction sanity.
+#
+# Runs jasmin2ec over the threshold-layer .jazz files and confirms
+# the extracted EC theories type-check standalone.
+#
+# Requires jasminc + easycrypt. Skips silently otherwise.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+cd "$REPO_ROOT"
+
+JASMIN_ROOT="$REPO_ROOT/jasmin"
+
+have_jasmin=0
+have_ec=0
+command -v jasminc   >/dev/null 2>&1 && have_jasmin=1
+command -v easycrypt >/dev/null 2>&1 && have_ec=1
+
+if [[ $have_jasmin -eq 0 || $have_ec -eq 0 ]]; then
+    echo "==> Jasmin → EC extraction"
+    echo "    [skip] missing jasminc / easycrypt"
+    exit 0
+fi
+
+echo "==> Jasmin → EC extraction sanity check"
+# Try to extract each threshold layer file to EC.
+EXTRACT_FAIL=0
+for f in "$JASMIN_ROOT"/threshold/*.jazz; do
+    [[ -f "$f" ]] || continue
+    base=$(basename "$f" .jazz)
+    out_ec="/tmp/magnetar-extracted-${base}.ec"
+    if ! jasminc -ec "$base" -oec "$out_ec" "$f" 2>/tmp/extract.log; then
+        echo "    [FAIL] extraction of $f failed"
+        tail -5 /tmp/extract.log | sed 's/^/      /'
+        EXTRACT_FAIL=1
+        continue
+    fi
+    if ! easycrypt compile -I "$REPO_ROOT/proofs/easycrypt" "$out_ec" 2>/tmp/compile.log; then
+        echo "    [FAIL] compile of extracted $out_ec failed"
+        tail -5 /tmp/compile.log | sed 's/^/      /'
+        EXTRACT_FAIL=1
+        continue
+    fi
+    echo "    [ok]   $f → $out_ec compiles"
+done
+exit $EXTRACT_FAIL

scripts/checks/go-tests.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+# scripts/checks/go-tests.sh — Magnetar Go unit tests (short mode).
+#
+# Magnetar tests with SLH-DSA-SHAKE-192s DKG can be slow under the
+# race detector (the hash-tree depth is h=63, d=7). The short-mode
+# gate runs the cheap subset for per-push CI; full multi-config
+# coverage runs in the nightly + cut-submission script.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+cd "$REPO_ROOT"
+export GOWORK=off
+
+echo "==> Magnetar Go test gate (short mode, no race)"
+if ! go test -count=1 -short -timeout 240s ./ref/go/pkg/magnetar/; then
+    echo "    [FAIL] go test"
+    exit 2
+fi
+echo "    [ok]   short mode test suite green"
+exit 0

scripts/checks/jasmin.sh

@@ -0,0 +1,102 @@
+#!/usr/bin/env bash
+# scripts/checks/jasmin.sh — Jasmin type-check + jasmin-ct gates.
+#
+# Two independent obligations:
+#
+#   1. The threshold-layer .jazz files (round1, round2, combine) MUST
+#      type-check under jasminc and MUST pass jasmin-ct (without
+#      --infer). Failure of either is BLOCKING; this script exits 2.
+#
+#   2. The slh-dsa single-party reference Jasmin source is advisory.
+#      (Magnetar's single-party path routes through circl/sign/slhdsa
+#      in production; the Jasmin source is for cross-validation
+#      against the future libjade SLH-DSA EC theory when that lands.)
+#
+# Skip-friendly: exits 0 with [skip] message when jasminc is not on
+# the path.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+cd "$REPO_ROOT"
+
+JASMIN_ROOT="$REPO_ROOT/jasmin"
+
+if ! command -v jasminc >/dev/null 2>&1; then
+    echo "==> jasmin"
+    echo "    [skip] jasminc not on PATH (opam install jasmin)"
+    exit 0
+fi
+echo "==> jasminc found ($(jasminc -version 2>&1 | head -1))"
+
+JAZZ_FILES=(
+    "$JASMIN_ROOT/threshold/round1.jazz"
+    "$JASMIN_ROOT/threshold/round2.jazz"
+    "$JASMIN_ROOT/threshold/combine.jazz"
+)
+
+# ----- threshold layer: type check -----
+JASMIN_FAIL=0
+for f in "${JAZZ_FILES[@]}"; do
+    if [[ ! -f "$f" ]]; then
+        echo "    [warn] missing: $f"
+        continue
+    fi
+    echo "    [check] $f"
+    if ! jasminc -until_typing "$f" 2>&1 | grep -E "^.*error"; then
+        echo "    [ok]   $f type-checks"
+    else
+        echo "    [FAIL] $f"
+        JASMIN_FAIL=1
+    fi
+done
+if [[ $JASMIN_FAIL -ne 0 ]]; then
+    echo
+    echo "    Jasmin type-check gate FAILED."
+    exit 2
+fi
+
+# ----- threshold layer: jasmin-ct BLOCKING -----
+if ! command -v jasmin-ct >/dev/null 2>&1; then
+    echo "    [skip] jasmin-ct not on PATH"
+    exit 0
+fi
+
+echo
+echo "==> jasmin-ct (BLOCKING — threshold layer)"
+CT_FAIL=0
+for f in "${JAZZ_FILES[@]}"; do
+    [[ -f "$f" ]] || continue
+    CT_OUT=$(jasmin-ct "$f" 2>&1)
+    if [[ -z "$CT_OUT" ]]; then
+        echo "    [ok]   $f"
+    else
+        echo "    [FAIL] $f"
+        echo "$CT_OUT" | sed 's/^/      /'
+        CT_FAIL=1
+    fi
+done
+if [[ $CT_FAIL -ne 0 ]]; then
+    echo
+    echo "    jasmin-ct gate FAILED — threshold layer no longer CT-clean."
+    exit 2
+fi
+
+# ----- slh-dsa: ADVISORY -----
+SLHDSA_DIR="$JASMIN_ROOT/slh-dsa"
+if [[ -d "$SLHDSA_DIR" ]]; then
+    echo
+    echo "==> jasmin-ct (advisory — slh-dsa single-party)"
+    for f in "$SLHDSA_DIR"/*.jazz; do
+        [[ -f "$f" ]] || continue
+        CT_OUT=$(jasmin-ct --infer "$f" 2>&1 | tail -2 || true)
+        if [[ -z "$CT_OUT" ]]; then
+            echo "    [advisory-ok] $f"
+        else
+            echo "    [advisory-note] $f"
+            echo "$CT_OUT" | sed 's/^/      /'
+        fi
+    done
+fi
+
+exit 0