docs+test: Track A close-out (commit 4/4) — COMPLIANCE narrative + CLI integration

COMPLIANCE.md

@@ -1,8 +1,8 @@
 # AS5506 AADL v2.2 Compliance Gap Analysis
 
-**Updated**: 2026-04-05 (v0.6.0)
+**Updated**: 2026-04-25 (v0.7.0 in progress)
 **Source**: 102 HTML files from OSATE2 (`org.osate.help/html/std/`)
-**Toolchain**: spar (1200+ tests passing across 16 crates)
+**Toolchain**: spar (1900+ tests passing across 17 crates)
 
 ---
 
@@ -216,7 +216,36 @@
 
 ## In progress / v0.7.0
 
-- IRQ-aware RTA: hierarchical two-tier analysis with `Dispatch_Jitter` and BCET/WCET split landed (Track A commit 2); PIP/PCP blocking deferred to v0.7.1.
+**Track A — IRQ-aware RTA (4/4 commits delivered)**
+
+- Foundation (#145): `Spar_Timing::{ISR_Priority, ISR_Execution_Time, Interrupt_Latency_Bound, Bottom_Half_Server}` and `Spar_Trace::{Probe_Point, Expected_BCET, Expected_WCET, Expected_Mean}` property sets land as non-standard predefined sets, resolvable via the same idiom as AS5506 standard sets.
+- Hierarchical RTA (#147): two-tier analysis — 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)`. Five new diagnostic kinds: `IrqResponseBudget`, `IrqBudgetViolated`, `IsrOverloadedCpu`, `MissingBottomHalfServer`, `ResponseBand`. Non-regression gate (`no_isrs_matches_classical_rta`) verifies models without `Spar_Timing::*` produce byte-identical RTA output.
+- Lean convergence (#148): `proofs/Proofs/Scheduling/RTAJittered.lean` proves monotonicity, zero-jitter degeneration to classical `rtaStep`, and least-fixed-point convergence in `deadline + 1` iterations. Three core theorems plus two helper lemmas, no `sorry`.
+- Close-out (this commit): COMPLIANCE wording, COMPLIANCE-side acknowledgement of out-of-scope items.
+
+**Out of scope for v0.7.0, deferred to v0.7.1+**: priority inheritance (PIP) / priority ceiling (PCP) blocking; multi-processor ISR migration; cache-aware interference inflation (research-grade, v1.0+).
+
+**Track B — Variants (foundation only)**
+
+- Variant binding contract v1 (#144): `docs/contracts/rivet-spar-variant-v1.md` — rivet owns the PLE truth (feature model, variant configs, bindings, SAT), spar consumes a JSON context blob and filters HIR. Implementation of the consumer crate (`spar-variants`) waits for rivet to emit its first context blob; tracked separately.
+
+**v0.7.x infrastructure landed alongside Track A**
+
+- Kani harnesses for spar-solver and spar-codegen invariants (#141, closes #136).
+- cargo-fuzz scaffolding for parser, solver, codegen-roundtrip targets (#142, closes #138).
+- Criterion benchmarks for scheduling solver and codegen (#143, closes #137).
+- Lean / Bazel / proptest CI gates (#151, closes #135) — Lean proofs now machine-checked in CI for the first time.
+- Track D and Track E research design docs landed (#152, #153) anchoring v0.8.0+ scope.
+
+---
+
+## v0.8.0 planning
+
+Two parallel tracks scoped from the v0.7.0 research:
+
+**Track D — TSN/Ethernet WCTT analysis (#149)**: WCTT is a foundational primitive for honest end-to-end timing, not a TSN-specific feature. Phase 1 (v0.8.0) ships a Network Calculus engine for FIFO+priority networks (classical Ethernet, CAN, FlexRay) and replaces `latency.rs`'s scalar bus-latency lookup with per-stream NC-derived bounds. Phase 2 (v0.8.x) adds TSN-specific service curves (TAS, CBS, frame preemption). Roadmap: 7 weeks across 6 commits.
+
+**Track E — Frozen-platform / mobile-application split + hypothetical-rebinding oracle (#150)**: Adds `Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason}` plus a verification mode (`spar moves verify`) and an enumeration mode (`spar moves enumerate`). The MCP tool surface (`spar.verify_move`, `spar.enumerate_moves`) ships in v0.9.0 — read-only / idempotent only, deterministic apply via CLI. LLM agents propose moves; spar deterministically verifies; certification chain stays in spar. Roadmap: 8 weeks across 8 commits for v0.8.0; another 8.5 weeks across the v0.9.0 MCP surface.
 
 ---
 

crates/spar-cli/tests/track_a_close_out.rs

@@ -0,0 +1,111 @@
+//! Track A close-out: end-to-end CLI integration test for IRQ-aware RTA.
+//!
+//! Exercises the full pipeline (parse → instance → analyze) on a model
+//! using the v0.7.0 `Spar_Timing::*` property surface. The unit/fixture
+//! tests in `spar-analysis/tests/fixtures/rta/` cover the algorithm at
+//! the analysis-crate level; this test is the CLI-level guard that the
+//! property surface flows through `spar analyze` end-to-end.
+
+use std::env;
+use std::fs;
+use std::process::Command;
+
+fn spar() -> Command {
+    Command::new(env!("CARGO_BIN_EXE_spar"))
+}
+
+const MODEL: &str = "\
+package Test_Track_A_IRQ
+public
+  with Timing_Properties;
+  with Deployment_Properties;
+  with Spar_Timing;
+
+  processor M4
+  end M4;
+
+  device Sensor_IRQ
+  end Sensor_IRQ;
+
+  device implementation Sensor_IRQ.Impl
+    properties
+      Spar_Timing::ISR_Priority         => 100;
+      Spar_Timing::ISR_Execution_Time   => 20 us .. 30 us;
+      Spar_Timing::Interrupt_Latency_Bound => 10 us;
+  end Sensor_IRQ.Impl;
+
+  thread Brake_Handler
+  end Brake_Handler;
+
+  thread implementation Brake_Handler.Impl
+    properties
+      Dispatch_Protocol => Sporadic;
+      Period            => 1 ms;
+      Compute_Execution_Time => 50 us .. 200 us;
+      Deadline          => 1 ms;
+  end Brake_Handler.Impl;
+
+  process P
+  end P;
+
+  process implementation P.Impl
+    subcomponents
+      bh: thread Brake_Handler.Impl;
+  end P.Impl;
+
+  system Top
+  end Top;
+
+  system implementation Top.Impl
+    subcomponents
+      cpu: processor M4;
+      irq: device Sensor_IRQ.Impl;
+      app: process P.Impl;
+    properties
+      Actual_Processor_Binding => (reference (cpu)) applies to app.bh;
+  end Top.Impl;
+end Test_Track_A_IRQ;
+";
+
+#[test]
+fn track_a_irq_aware_rta_runs_through_cli() {
+    let path = env::temp_dir().join(format!("spar_track_a_irq_{}.aadl", std::process::id()));
+    fs::write(&path, MODEL).expect("write temp AADL");
+
+    let output = spar()
+        .arg("analyze")
+        .arg("--root")
+        .arg("Test_Track_A_IRQ::Top.Impl")
+        .arg(&path)
+        .output()
+        .expect("failed to run spar");
+
+    let combined = format!(
+        "{}\n{}",
+        String::from_utf8_lossy(&output.stdout),
+        String::from_utf8_lossy(&output.stderr),
+    );
+
+    // The pipeline must complete (non-zero exit only on hard parse errors,
+    // which this model doesn't have). Diagnostic content can vary as the
+    // analysis matures; we only guard the must-not-crash invariant + the
+    // presence of *some* RTA output, since the model is RTA-relevant.
+    assert!(
+        !combined.contains("panicked"),
+        "spar analyze panicked on Spar_Timing::* model:\n{combined}",
+    );
+    assert!(
+        !combined.contains("internal compiler error"),
+        "spar analyze internal error:\n{combined}",
+    );
+
+    // Loose check: RTA must say *something* about the handler thread
+    // since it is bound to a CPU and has a deadline.
+    let mentions_handler = combined.contains("Brake_Handler") || combined.contains("bh");
+    assert!(
+        mentions_handler,
+        "spar analyze did not surface any output mentioning the handler thread:\n{combined}",
+    );
+
+    let _ = fs::remove_file(&path);
+}