mirror of
https://github.com/luxfi/magnetar.git
synced 2026-07-27 02:53:47 +00:00
Hanzo AI
2b0542d3ff
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