Track E: Frozen-platform/mobile-application split + hypothetical-rebinding oracle

[avrabe]

Problem

spar's allocation analyses verify one binding at a time. Three real workflows are blocked:

1. Platform-vs-application split: Today AADL mixes both freely; no formal way to declare "the platform is fixed; only the application can move".
2. Hypothetical-binding queries: "If I move component X from CPU A to CPU B, do all my deadlines and bandwidth budgets still close?" — requires running analyses on a tentative binding without committing.
3. AI/LLM design-space exploration: An AI agent should be able to propose moves and have spar verify them deterministically, with spar as the certifying oracle and the LLM as the search heuristic. The certification chain stays in spar; the LLM's judgment never enters the safety case.

This is needed for incremental architecture redesign on existing E/E platforms.

Acceptance

• New property set `Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason}`
• Verification mode: `spar moves verify --component X --to Y` returns pass/fail per analysis pass with violations
• Enumeration mode: `spar moves enumerate --component X` lists valid targets within `Allowed_Targets`, ranked by slack/objective
• Solver extension: hypothetical-binding mode in `spar-solver` (MILP variant that doesn't mutate state)
• MCP tool surface: `spar.verify_move(component, target)` and `spar.enumerate_moves(component)` so LLM agents can drive design-space exploration with spar as the deterministic correctness oracle
• Integration with rivet variants (v1 contract from docs: rivet <-> spar variant binding contract v1 (proposed) #144): mobile components can also be variant-conditional
• Documentation: how an AI agent should drive design-space exploration with spar as the oracle
• Rivet traceability for new requirements

Research scope (in flight)

Subagent dispatched 2026-04-25 to survey: existing component-placement tooling (OSATE2 binding, Stood, Bauhaus, PolarSys CHESS), AUTOSAR BSW/RTE/SWC + Adaptive AUTOSAR's manifest format, multi-objective allocation literature (NSGA-II for AADL deployment), LLM + constraint-solver patterns, MCP tool design for verification oracles. Refined acceptance criteria land based on the research output.

Notes

• The MCP boundary is the certification-critical detail: LLM never crosses into the deterministic analysis path
• `Allowed_Targets` is the AUTOSAR-style platform-API contract hook
• Solver enumeration cost is bounded by `Allowed_Targets` cardinality, so explicit constraints help scalability
• ~6-8 weeks scope, touches `spar-solver`, `spar-cli`, new `spar-moves` crate