spar v0.40.0

v0.40.0 — things that looked like evidence and were not

WHY THIS FOLLOWS v0.37.0 AND NOT v0.39.0. The version bumps for 0.38.0 (#428)
and 0.39.0 (#431) both merged to main with green CI, and neither was ever
tagged: the release automation has no signing key, so it stages a bump and
asks for a signature it cannot produce. Two version windows therefore exist in
git history with no tag, no GitHub Release and no binaries behind them.

They are retired rather than back-filled, deliberately. The tag-point gate
(tools/ci/check-tag-point.sh, #366) refuses a tag that silently excludes
already-landed work unless the tagger acknowledges it in a Tag-Point: trailer
— and a v0.38.0 tag cut today would have to acknowledge that it excludes, among
other things, the v0.39.0 bump itself. Signing that is not honesty, it is
paperwork around an incoherent artifact. Releases go 0.37.0 -> 0.40.0; 0.38.0
and 0.39.0 name Cargo.toml windows that were never published. Nothing is lost
downstream: this project publishes no crate and no npm package, so the gap is
visible only in the GitHub Releases list and the VS Code Marketplace.

THE RELEASE ITSELF. Five features, and one shape between them. Each is a claim
that rendered as evidence while nothing checked it — the v0.36.0 defect class
turned on the guardrails themselves rather than on the code they watch.

  #432  A guard shall not be its own witness.
        REQ-GUARD-GATE-EVIDENCE-002 once asserted, in prose, that "each was
        mutation-tested" — self-reported, unrepeatable, and false in its
        universal form (#405 falsified it by finding two guards whose
        --self-test did NOT catch a mutation of the logic it claimed to
        cover). tools/check_self_test_potency.py replaces the sentence with a
        standing oracle: for each declared mutant it applies the source
        substitution, runs that tool's own --self-test, and asserts the
        self-test now FAILS. A survivor reds the build.

            declared mutants: 4
              CAUGHT  vf-colon-tail        [check_verification_filters.py]
              CAUGHT  vf-none-lenient      [check_verification_filters.py]
              CAUGHT  ls-drop-below-floor  [check_lean_sorries.py]
              CAUGHT  ls-drop-axiom        [check_lean_sorries.py]
            caught: 4   survived: 0   errored: 0

        Including the exact two mutations #405 used to demonstrate the lie.

  #424  A status rivet never sees is not a status. `status:` written into an
        artifact's `fields:` bag is valid YAML, tolerated by the schema, and
        invisible to every lifecycle query — the #370 `release:` defect one
        field over. Six live cases (ARCH-026/-027/-028/-030/-031/-032) each
        carried `fields.status: planned` with no artifact-plane status at all.
        The plane guard generalises from one field to a set rather than
        growing a second bespoke checker beside a working one.

  #430  94 artifacts read as tracked safety traceability while tracked by
        nothing. safety/requirements.yaml and safety/analysis.yaml sit outside
        every rivet.yaml `sources:` path, so rivet never loaded them: no
        status, release or vocabulary guard has ever reached them. A
        clean-room re-derivation found 0 ids unique to either file and the
        loaded safety/stpa/ copies strictly ahead — they were a frozen
        2026-03-10 snapshot. Deleted, with check_safety_sources.py to stop an
        un-sourced safety file returning.

  #429  A count is not a debt until you know what it counts. The third-party
        ratchet listed 14 unparsed models, which reads as 14 units of parser
        debt. Opening all 14 against the source put it at 3: seven are files
        carrying committed git merge-conflict markers, two are AADLv1 unnamed
        connections OSATE also rejects, two are malformed v2. Every row now
        carries a class token, a new row must be classified before it can be
        ratcheted in, and SPAR-DEFECT is asserted exactly — so a real
        too-strict regression can no longer hide in a mixed pile.

  #426  Two numbers stated in prose with nothing under them, both already
        drifted: a doc claiming 117 first-party models against a corpus of
        120 (the guard asked only `> 100`, which catches a broken walk and not
        a growing corpus), and a count of "5414 declarations" nobody can
        reproduce. Plus a CHANGELOG whose first line claimed to document all
        notable changes and stopped 27 releases earlier.

FALSIFICATION. The claim is that these guards can still fail. To falsify it,
run `tools/check_self_test_potency.py` and find a declared mutant that
survives, or mutate any guard's logic in a way its --self-test does not catch.

WHAT IS NOT CLAIMED, and it is the honest ceiling: 15 tools in tools/ carry a
--self-test; the potency table declares mutants for 2 of them. A green run
means "the declared mutants are all caught", never "this suite is complete" —
the tool's own docstring says so, and extending the table to the other 13 is
the obvious next increment. Nor is it claimed that #429's classification makes
the three SPAR-DEFECT parser gaps go away; they are open, reproduced against
this binary, and tracked in #434.

The text above is the message of the signed annotated tag v0.40.0.
Re-derive it, signature and all, with git tag -v v0.40.0.

Verified on this release's own workflow

x86_64-pc-windows-msvc    binary says: spar 0.40.0 == tag implies: spar 0.40.0  + exit 2 contract
aarch64-apple-darwin      binary says: spar 0.40.0 == tag implies: spar 0.40.0  + exit 2 contract
x86_64-unknown-linux-gnu  binary says: spar 0.40.0 == tag implies: spar 0.40.0  + exit 2 contract
aarch64-unknown-linux-gnu ::notice SKIPPED - aarch64 target on x86_64 runner
x86_64-apple-darwin       ::notice SKIPPED - x86_64 target on aarch64 runner

release assets gathered: 13 (floor 10)      # the empty-release guard, #402

And from a user's position, on the published, stripped artifact (the
strip step runs after the assertion above, so this is not the same bytes):

./spar-v0.40.0-aarch64-apple-darwin.tar.gz: OK     # shasum -c against SHA256SUMS.txt
spar 0.40.0                                       # --version
2                                                 # unknown command exit code
test-data/parser/complex_system.aadl: OK          # it actually parses

---

What's Changed

• chore(interop,changelog,repo): gate two drifted counts, and ignore a results file that reads like a claim by @avrabe in #426
• feat(guard): generalise the plane guardrail to catch a fields-nested status (#375) by @avrabe in #424
• chore(release): v0.38.0 by @avrabe in #428
• feat(interop): classify third-party gap rows; ratchet SPAR-DEFECT count exactly (#427) by @avrabe in #429
• feat(guard): delete the two unloaded shadow safety files; guard their return (#375) by @avrabe in #430
• chore(release): v0.39.0 by @avrabe in #431
• feat(guard): mechanise self-test potency with a declared-mutant harness (#405) by @avrabe in #432
• chore(release): v0.40.0 by @avrabe in #433

Full Changelog: v0.37.0...v0.40.0

spar v0.37.0

v0.37.0 — does the reference implementation accept what WE write?

Five commits since v0.36.0. Every conformance test spar had asked one
direction of one question: can spar read the AADL that OSATE wrote? That
direction cannot fail interestingly — a parser that rejects a vendored corpus
fails loudly on the first run and never ships. The direction that bites a user
is the other one: they open OUR model in OSATE and it errors. Nothing measured
it, so nothing was known about it.

Three gates now measure it, over 2015 models: the 120 .aadl files
pulseengine itself writes, the 548 vendored osate/examples, and 1347
third-party models newly vendored here.

  #419  Direction B, in three layers.

        * first_party_legality.rs sweeps all 120 first-party .aadl with
          DECLARED verdicts — the 22 under test-data/negative/** must be
          REJECTED, the other 98 ACCEPTED. Deriving the verdict from the path
          rather than from what spar currently does is the point: a sweep that
          recorded current behaviour would have called an unparseable file
          "expected: reject" and stayed green forever. It found one — a
          descriptor added in #215 whose stated purpose was to be a cross-check
          and which had never parsed, because no gate walked docs/ at all. No
          ratchet here: a first-party model we cannot parse is a defect, not a
          budget.

        * osate_agreement.rs is the 2-way matrix against OSATE 2.18.0.
          too-permissive ratchets down from 53 and is EXACT (a win below the
          floor also fails, so it is locked in rather than left as slack).
          too-strict is an INVARIANT at 0 — spar rejecting what the reference
          accepts has no acceptable non-zero value. A spar-stricter file is
          adjudicated against the standard, never assumed wrong.

        * three_way_conformance.rs adds Ocarina (OpenAADL, Ada — no shared
          code with OSATE's Xtext grammar), so a disagreement between the two
          implementations is CONTESTED and exempt from grading rather than
          silently resolved in whichever direction is convenient.

        All three baselines cover the SAME 120 paths, asserted, so neither
        the sweep nor either implementation's column can drift ahead of the
        others.

        1347 third-party models vendored (GaloisInc CASE-AADL-Tutorial,
        AADLib, FMW, VERDICT) and ratcheted as a SET OF PATHS, not a count —
        a passing file that starts failing cannot be paid for by a failing
        file that starts passing.

        Six parser fixes fall out, including the first genuine too-strict
        defect: the subcomponent-category table was MEASURED from OSATE
        (196/196 probes), not transcribed from AS5506B, because a slip in the
        forbidding direction makes spar reject valid AADL.

        OSATE IS A TEST, NOT THE AUTHORITY. If "agrees with OSATE" were the
        pass condition, every OSATE bug would become a bug spar is obliged to
        reproduce. The authority is SAE AS5506; OSATE is the oracle we can
        actually run.

  #417  An unresolvable --root must FAIL, not fabricate a model. `spar
        instantiate --root Nonexistent.impl` built an empty instance and
        reported success — the v0.36.0 defect class exactly, an operation
        whose "nothing happened" rendered identically to "it worked".

  #422  `spar --version` did not exist. The shipped binary could not state
        which spar it was. It now prints to stdout, equals CARGO_PKG_VERSION
        by test, and the release workflow RUNS the freshly built binary and
        asserts it reports the tag — on every target whose architecture the
        runner can execute, announcing every skip via ::notice rather than
        passing silently.

  #414  A verification artifact's evidence step must run from a clean
        checkout, and a threshold a gate enforces must live in ONE place.
        TEST-GUARD-GATE-EVIDENCE declared a step requiring mutants-out/, which
        exists only after a 3h CI job, so it scored permanently FAILED from
        any checkout; and it restated --max-missed 210 while ci.yml enforced
        292. `--assert-workflow-threshold` reads the committed workflow
        instead of carrying a copy.

FALSIFICATION. This release claims spar's output is accepted by two
independent AADL implementations to a measured, non-increasing degree. To
falsify it: hand OSATE 2.18.0 or Ocarina a first-party .aadl file that
osate-first-party.tsv records as ACCEPT and observe a rejection, or find a
file spar rejects that both implementations accept (the too-strict cell is
asserted at exactly 0). What is NOT claimed: that the 53 too-permissive files
are correct AADL — they are files OSATE rejects and spar does not, an
acknowledged debt with a ratchet on it (#420) — and the OSATE column came
from FULL VALIDATION while spar's comes from `parse`, so some of that 53 may
be caught by later spar stages at matched stage.

The text above is the message of the signed annotated tag v0.37.0.
Re-derive it, signature and all, with git tag -v v0.37.0.

Verified on this release's own workflow

The #422 guard ran the freshly built binary and asserted it reports the tag.
It executed on 3 of 5 targets and announced the other 2 rather than passing silently:

x86_64-pc-windows-msvc    binary says: spar 0.37.0  == tag implies: spar 0.37.0  + exit 2 contract
aarch64-apple-darwin      binary says: spar 0.37.0  == tag implies: spar 0.37.0  + exit 2 contract
x86_64-unknown-linux-gnu  binary says: spar 0.37.0  == tag implies: spar 0.37.0  + exit 2 contract
aarch64-unknown-linux-gnu ::notice SKIPPED - aarch64 target on x86_64 runner
x86_64-apple-darwin       ::notice SKIPPED - x86_64 target on aarch64 runner

The two skips are genuine arch mismatches, and both artifacts ship without a
version check — stated here because a guard that skips silently everywhere is
indistinguishable from one that passes.

---

What's Changed

• fix(hir,cli): an unresolvable --root must fail, not fabricate a model (#417) by @avrabe in #418
• test(interop): gate the AADL we write — first-party sweep + OSATE agreement ratchet by @avrabe in #419
• chore(release): v0.37.0 by @avrabe in #412
• feat(guard): an evidence step must run from a checkout; single-source the mutation threshold (#414) by @avrabe in #423

Full Changelog: v0.36.0...v0.37.0

spar v0.36.0

What's Changed

• ci(guard): enforce human-scoped artifacts mechanically (REQ-GUARD-HUMAN-SCOPED-001) by @avrabe in #359
• chore(artifacts): tag the three ordeal artifacts human-scoped by @avrabe in #367
• fix(artifacts): put release: on the plane rivet actually reads (#370) by @avrabe in #373
• ci: six reviewed guardrail PRs as one branch, plus two gate repairs (#381, #383) by @avrabe in #387
• ci(fixture-vm): make the nightly actually run — lock, qcow2 attribute, git-dep hash (#362, #365) by @avrabe in #364
• plan(v0.36.0): scope the gate-evidence release and close two open V's by @avrabe in #392
• feat(guard): fail a verification step whose test filter selects nothing (#388) by @avrabe in #393
• fix(trace-topology): taprio GCL readback honours sched-entry cmd (S/H/R) (#390) by @avrabe in #394
• feat(guard): clippy every workspace, and assert the fuzz target set (#383, #390) by @avrabe in #395
• feat(guard): a sorry cannot exempt itself by writing a comment (#385) by @avrabe in #396
• fix(guard): the changed-path classifier cannot fail open (#384) by @avrabe in #399
• feat(guard): a truncated cargo-mutants run cannot score (#389) by @avrabe in #401
• fix(release,guard): a short release cannot be signed; withdraw a false claim by @avrabe in #407
• fix(guard): close the two live holes in obligations (c) and (f) by @avrabe in #408
• feat(guard): audit the REQUIRED fuzz context's target list, not only the advisory one (#406) by @avrabe in #409
• chore(release): v0.36.0 by @avrabe in #410
• feat(guard): require a bounded timeout-minutes on every required-context job (#398) by @avrabe in #411
• feat(guard): an artifact claiming evidence must carry a runnable step (#403) by @avrabe in #413
• fix(ci): the tag-point gate must fetch the tag OBJECT, not judge the ref by @avrabe in #415

Full Changelog: v0.35.0...v0.36.0

spar v0.35.0

What's Changed

• plan(rivet): ordeal-integration release roadmap (v0.35–v0.42) by @avrabe in #352
• feat(codegen): certify AADL↔WIT byte-layout equivalence via ordeal (#327) by @avrabe in #354
• chore(release): bump to v0.35.0 by @avrabe in #355
• ci: skip heavy jobs on artifacts/docs-only diffs by @avrabe in #353
• fix(codegen): withdraw the layout certificate — it proved a tautology (#327) by @avrabe in #356
• fix(analysis): report unmeasurable bus demand instead of silence (REQ-NC-BUS-PAYLOAD-001) by @avrabe in #357

Full Changelog: v0.34.0...v0.35.0

spar v0.34.0

What's Changed

• ci: make rivet-validate deterministic to fix stale-binary false-red by @avrabe in #348
• feat(codegen): emit target constants module + linker memory map (#338) by @avrabe in #349
• chore(release): bump to v0.34.0 by @avrabe in #351

Full Changelog: v0.33.0...v0.34.0

spar v0.33.0

What's Changed

• feat(codegen): emit typed WIT list from Array data types (#345) by @avrabe in #346
• chore(release): bump to v0.33.0 by @avrabe in #347

Full Changelog: v0.32.0...v0.33.0

spar v0.32.0

What's Changed

• fix(parser): reject C-style radix literals (0x/0b/0o) instead of silently parsing to 0 (#337) by @avrabe in #343
• chore(release): bump to v0.32.0 by @avrabe in #344

Full Changelog: v0.31.0...v0.32.0

spar v0.31.0

What's Changed

• fix(parser): accept underscore digit-separators in based literals (#339) by @avrabe in #341
• chore(release): bump to v0.31.0 by @avrabe in #342

Full Changelog: v0.30.0...v0.31.0

spar v0.30.0

What's Changed

• feat(proofs): reflection generator for scheduling_verified.rs (closes #321) by @avrabe in #336
• chore(release): bump to v0.30.0 (#321 — reflection generator) by @avrabe in #340

Full Changelog: v0.29.0...v0.30.0

spar v0.29.0

What's Changed

• refactor(proofs): remove codegen fiction, name the scheduling-math source (#321 foundation) by @avrabe in #334
• chore(release): bump to v0.29.0 (#321 foundation) by @avrabe in #335

Full Changelog: v0.28.0...v0.29.0