spar v0.22.0

What's Changed

• chore(planning): record TAS-composition soundness NO-GO + simulator-floor gate (#141) by @avrabe in #304
• chore: gitignore cargo-mutants output dirs by @avrabe in #305
• chore(planning): scope v0.22.0 to Deployable TSN synthesis (4 items) by @avrabe in #306
• feat(analysis): authoritative network-wide NC bound = min(PLP,TFA) (REQ-NC-PLP-MIN-001) by @avrabe in #307
• feat(analysis): verify wrpc-binding resolves to a bus (REQ-WRPC-BINDING-003) by @avrabe in #308
• feat(network): guard-band-aware 802.1Qbv GCL splitting (REQ-TSN-SYNTH-QBV-GUARDBAND-001) by @avrabe in #309
• chore(release): bump to v0.22.0 by @avrabe in #310

Full Changelog: v0.21.0...v0.22.0

spar v0.21.0

What's Changed

• chore(planning): map open GitHub issues into the rivet release roadmap by @avrabe in #298
• feat(network): sound exact TAS service-curve latency for multi-window GCLs (REQ-TSN-SVC-MULTIWIN-001) by @avrabe in #299
• fix(analysis): honor per-connection Actual_Connection_Binding in wrpc-binding (REQ-WRPC-BINDING-002) by @avrabe in #300
• chore(planning): re-scope REQ-EMV2-PROPAGATION-002 after investigation (#294) by @avrabe in #301
• feat(network): window-splitting 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001) by @avrabe in #302
• chore(release): bump to v0.21.0 by @avrabe in #303

Full Changelog: v0.20.0...v0.21.0

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.