Files
pulsar/scripts/check-high-assurance.sh
Hanzo AI ac293cbe49 consolidate: merge pulsar-mptc submission framework into canonical luxfi/pulsar
Single repo, one canonical impl + spec + proofs + KAT + cut tool.

Per "ONE and ONLY ONE way to do things" the prior dual-repo split
(luxfi/pulsar = production library, luxfi/pulsar-mptc = NIST MPTC
submission framework) is collapsed into a single canonical home at
github.com/luxfi/pulsar. SINGLE-IMPL-PLAN.md (now marked COMPLETED)
describes the steps; this commit lands the final step.

Files moved (89 new):
  16 submission docs (SUBMISSION, NIST-SUBMISSION, SPEC, SUITE,
     PATENTS, AXIOM-INVENTORY, PROOF-CLAIMS, FIPS-TRACEABILITY,
     TRUSTED-COMPUTING-BASE, HANZO-CRYPTO-SUITE, INFORMATION-
     ARCHITECTURE, ROADMAP, CHANGELOG, SYNC-STATUS, STATUS-
     SUBMISSION-READINESS, SINGLE-IMPL-PLAN)
  10 docs/ supplements (ietf-draft-skeleton, magnetar, evaluation,
     patent-claims, x-wing-sig, design-decisions, family-architecture,
     threat-model, nist-mptc-category, patent-notes-draft)
  19 proofs/ (13 EC theories + 2 EC lemmas + 4 metadata/READMEs +
     lean-easycrypt-bridge.md)
  14 jasmin/ (lib/* + ml-dsa-65 fetch + threshold/{combine,round1,
     round2}.jazz + READMEs)
  10 ct/dudect/ (Makefile, combine_ct.go, dudect_combine.c,
     dudect_compat.h, dudect_verify.c, fetch.sh, README, run-
     submission.sh, verify_ct.go) + ct/jasmin-ct-libjade.md
  1 .github/workflows/ci.yml
  1 test/interoperability/n1_class_test.go (19/19 N1 subtests)
  1 bench/results/REPORT.md
  11 scripts/ (cut-submission, check-high-assurance, check-lean-
     bridge, nightly, extract-jasmin-ec, checks/{ec-admits, ec-
     compile, ec-refinement-scaffold, ec-regressions, extraction,
     jasmin}, checks/test/{go-unit, interop, kat, no-secret-logs})

Files merged (16 overlapping, mptc-canonical chosen because newer +
post-rewire-correct; pulsar versions still bore stale "Pulsar-M" /
"pulsarm" branding):
  README.md, BLOCKERS.md, CONTRIBUTING.md, LICENSE, LICENSING.md,
  SECURITY.md, .gitignore, bench/run_all.sh, vectors/dkg.json (v1.0.7
  regen), scripts/{bench,build,gen_vectors,sbom,test}.sh,
  spec/{pulsar,parameters,system-model}.tex,
  CRYPTOGRAPHER-SIGN-OFF.md (path refs).

Pulsar-only spec supplements preserved:
  spec/{blockers,design-decisions,family-architecture,nist-mptc-
  category,patent-notes,threat-model}.tex.

Path rewrites applied: 158 occurrences across 26 files
  github.com/luxfi/pulsar-mptc -> github.com/luxfi/pulsar
  ~/work/lux/pulsar-mptc/      -> ~/work/lux/pulsar/
  luxfi/pulsar-mptc            -> luxfi/pulsar
  pulsar-mptc/                  -> ./

Narrative collapses (no more two-repo framing):
  SUBMISSION.md "At a glance" — single Repository row
  SYNC-STATUS.md — rewritten to single-repo state
  SINGLE-IMPL-PLAN.md — marked COMPLETED 2026-05-18
  HANZO-CRYPTO-SUITE.md — tier 1 row = single canonical home
  scripts/cut-submission.sh — replace/vendor dance removed; cuts
  directly from in-tree canonical sources

go.mod: dropped mptc's replace directive (no longer needed since this
IS the canonical pulsar repo). Module path is github.com/luxfi/pulsar.
Deps: cloudflare/circl v1.6.3, golang.org/x/crypto v0.32.0.

Verification:
  GOWORK=off go build ./...              PASS
  GOWORK=off go test -count=1 ./...      PASS (1.4s)
  GOWORK=off go test -race ./ref/...     PASS (14.7s)
  go test ./test/interoperability/       PASS (19/19 N1 subtests)
  scripts/check-high-assurance.sh        PASS
  scripts/check-lean-bridge.sh           PASS (5/5 bridges)
  scripts/gen_vectors.sh                 byte-identical replay
  scripts/cut-submission.sh --help       PASS
2026-05-18 19:53:08 -07:00

72 lines
2.5 KiB
Bash
Executable File

#!/usr/bin/env bash
# Pulsar high-assurance gate — orchestrator (per-push, REAL checks).
#
# 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.
#
# The checks, in order:
#
# 1. jasmin.sh — jasminc type-check + jasmin-ct
# on the threshold layer (blocking).
# libjade sign is advisory under #2.
# 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.
# 6. extraction.sh — Jasmin → EC extraction sanity.
# 7. ec-compile.sh — All EC files compile clean.
#
# 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 (scripts/nightly.sh), not per-push.
#
# 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"
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"
)
echo "==> Pulsar 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
if [[ $OVERALL -eq 0 ]]; then
echo "==> done — high-assurance gate green"
fi
exit $OVERALL