[avrabe]

threads_for_processor compared the last segment of each thread's binding
with the processor's NAME. Two different processors that share a name
(left.cpu and right.cpu, both cpu) each collected both threads. On
the published v0.46.0 binary, spar codegen --verify proof on that
model emits a scheduling theorem that charges t 6 ms of interference
from a thread running on the OTHER processor: 6 + 6 = 12 ms against a
10 ms deadline, which is a false theorem. With one processor per node
named both cpu and left.cpu, each proof collected all four threads
instead of its two.

The binding now resolves from the component that declared it
(actual_processor_binding_with_overlay, REQ-AADL-REF-CONTEXT-001) and is
compared by identity. An unresolved binding keeps the old name
comparison.

Oracles:

• CLI tests on the generated Lean: one theorem with no foreign
  interference; two theorems where a processor really has two threads
  (both red on v0.46.0);
• unit test: each same-named processor gets exactly its own thread, by
  instance path. cargo-mutants found that bound == proc_idx flipped to
  != SURVIVED the CLI tests: both threads are t and codegen --verify proof names each processor's Lean proof by the processor's NAME — two processors named cpu write one file, the second silently overwrites the first #510's file
  collision hides which proof survives. It is caught by this test;
• cargo-mutants (spar-codegen, spar): 1 caught, 1 unviable, plus that
  survivor, now caught.

Found while writing this: both processors also write
proofs/cpu_scheduling.lean, so one proof overwrites the other (#510).

Refs #498, #510

🤖 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

❌ Patch coverage is 98.38710% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-codegen/src/lib.rs	98.38%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!