feat(moves): rivet variant integration in verify/enumerate (Track E commit 6/8)

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).

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"

artifacts/requirements.yaml

@@ -1263,6 +1263,36 @@ artifacts:
     status: planned
     tags: [migration, track-e, v080, cli, solver]
 
+  - id: REQ-MIGRATION-008
+    type: requirement
+    title: spar moves verify/enumerate variant scoping (rivet v1 contract)
+    description: >
+      System shall accept `--variant NAME` (implicit form; spar shells
+      out to `rivet resolve --variant <name> --format spar-context-json`
+      per docs/contracts/rivet-spar-variant-v1.md) and
+      `--variant-context PATH` (explicit form; PATH is `-` for stdin or
+      a filesystem path) on both `spar moves verify` and
+      `spar moves enumerate`. The two flags are mutually exclusive. When
+      a variant is in play the move-oracle scopes its analysis to the
+      resolved-variant subset of HIR: components dropped by
+      keep_in_variant are unreachable as `--component` / `--to` targets
+      and are excluded from the candidate-target set in enumerate.
+      Resolution failures map to typed CLI errors — RivetNotFound
+      points at the explicit form, ComponentNotInVariant /
+      TargetNotInVariant identify dropped-by-variant inputs, and
+      VariantContextSchema surfaces the v1 reader's strict-version
+      refusal of v2+ blobs. The variant scope is non-mutating:
+      [`crate::variants_bridge::VariantScope`] wraps the SystemInstance
+      and exposes lookup-time accessors that hide dropped components
+      without touching the parsed model. JSON output adds top-level
+      `variant` and `feature_model_hash` fields; text output prefixes
+      the summary line with `(variant=<name>)`. Track E commit 6/8 of
+      the v0.8.0 migration design research, wiring the spar-variants
+      consumer crate (REQ-VARIANT-001) into the verify/enumerate
+      pipelines (REQ-MIGRATION-005, REQ-MIGRATION-006).
+    status: planned
+    tags: [migration, variants, track-e, track-b, v080, cli]
+
   - id: REQ-NETWORK-004
     type: requirement
     title: Typed network graph extraction from a SystemInstance

artifacts/verification.yaml

@@ -1626,6 +1626,53 @@ artifacts:
       - type: satisfies
         target: REQ-MIGRATION-004
 
+  - id: TEST-MOVES-VARIANT
+    type: feature
+    title: spar moves verify/enumerate variant integration tests
+    description: >
+      Integration tests in crates/spar-cli/tests/moves_variant.rs that
+      shell out to the `spar` binary and exercise the variant-aware
+      flags on `spar moves verify` and `spar moves enumerate` (Track E
+      commit 6/8). Coverage:
+      (1) verify with --variant-context filters the analysis surface to
+          the kept subset and emits ok=true plus a top-level
+          `variant` field for the petrol-only fixture;
+      (2) --component pointing at a dropped-by-variant subcomponent
+          yields a "not part of variant <name>" diagnostic and
+          non-zero exit;
+      (3) enumerate with --variant-context excludes processors gated
+          on a missing feature from the candidate list;
+      (4) --variant-context accepts both a filesystem path and `-`
+          (stdin) per the v1 contract's CLI section;
+      (5) --variant NAME shells out to rivet via $RIVET_BIN / $PATH;
+          a test seam (SPAR_VARIANT_TEST_RIVET_OUTPUT env var)
+          short-circuits the shell-out so CI runners without rivet
+          can still cover the implicit-form code path end-to-end;
+      (6) --variant NAME with no rivet on PATH and no $RIVET_BIN
+          emits the documented diagnostic that points back to the
+          explicit form and the contract doc;
+      (7) any rivet_spar_context_version other than "1" is refused
+          with a clear error message, satisfying the contract's
+          strict-version-rejection clause;
+      (8) JSON output includes both `variant` and `feature_model_hash`
+          top-level fields when a variant context is active, supplying
+          the audit-trail metadata MCP / rivet downstream consume.
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar --test moves_variant
+    status: passing
+    tags: [migration, variants, track-e, track-b, v080, cli]
+    links:
+      - type: satisfies
+        target: REQ-MIGRATION-008
+      - type: satisfies
+        target: REQ-VARIANT-001
+      - type: satisfies
+        target: REQ-MIGRATION-005
+      - type: satisfies
+        target: REQ-MIGRATION-006
+
   - id: TEST-SPAR-NETWORK-GRAPH
     type: feature
     title: Network graph extraction tests

crates/spar-cli/Cargo.toml

@@ -22,7 +22,9 @@ spar-sysml2.workspace = true
 spar-solver.workspace = true
 spar-render.workspace = true
 spar-codegen.workspace = true
+spar-variants.workspace = true
 etch.workspace = true
+la-arena.workspace = true
 rowan.workspace = true
 salsa.workspace = true
 serde.workspace = true
@@ -32,6 +34,5 @@ serde_json = "1"
 toml.workspace = true
 
 [dev-dependencies]
-la-arena.workspace = true
 rustc-hash = "2"
 proptest.workspace = true