[avrabe]

The solver named processors by their dot path (Top.impl.cpu2) and kept
each thread's binding as its raw target (cpu2). allocate (ffd/bfd) and
milp match the two by string, so they never matched. On the published
v0.46.0 binary, (reference (cpu2)) applies to app.t gives:

warning: Thread 'Top.impl.app.t' pre-bound to unknown processor 'cpu2'
Unallocated threads:
  Top.impl.app.t

ModelConstraints::from_instance now resolves the binding from the
component that declared it (actual_processor_binding_with_overlay,
REQ-AADL-REF-CONTEXT-001) and records that processor's dot path, which is
how processors names it. An unresolved binding keeps its text, as
before. The unit test that sets the binding directly on a thread still
sees cpu1.

Oracles:

• CLI tests: the pre-bound thread stays on Top.impl.cpu2 with no
  "unknown processor" (red on v0.46.0: unallocated), and a binding to a
  missing cpu9 is still reported as unknown;
• spar analyze does not use the solver. Full-output corpus diff
  anyway: 462 runs, 451 instantiating, identical;
• cargo-mutants (spar-solver, spar): 2 mutants, both unviable, since the
  change is a closure inside map. The hand mutant that matters,
  reverting to the raw binding text, IS v0.46.0's behaviour, and the CLI
  test fails on it.

Refs #498, #508

🤖 Generated with Claude Code

https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!