diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..07fa507 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,108 @@ +# Changelog + +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.7.1] — 2026-04-27 + +This release closes the v0.7.x line. Headline: full IRQ-aware response-time +analysis with priority-inheritance / priority-ceiling blocking, machine-checked +in Lean. Plus the entire v0.7.x verification-infrastructure ratchet. + +Track D Phase 1 (TSN/Ethernet WCTT) and Track E (migration oracle, commits 1-4) +are also on `main` at the time of this tag — they will be promoted in the next +release (v0.8.0). They are functional and tested but the Track E surface is +not yet at its commit-8 close-out. + +### Added — Track A v0.7.0 (IRQ-aware RTA) + +- `Spar_Timing::*` and `Spar_Trace::*` non-standard property sets + (`ISR_Priority`, `ISR_Execution_Time`, `Interrupt_Latency_Bound`, + `Bottom_Half_Server`; `Probe_Point`, `Expected_BCET`, `Expected_WCET`, + `Expected_Mean`). +- Hierarchical two-tier RTA: ISR layer steals CPU capacity first, residual + feeds task RTA. `Dispatch_Jitter` woven into the Tindell-Clark recurrence. + `Compute_Execution_Time`'s Time_Range consumed as `(BCET, WCET)`. +- New diagnostics: `IrqResponseBudget`, `IrqBudgetViolated`, + `IsrOverloadedCpu`, `MissingBottomHalfServer`, `ResponseBand`. +- Lean theorems for jittered RTA convergence (`proofs/Proofs/Scheduling/RTAJittered.lean`). +- Non-regression: models without `Spar_Timing::*` produce byte-identical + RTA output to v0.6.0. + +### Added — Track A v0.7.1 (PIP/PCP blocking) + +- `Thread_Properties::Locking_Protocol` (`Priority_Inheritance_Protocol`, + `Priority_Ceiling_Protocol`, `Stop_For_Lock`, `None`) + + `Spar_Timing::Critical_Section_Blocking` property recognition. +- Blocking term `B_i` folded into the hierarchical-RTA recurrence per + Joseph & Pandya 1986 / Buttazzo. New `BlockingInflated` Info diagnostic. +- Non-regression: models without `Locking_Protocol` produce byte-identical + output to v0.7.0. + +### Added — Track B v0.7.x foundation (variants) + +- `docs/contracts/rivet-spar-variant-v1.md` — interchange contract between + rivet (PLE truth) and spar (HIR consumer). Shape 1: rivet emits a JSON + context blob; spar consumes and filters HIR. +- New crate `spar-variants`: reads the v1 context blob, applies + intersection-semantics binding rules, exposes `keep_in_variant` predicate. + CLI integration arrives once rivet's emitter side ships. + +### Added — v0.7.x verification infrastructure + +- **Lean + Bazel + proptest CI gates** (`.github/workflows/proofs.yml` + + `bazel-test` + `Rivet validate (artifacts)` jobs in `ci.yml`). + Lean proofs now machine-checked on every PR via Mathlib precompiled cache. + Closes #135. +- **Kani harnesses** (`crates/spar-{solver,codegen}/tests/kani_*.rs`) bounded- + model-check ARINC653 solver invariants (closes #136). +- **cargo-fuzz scaffolding** (`fuzz/`, three targets: parser, solver, + codegen-roundtrip, with PR smoke + nightly soak workflows) (closes #138). +- **Criterion benchmarks** (`crates/spar-{solver,codegen}/benches/`, + PR compile-gate + nightly baseline) (closes #137). +- Status badges + AGENTS.md regeneration via `rivet init --agents`. + +### Added — v0.8.0 in flight (on main, not feature-promoted in this release) + +- **Track D Phase 1 — TSN/Ethernet WCTT analysis (6/6 commits)**: new + `spar-network` crate with NetworkGraph extraction + Network Calculus + primitives + Lean theorems. New `WcttAnalysis` pass produces per-stream + end-to-end traversal-time bounds. `latency.rs` integration alternates + RTA-derived WCET on compute hops with WCTT on network hops, replacing the + scalar `Bus_Properties::Latency` placeholder when `Spar_Network::*` is + annotated. +- **Track E commits 1-4 (4/8)**: `Spar_Migration::*` property set, + `BindingOverlay` for hypothetical-binding queries, `spar moves verify` + CLI returning JSON pass/fail, `spar moves enumerate` listing valid + rebinding candidates ranked by slack. + +### Changed + +- COMPLIANCE.md narrative updated for v0.7.0 / v0.7.1 / partial v0.8.0. +- Test count: ~1900+ across 17 crates (previously ~1200 across 16). +- `rivet validate` pin in CI bumped from v0.1.0 to v0.4.3 to match the schema- + tolerance behaviour of current artifacts. +- Migration: `cargo-fuzz` job now pinned to `x86_64-unknown-linux-gnu` + (avoids ASan / static-libc conflict). + +### Fixed + +- Two Lean import-order / comment-style issues in `RTAJittered.lean` and + `Network/MinPlus.lean` surfaced (and resolved) by the new Lean CI gate. +- Cargo-vet exemption ordering bug after appending criterion + pretty_assertions + dev-deps; sorter Python script now keeps the store-format check happy. + +### Documentation + +- `docs/designs/v0.7.0-hierarchical-rta.md` — design doc for Track A commit 2. +- `docs/designs/track-d-tsn-wctt-research.md` — TSN/WCTT design space + commercial-tool comparison (RTaW-Pegase et al.). +- `docs/designs/track-e-migration-research.md` — migration / design-space oracle research, MCP boundary design. +- `docs/designs/track-f-sysml-kerml-engagement.md` — SysML v2 / KerML community engagement strategy. +- `docs/contracts/rivet-spar-variant-v1.md` — variant-context interchange contract. + +--- + +## [0.6.0] — 2026-04-05 + +Earlier releases — see git history (no formal changelog kept before v0.7.1). diff --git a/Cargo.lock b/Cargo.lock index a495300..94d25e6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1215,7 +1215,7 @@ dependencies = [ [[package]] name = "spar" -version = "0.6.0" +version = "0.7.1" dependencies = [ "etch", "la-arena", @@ -1243,7 +1243,7 @@ dependencies = [ [[package]] name = "spar-analysis" -version = "0.6.0" +version = "0.7.1" dependencies = [ "la-arena", "rustc-hash 2.1.2", @@ -1256,7 +1256,7 @@ dependencies = [ [[package]] name = "spar-annex" -version = "0.6.0" +version = "0.7.1" dependencies = [ "rowan", "spar-syntax", @@ -1264,7 +1264,7 @@ dependencies = [ [[package]] name = "spar-base-db" -version = "0.6.0" +version = "0.7.1" dependencies = [ "rowan", "salsa", @@ -1274,7 +1274,7 @@ dependencies = [ [[package]] name = "spar-codegen" -version = "0.6.0" +version = "0.7.1" dependencies = [ "criterion", "la-arena", @@ -1288,7 +1288,7 @@ dependencies = [ [[package]] name = "spar-hir" -version = "0.6.0" +version = "0.7.1" dependencies = [ "salsa", "serde", @@ -1301,7 +1301,7 @@ dependencies = [ [[package]] name = "spar-hir-def" -version = "0.6.0" +version = "0.7.1" dependencies = [ "la-arena", "rowan", @@ -1315,7 +1315,7 @@ dependencies = [ [[package]] name = "spar-network" -version = "0.6.0" +version = "0.7.1" dependencies = [ "spar-base-db", "spar-hir-def", @@ -1323,7 +1323,7 @@ dependencies = [ [[package]] name = "spar-parser" -version = "0.6.0" +version = "0.7.1" dependencies = [ "expect-test", "proptest", @@ -1333,7 +1333,7 @@ dependencies = [ [[package]] name = "spar-render" -version = "0.6.0" +version = "0.7.1" dependencies = [ "etch", "la-arena", @@ -1344,7 +1344,7 @@ dependencies = [ [[package]] name = "spar-solver" -version = "0.6.0" +version = "0.7.1" dependencies = [ "criterion", "good_lp", @@ -1358,7 +1358,7 @@ dependencies = [ [[package]] name = "spar-syntax" -version = "0.6.0" +version = "0.7.1" dependencies = [ "expect-test", "rowan", @@ -1367,7 +1367,7 @@ dependencies = [ [[package]] name = "spar-sysml2" -version = "0.6.0" +version = "0.7.1" dependencies = [ "expect-test", "la-arena", @@ -1378,7 +1378,7 @@ dependencies = [ [[package]] name = "spar-transform" -version = "0.6.0" +version = "0.7.1" dependencies = [ "la-arena", "serde", @@ -1389,7 +1389,7 @@ dependencies = [ [[package]] name = "spar-variants" -version = "0.6.0" +version = "0.7.1" dependencies = [ "pretty_assertions", "serde", @@ -1399,14 +1399,14 @@ dependencies = [ [[package]] name = "spar-verify" -version = "0.6.0" +version = "0.7.1" dependencies = [ "spar-verify-macros", ] [[package]] name = "spar-verify-macros" -version = "0.6.0" +version = "0.7.1" dependencies = [ "proc-macro2", "quote", @@ -1415,7 +1415,7 @@ dependencies = [ [[package]] name = "spar-wasm" -version = "0.6.0" +version = "0.7.1" dependencies = [ "etch", "la-arena", diff --git a/Cargo.toml b/Cargo.toml index ef5ce53..9e91ee0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -22,7 +22,7 @@ members = [ ] [workspace.package] -version = "0.6.0" +version = "0.7.1" edition = "2024" license = "MIT" repository = "https://github.com/pulseengine/spar" diff --git a/vscode-spar/package.json b/vscode-spar/package.json index 6aecc06..4b52cbb 100644 --- a/vscode-spar/package.json +++ b/vscode-spar/package.json @@ -3,7 +3,7 @@ "displayName": "AADL (spar)", "description": "AADL v2.2 language support with live architecture visualization", "publisher": "pulseengine", - "version": "0.6.0", + "version": "0.7.1", "license": "MIT", "repository": { "type": "git",