diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c50f14..dbceee6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,93 @@ All notable changes to spar are documented here. Format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and the project follows [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.9.2] — 2026-05-03 + +Honesty + tightness pass. Closes the post-v0.9.0 reviewer's NC top-5 +items #4 and #13, three Tier-A soundness items (#5/#6/#9), the CBS +hi/loCredit user-tunability gap (#8), and the Lean/Rust α(0) +spec-impl mismatch (#2). Plus org-wide CI concurrency control and the +v0.8.x nightly-CI workflow fix. + +### Added — NC kernel honesty (4 PRs) + +- **α(0) = 0 causality fix (#193)** — Rust `ArrivalCurve::at` short- + circuited to return `σ` at t=0; Lean spec said `min(σ,0) = 0`. + Aligned to the causal answer (no traffic before t=0). Discharged + the 5th `MinPlus.lean` sorry; sorry count 5 → 4. +- **`Spar_TSN::Hi_Credit` + `Lo_Credit` user-tunable CBS (#195)** — + v0.8.1 hardcoded both credits to `Max_Frame_Size` regardless of + what the model declared. Real Qcc/YANG configs carry these per + traffic class. Property count 129 → 131. Default unset → + byte-identical to v0.8.1/v0.9.1. New `WcttCbsCredit` Info + diagnostic when at least one credit is explicit. Reviewer + Tier A #8. +- **WCTT per-stream sensitivity output (#196)** — every `WcttBound` + Info now followed by a `WcttSensitivity` Info carrying worst-hop + partial derivatives ∂σ_self / ∂ρ_competing / ∂T_link. Pure + post-processing on closed-form derivatives. Reviewer NC top-5 + #13: cheapest workflow win, turns spar from judge into design + partner. +- **RTA→WCTT release-jitter coupling (#199)** — when a stream's + source declares `Timing_Properties::Dispatch_Jitter`, that value + J is treated as ingress release-jitter and inflates the arrival + burst σ by `ρ·J` bytes. New `WcttRtaCoupled` Info diagnostic. + Reviewer NC top-5 #4: single biggest credibility lift. + +### Added — RTA / safety soundness (2 PRs) + +- **Stop_For_Lock + ARINC severity (#197)** — (a) RTA emits a + Warning when a thread declares `Locking_Protocol => Stop_For_Lock` + but no `Critical_Section_Blocking` (was silently using B=0, + unsound under priority inversion); (b) `ARINC-PARTITION-ISOLATION` + promoted from Warning to Error per DO-297 spatial-isolation + invariant; new `spar analyze --allow arinc-partition-isolation` + CLI flag for legitimate IMA bypasses. Reviewer Tier A #6 + #9. +- **Context_Switch_Time in RTA recurrence (#198)** — v0.8.x emitted + a STPA-REQ-022 advisory if `Context_Switch_Time` was unset but + never folded the value into the recurrence when set. Now inflates + each thread's WCET by `2 × Context_Switch_Time` per Buttazzo §7 + (one preemption-in + one preemption-out). New `OverheadInflation` + Info diagnostic. Lean recurrence theorem unchanged (caller-side + inflation). Reviewer Tier A #5 (partial — `Interrupt_Overhead` + per ISR firing still deferred). + +### Added — CI infrastructure (2 PRs) + +- **CI concurrency control (#200)** — top-level `concurrency:` block + on every workflow. Cancel superseded PR runs aggressively; never + cancel main / tags / scheduled events. Variant per workflow: + default for `ci.yml` + `proofs.yml`, scheduled (per-run group) + for `bench-nightly.yml` + `fuzz-nightly.yml`, release (group by + tag, never cancel) for `release.yml`. Per the org-wide CI + hardening brief. +- **Nightly fuzz + bench fixes (#194)** — both nightly workflows + had failed since 2026-04-24 introduction. Fuzz: add + `--target x86_64-unknown-linux-gnu` to avoid the cargo-fuzz musl + / ASan conflict. Bench: gate `solver_worst_case/milp/worst_64` + behind `SPAR_BENCH_SLOW_MILP=1` env var; add `timeout-minutes: 60` + ceiling. + +### Changed + +- COMPLIANCE.md narrative for v0.9.2. +- Test count: 2790+ across 19 crates (was 2772 at v0.9.1). +- Property count: 129 → 131 (Spar_TSN::Hi_Credit + Lo_Credit). + +### Deferred + +- `Interrupt_Overhead` per ISR firing in RTA recurrence — Tier A + #5 partial close-out; companion to v0.9.2 `Context_Switch_Time`. +- Full RTA→WCTT automatic propagation (consume RTA's *computed* + `response_time` directly without requiring user-declared + `Dispatch_Jitter`). +- `MinPlus.lean` 4 remaining sorrys (`backlog_bound_classical`, + `delay_bound_classical`, `output_dominates_input`, + `compose_delays_dominates`) — tracked as TODO(v1.0.0). +- Kani harness production-code wiring (Tier A #3). + +--- + ## [0.9.1] — 2026-04-29 NC kernel soundness pass. Fixes two pure-soundness gaps flagged by an diff --git a/Cargo.lock b/Cargo.lock index d0ca6ac..76fbb01 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1215,7 +1215,7 @@ dependencies = [ [[package]] name = "spar" -version = "0.9.1" +version = "0.9.2" dependencies = [ "etch", "la-arena", @@ -1245,7 +1245,7 @@ dependencies = [ [[package]] name = "spar-analysis" -version = "0.9.1" +version = "0.9.2" dependencies = [ "la-arena", "rustc-hash 2.1.2", @@ -1258,7 +1258,7 @@ dependencies = [ [[package]] name = "spar-annex" -version = "0.9.1" +version = "0.9.2" dependencies = [ "rowan", "spar-syntax", @@ -1266,7 +1266,7 @@ dependencies = [ [[package]] name = "spar-base-db" -version = "0.9.1" +version = "0.9.2" dependencies = [ "rowan", "salsa", @@ -1276,7 +1276,7 @@ dependencies = [ [[package]] name = "spar-codegen" -version = "0.9.1" +version = "0.9.2" dependencies = [ "criterion", "la-arena", @@ -1290,7 +1290,7 @@ dependencies = [ [[package]] name = "spar-hir" -version = "0.9.1" +version = "0.9.2" dependencies = [ "salsa", "serde", @@ -1303,7 +1303,7 @@ dependencies = [ [[package]] name = "spar-hir-def" -version = "0.9.1" +version = "0.9.2" dependencies = [ "la-arena", "rowan", @@ -1317,7 +1317,7 @@ dependencies = [ [[package]] name = "spar-insight" -version = "0.9.1" +version = "0.9.2" dependencies = [ "pretty_assertions", "serde", @@ -1329,7 +1329,7 @@ dependencies = [ [[package]] name = "spar-mcp" -version = "0.9.1" +version = "0.9.2" dependencies = [ "serde", "serde_json", @@ -1344,7 +1344,7 @@ dependencies = [ [[package]] name = "spar-network" -version = "0.9.1" +version = "0.9.2" dependencies = [ "spar-base-db", "spar-hir-def", @@ -1352,7 +1352,7 @@ dependencies = [ [[package]] name = "spar-parser" -version = "0.9.1" +version = "0.9.2" dependencies = [ "expect-test", "proptest", @@ -1362,7 +1362,7 @@ dependencies = [ [[package]] name = "spar-render" -version = "0.9.1" +version = "0.9.2" dependencies = [ "etch", "la-arena", @@ -1373,7 +1373,7 @@ dependencies = [ [[package]] name = "spar-solver" -version = "0.9.1" +version = "0.9.2" dependencies = [ "criterion", "good_lp", @@ -1387,7 +1387,7 @@ dependencies = [ [[package]] name = "spar-syntax" -version = "0.9.1" +version = "0.9.2" dependencies = [ "expect-test", "rowan", @@ -1396,7 +1396,7 @@ dependencies = [ [[package]] name = "spar-sysml2" -version = "0.9.1" +version = "0.9.2" dependencies = [ "expect-test", "la-arena", @@ -1407,7 +1407,7 @@ dependencies = [ [[package]] name = "spar-transform" -version = "0.9.1" +version = "0.9.2" dependencies = [ "la-arena", "serde", @@ -1418,7 +1418,7 @@ dependencies = [ [[package]] name = "spar-variants" -version = "0.9.1" +version = "0.9.2" dependencies = [ "pretty_assertions", "serde", @@ -1428,14 +1428,14 @@ dependencies = [ [[package]] name = "spar-verify" -version = "0.9.1" +version = "0.9.2" dependencies = [ "spar-verify-macros", ] [[package]] name = "spar-verify-macros" -version = "0.9.1" +version = "0.9.2" dependencies = [ "proc-macro2", "quote", @@ -1444,7 +1444,7 @@ dependencies = [ [[package]] name = "spar-wasm" -version = "0.9.1" +version = "0.9.2" dependencies = [ "etch", "la-arena", diff --git a/Cargo.toml b/Cargo.toml index 448a0e5..c6dfce7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -24,7 +24,7 @@ members = [ ] [workspace.package] -version = "0.9.1" +version = "0.9.2" edition = "2024" license = "MIT" repository = "https://github.com/pulseengine/spar" diff --git a/vscode-spar/package.json b/vscode-spar/package.json index d127a4c..6dcdda6 100644 --- a/vscode-spar/package.json +++ b/vscode-spar/package.json @@ -3,7 +3,7 @@ "displayName": "AADL (spar)", "description": "AADL v2.2/v2.3 language support with live architecture visualization", "publisher": "pulseengine", - "version": "0.9.1", + "version": "0.9.2", "license": "MIT", "repository": { "type": "git",