spar v0.20.0

What's Changed

• feat(dbc): CAN message flows as AADL ports + bus-bound connections (REQ-INGEST-DBC-FLOWS-001) by @avrabe in #289
• feat(network): 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-BASE-001) by @avrabe in #290
• feat(network): standard CQF synthesis baseline (REQ-TSN-SYNTH-CQF-BASE-001) by @avrabe in #291
• feat(analysis): AADL→CQF synthesis bridge (REQ-TSN-SYNTH-CQF-BRIDGE-001) by @avrabe in #292
• feat(network): 802.1Qcw YANG/NETCONF export of synthesized GCL (REQ-TSN-EXPORT-YANG-001) by @avrabe in #293
• fix(network,analysis): guard YANG whole-ns precondition + correct cqf_synth Period doc by @avrabe in #295
• chore(release): bump to v0.20.0 by @avrabe in #296

Full Changelog: v0.19.0...v0.20.0

spar v0.19.0

What's Changed

• feat(network): PLP on converging sink-trees via topological relabel (REQ-NC-PLP-CONVERGE-001) by @avrabe in #285
• docs(readme): reframe as a compiler for system-architecture models by @avrabe in #286
• feat(network): TFA-strengthened PLP tightening to EXACT (REQ-NC-PLP-003) by @avrabe in #287
• chore(release): bump to v0.19.0 by @avrabe in #288

Full Changelog: v0.18.0...v0.19.0

spar v0.18.0

What's Changed

• feat(network): NC cross-validation against panco reference (REQ-NC-VALIDATION-001) by @avrabe in #279
• feat(network): PLP polynomial-LP network-calculus bounds (REQ-NC-PLP-001) by @avrabe in #280
• feat(network): AADL instance → network-wide TFA/PLP solver bridge (REQ-NC-BRIDGE-001) by @avrabe in #283
• chore(release): bump to v0.18.0 by @avrabe in #284

Full Changelog: v0.17.0...v0.18.0

spar v0.17.0

What's Changed

• docs(strategy): TSN-competitor roadmap + rivet scope (DEC-TSN-OSS-001) by @avrabe in #274
• feat(network): FP-TFA/TFA++ total-flow network-calculus bounds (REQ-NC-TFA-001) by @avrabe in #276
• feat(dbc): CAN .dbc ingest → AADL via spar-dbc (REQ-INGEST-DBC-001) by @avrabe in #277
• chore(release): bump to v0.17.0 by @avrabe in #278

Full Changelog: v0.16.0...v0.17.0

spar v0.16.0

What's Changed

• feat(parser): close four core AADL parser gaps (REQ-PLUGFEST-003) by @avrabe in #271
• chore(release): bump to v0.16.0 by @avrabe in #273
• chore(deps): bump rand to 0.9.3 to clear RUSTSEC-2026-0097 by @avrabe in #275

Full Changelog: v0.15.0...v0.16.0

spar v0.15.0

What's Changed

• chore(traceability): wire REQ-PROOF-SCHED-001 to the gating Lean job (v0.15.0) by @avrabe in #269
• chore(release): bump to v0.15.0 by @avrabe in #270

Full Changelog: v0.14.0...v0.15.0

Falsification criterion

v0.15.0 is wrong if:

• any proof in proofs/Proofs/Scheduling/ acquires a sorry (or an axiom standing in for a proof) and the Lean proof typecheck (lake build) check stays green — the fail-on-sorry gate must turn it red;
• a Lean/Mathlib toolchain bump breaks a scheduling proof and the check is NOT a required, merge-blocking status on main (verify via branch protection: it must appear in the required contexts);
• proofs/Proofs.lean stops importing any of Scheduling.{RTA, RMBound, EDF, RTAJittered, Latency, Arinc653Isolation}, removing it from the gated build without the requirement (REQ-PROOF-SCHED-001) being re-opened;
• cosign verify-blob … --bundle SHA256SUMS.txt.cosign.bundle SHA256SUMS.txt ≠ Verified OK, or gh attestation verify spar-v0.15.0-<triple>.tar.gz --repo pulseengine/spar fails.

Verified at publish: SHA256SUMS MATCH (binary + wasm bundle), cosign Verified OK, gh attestation verify exit 0.

spar v0.14.0

What's Changed

• fix(proofs): stratified period proofs + Kani 0.67 CI + build-time contract verification (#252) by @avrabe in #263
• [temper] Configuration update by @temper-pulseengine[bot] in #167
• chore(traceability): v0.14.0 link-and-promote — six codegen/MCP requirements to implemented by @avrabe in #266
• feat(codegen): WIT scalar type fidelity from Data_Size (REQ-CODEGEN-WIT-TYPES) by @avrabe in #267
• fix(hir-def): lower uppercase AADL keywords — case-insensitive item-tree extraction (#235) by @avrabe in #265
• chore(release): bump to v0.14.0 by @avrabe in #268

New Contributors

• @temper-pulseengine[bot] made their first contribution in #167

Full Changelog: v0.13.0...v0.14.0

Falsification criterion

v0.14.0 is wrong if any of the following is observed:

• the prove_thread_period_preserved_d1..d10 Kani harnesses do not collectively cover (0, 10^9] ns (a const assertion guards the tiling; a gap means the stratified proof is weaker than the original full-domain claim), or any band reports VERIFICATION:- FAILED for a non-resource reason (#252/#263);
• spar codegen --verify build does not emit a build.rs that fails compilation when a generated PERIOD_PS/DEADLINE_PS/WCET_PS constant diverges from aadl-contract.toml (REQ-CODEGEN-VERIFY-BUILD);
• spar codegen --format wit maps an AADL data type with Data_Size => 8 Bytes to anything other than u64 (1→u8, 2→u16, 4→u32, 8→u64; else list<u8>) (REQ-CODEGEN-WIT-TYPES);
• spar instance on an all-uppercase-keyword AADL model produces a different instance tree than its lowercase twin, or returns an empty/partial model where the lowercase form is complete (#235);
• a Lean/Mathlib bump breaks a proofs/Proofs/Scheduling/ proof and the Lean proof typecheck (lake build) check does not turn red and block merge (it is a required gating check as of this release);
• cosign verify-blob --certificate-identity-regexp 'https://github.com/pulseengine/spar/.github/workflows/release.yml@.*' --certificate-oidc-issuer 'https://token.actions.githubusercontent.com' --bundle SHA256SUMS.txt.cosign.bundle SHA256SUMS.txt does not return Verified OK, or gh attestation verify spar-v0.14.0-<triple>.tar.gz --repo pulseengine/spar fails.

Verified at publish: SHA256SUMS MATCH (binary + wasm bundle), cosign Verified OK, gh attestation verify exit 0. (The VS Code Marketplace publish step failed transiently — a token/external-store issue, outside the signed artifact chain; the GitHub release and all 19 assets are intact and verified.)

spar v0.13.0

What's Changed

• chore(traceability): promote 25 verified requirements to implemented by @avrabe in #250
• chore(traceability): promote REQ-NETWORK-007 to implemented by @avrabe in #253
• ci(release): emit artifacts.yaml for website data auto-generation by @avrabe in #251
• fix(vscode): highlight AADL keywords case-insensitively (#235) by @avrabe in #258
• feat(wasm): build spar-wasm for wasm32 + publish browser bundle (#259) by @avrabe in #260
• chore(planning): release plan v0.13.0–v0.22.0 in rivet by @avrabe in #262
• fix(codegen): emit valid, bindable WIT — kebab idents + defined types (#254) by @avrabe in #255
• fix(hir-def): don't panic instantiating cross-file extends chains (#236) by @avrabe in #256
• fix(hir-def): preserve properties applied to connections and features (#237) by @avrabe in #257
• chore(release): bump to v0.13.0 by @avrabe in #264

Full Changelog: v0.12.0...v0.13.0

Falsification criterion

v0.13.0 is wrong if any of the following is observed in the field:

• spar codegen --format wit emits WIT that wasm-tools component wit rejects (invalid identifier or unresolved type) for any process whose AADL identifiers are well-formed — or the generated interface omits a type definition for a data type a port references (#254);
• spar instance panics on a well-formed model whose implementation extends a parent declared in another file (#236), or the instantiated model drops a property attached via applies to <connection> / applies to <feature> or collapses two ports' properties into one (#237);
• the VS Code grammar fails to highlight an AS5506-legal keyword solely because of its case (#235);
• spar-wasm-browser-v0.13.0.tar.gz fails to instantiate in a browser via its spar_wasm.js loader, or the bundle was built with the HiGHS MILP solver present (it must be feature-gated out) (#259);
• cosign verify-blob --certificate-identity-regexp 'https://github.com/pulseengine/spar/.github/workflows/release.yml@.*' --certificate-oidc-issuer 'https://token.actions.githubusercontent.com' --bundle SHA256SUMS.txt.cosign.bundle SHA256SUMS.txt does not return Verified OK, or gh attestation verify spar-v0.13.0-<triple>.tar.gz --repo pulseengine/spar fails.

Verified at publish: SHA256SUMS MATCH (binary + wasm bundle), cosign Verified OK, gh attestation verify exit 0, bundle carries spar_wasm.js + core*.wasm.

spar v0.12.0

What's Changed

• fix(analysis): resolve multi-level dotted binding reference paths by @avrabe in #248
• feat(interop): AADL plug-fest Tier-A — OSATE corpus parse ratchet (#246) by @avrabe in #247
• chore(release): bump to v0.12.0 by @avrabe in #249

Full Changelog: v0.11.0...v0.12.0

Falsification criterion

v0.12.0 is wrong if any of the following is observed in the field:

• spar analyze reports a binding-target error (e.g. unresolved or wrong-category) for an Actual_Processor_Binding/Actual_Memory_Binding whose multi-level dotted reference path (a.b.c) resolves to a real component of the correct category in the instance model — or stays silent when such a binding names a non-existent path or a target of the wrong category (#248);
• the parser rejects a well-formed AADL property set whose declared property applies to (...) names a feature/port/flow/mode/access/parameter/connections owner category accepted by AS5506 §11.3 — or accepts an owner category outside that grammar (#247);
• spar regresses on any OSATE examples corpus file it parsed at this tag without that file being recorded in a regression baseline (test-data/interop/baseline/), i.e. the Tier-A ratchet silently loosens (#246/#247);
• cosign verify-blob --certificate-identity-regexp 'https://github.com/pulseengine/spar/.github/workflows/release.yml@.*' --certificate-oidc-issuer 'https://token.actions.githubusercontent.com' --bundle SHA256SUMS.txt.cosign.bundle SHA256SUMS.txt does not return Verified OK, or gh attestation verify spar-v0.12.0-<triple>.tar.gz --repo pulseengine/spar fails, for the published assets.

Verified at publish: SHA256SUMS integrity MATCH, cosign verify-blob → Verified OK, gh attestation verify → exit 0.

spar v0.11.0

What's Changed

• fix(codegen): --format wit emits only WIT, not the Rust workspace by @avrabe in #232
• feat(trace-topology): Rust trace-fixture generator (netns + TSN, v0.11.0) by @avrabe in #233
• feat(trace-topology): NixOS guest + QEMU harness for fixture generation (v0.11.0 PR 2) by @avrabe in #234
• fix(trace-fixtures): correct bogus nixos/nix container digest by @avrabe in #238
• fix(trace-fixtures): require podman label on fixture-vm workflows by @avrabe in #240
• feat(trace-topology): IdentityUnknown reconciliation check (v0.11.0) by @avrabe in #239
• feat(trace-topology): GptpOutOfBudget reconciliation check (v0.11.0) by @avrabe in #241
• fix(release): standardize on pulseengine cosign + SLSA flow (synth ref) by @avrabe in #244
• chore(release): bump to v0.11.0 by @avrabe in #245
• fix(codegen): per-category summary + hint when WIT requested but none emitted by @avrabe in #242

Full Changelog: v0.10.0...v0.11.0

---

Falsification criterion

v0.11.0 is wrong if any of the following is observed in the field:

• the trace-topology reconciler emits an IdentityUnknown or GptpOutOfBudget finding for a deployment whose AADL model fully and correctly declares the observed identities / sync budget (false positive), or stays silent when an observed identity / worst-case sync error has no corresponding declaration (false negative);
• cosign verify-blob --certificate-identity-regexp 'https://github.com/pulseengine/spar/.github/workflows/release.yml@.*' --certificate-oidc-issuer 'https://token.actions.githubusercontent.com' --bundle SHA256SUMS.txt.cosign.bundle SHA256SUMS.txt does not return Verified OK, or gh attestation verify spar-v0.11.0-<triple>.tar.gz --repo pulseengine/spar fails, for the published assets.