feat(cli): spar moves verify — hypothetical rebinding oracle (Track E commit 3/8)

artifacts/requirements.yaml

@@ -1175,6 +1175,34 @@ artifacts:
     status: planned
     tags: [migration, track-e, v080]
 
+  - id: REQ-MIGRATION-005
+    type: requirement
+    title: spar moves verify CLI — hypothetical-rebinding oracle
+    description: >
+      System shall expose a `spar moves verify --component X --to Y`
+      CLI subcommand that returns a structured pass/fail report with
+      violations, using the BindingOverlay from REQ-MIGRATION-004.
+      The pipeline parses the AADL model, instantiates the requested
+      root, resolves --component and --to to ComponentInstanceIdx
+      values via FQN matching against the instance hierarchy, builds a
+      single-move overlay, runs overlay validation (frozen /
+      allowed-targets), and runs the standard analysis-pass suite
+      (RTA, latency, bandwidth, EMV2, ARINC653, …) against the
+      un-overlayed instance for commit 3. The report carries `ok`,
+      component / target FQNs, a Violation list (Frozen /
+      AllowedTargets / AnalysisError variants), and a per-pass
+      diagnostic stream keyed by analysis name. Output is rendered as
+      either text (developer-friendly) or JSON (canonical
+      machine-readable contract for the v0.9.0 MCP `spar.verify_move`
+      tool surface). Exit codes: 0 = ok, 1 = analysis errors, 2 =
+      overlay violations. For commit 3 only the HIR-level
+      property-lookup helper (`actual_processor_binding_with_overlay`)
+      is overlay-aware; widening the analysis suite itself to consume
+      the overlay is commit 4. Per Track E commit 3/8 of the v0.8.0
+      migration design research (§6.3).
+    status: planned
+    tags: [migration, track-e, v080, cli]
+
   - id: REQ-NETWORK-004
     type: requirement
     title: Typed network graph extraction from a SystemInstance

artifacts/verification.yaml

@@ -1481,6 +1481,46 @@ artifacts:
       - type: satisfies
         target: REQ-MIGRATION-002
 
+  - id: TEST-MOVES-VERIFY
+    type: feature
+    title: spar moves verify CLI integration tests
+    description: >
+      Integration tests in crates/spar-cli/tests/moves_verify.rs that
+      shell out to the `spar` binary and exercise the
+      `spar moves verify` subcommand (Track E commit 3/8). Coverage:
+      (1) admissible move emits ok=true and exit 0;
+      (2) unknown --to argument exits non-zero with the offending name
+          mentioned on stderr;
+      (3) unknown --component argument behaves the same way;
+      (4) Spar_Migration::Frozen component yields exit 2 and a
+          structured Frozen violation carrying the Pinned_Reason;
+      (5) target outside Spar_Migration::Allowed_Targets yields exit 2
+          and an AllowedTargets violation citing the offending target;
+      (6) error-severity analysis diagnostics are surfaced into the
+          per-pass diagnostic stream and (when present) raised as
+          AnalysisError violations with exit 1;
+      (7) --format text emits a single OK/FAIL summary line plus
+          human-readable violation lines;
+      (8) --format json emits a JSON document with the documented
+          schema (ok / component / target / violations /
+          diagnostics_by_pass);
+      (9) running `spar moves verify` does not mutate the underlying
+          model — `spar analyze` returns identical output before and
+          after, and the AADL file on disk is unchanged;
+      (10) a trivial move whose target equals the declared binding is
+           reported as ok with no violations.
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar --test moves_verify
+    status: passing
+    tags: [migration, track-e, v080, cli]
+    links:
+      - type: satisfies
+        target: REQ-MIGRATION-005
+      - type: satisfies
+        target: REQ-MIGRATION-004
+
   - id: TEST-SPAR-NETWORK-GRAPH
     type: feature
     title: Network graph extraction tests

crates/spar-cli/src/main.rs

@@ -1,6 +1,7 @@
 mod assertion;
 mod diff;
 mod lsp;
+mod moves;
 mod refactor;
 mod sarif;
 mod verify;
@@ -41,6 +42,7 @@ fn main() {
         "extract" => cmd_sysml2_extract(&args[2..]),
         "generate" => cmd_sysml2_generate(&args[2..]),
         "lsp" => cmd_lsp(),
+        "moves" => moves::cmd_moves_dispatch(&args[2..]),
         other => {
             eprintln!("Unknown command: {other}");
             process::exit(1);
@@ -62,6 +64,9 @@ fn print_usage() {
     eprintln!("  render     Render architecture SVG from an instantiated system");
     eprintln!("  verify     Verify requirements against analysis results");
     eprintln!("  codegen    Generate code from an instantiated system model");
+    eprintln!(
+        "  moves      Hypothetical-rebinding oracle (verify a move under the migration overlay)"
+    );
     eprintln!("  lsp        Start Language Server Protocol server (stdin/stdout)");
     eprintln!();
     eprintln!("Options:");
@@ -83,6 +88,9 @@ fn print_usage() {
     eprintln!(
         "  codegen  --root Package::Type.Impl [--output dir] [--format rust|wit|both] [--verify all|build|test|proof] [--rivet] [--dry-run] <file...>"
     );
+    eprintln!(
+        "  moves    verify --root Package::Type.Impl --component <fqn> --to <processor> [--format text|json] <file...>"
+    );
 }
 
 fn cmd_lsp() {