fix(runtime): interleave executors due at one instant move by move

[devin-ai-integration]

What and why

Executors due at one instant (two actions, an action and a state machine, two machines) are unordered, but under explore, check, replay and seed:<n> the executor drawn from the due order ran all its work at the instant before any other could move. Two actions that each read a shared counter and then write it never reached the lost update: both reads before either write.

The executor drawn now makes one move, then keeps its turn only while its next move is independent of everything each other due executor may still do at the instant; otherwise the due order is drawn again.

runDue / runTurn:
  owner := pickDue(due)
  loop:
    owner.runMove()
    if !owner.dueWork() || ctx.contended(owner): redraw
yieldTurn redraws when contended(driver) || endContended(driver)
contended(w)    = nextFootprint(w).DependentBy(futures.executorFuture(rival), ctx.relation(w, rival)) for some rival
endContended(w) = mayEnd(w) && some rival may still move   // an end observes every place

• future_footprint.go: an executor's future at the instant is everything it may still do, stopped only at a wait on a literal delay that resolves past the instant. gate() gathers every send any executor may make at the instant; a machine's future then leaves out a transition whose signal no queued message carries and no gathered send can meet (cannotFire), unless some executor may send anything.
• message_dependence.go Context.relation + lower.Footprint.DependentBy(g, rel): two executors on two objects commute on direct accesses to features each object holds itself (Relation.Held); a send naming no target (Channel.Own) meets no consumer run for another object. A send and an accept, or two accepts, are separated only where both signal types resolve statically and do not conform; an unresolved type, a via route, an unresolved receiver or port, and a dispatch that may drop the message all stay dependent.
• advance.go Context.endContended: a move that may end the driver's performance (an action token past no unguarded succession, out of a nested frame, or reaching beyond its node; a machine that can complete or terminate) yields to any rival still able to move, since the run's outcome is read at that end.
• -engine check holds the same turn: invocationRun.turn limits the enabled moves to the held executor, is part of the canonical state (turn: line) and is saved and restored with each frame. The persistent-set reduction uses the same DependentBy with the same relation, and persistentClosure.include now follows future dependence from every unit it adds, enabled or not; a do behavior stepping a stated flow contributes that flow's token footprints.
• StateExecutor.runMove reports whether the machine ran a unit at all, not only whether it bumped the event or do-step counters, so resuming a held entry or completing the machine counts as its move and a turn goes on through the rest of the instant's work.
• A callee a body performs that pauses at its start-shot move is marked held, as one paused on its waits already is, so the clock leaves it to the body that resumes it instead of running it as a due executor of its own.
• declared and reverse keep their order: the executor drawn runs its work at the instant through (scheduler.interleavesTurns).

Specification basis

Kernel Semantic Library Clocks.kerml / Occurrences.kerml: two performances waiting on the same TimeInstantValue are HappensBefore-linked by nothing, so their steps interleave. The spec-compliance.md rows for executors due at one instant and for the model checker's moves now describe move-by-move turns; both stay Faithful.

How it was verified

• New cmd/sysml/explore_turns_test.go:TestExploreRunsAHeldEntryAsAMove: a held entry cascade with a Go queued behind it and an action reading what the cascade writes. Every explored and seeded run dispatches Go at the instant (inner+b), and explore reaches the read between the cascade and the dispatch (order = 12; seen = 1).
• New cmd/sysml/explore_turns_test.go:TestExploreInterleavesExecutorsMoveByMove: the read-then-write pair reaches 3 outcomes under explore (complete) and check (witness replayed), seeds 1..12 reach all three, and declared/reverse keep seen = 0, seen = 1 / seen = 1, seen = 0. It fails on develop (2 outcomes, no seed reaches the lost update).
• Check's reduction: TestCheckReductionIsSound passes (reduced finals equal unreduced). Final outcome sets over the reduction corpus against develop: unchanged in 17 models, strictly larger in 2 (por_state_send_accept +1, por_state_join_exit +6), none lost.
• The spacecraft showcase (runs=500), TestExploredRunsAreGivenOneObjectPerInstantiate and TestExploredPathsAreCheckedAgainstTheDeclarations reach their develop outcomes at their unchanged budgets.
• go build ./..., go vet ./..., gofmt -l ., go test ./... (pilot library XMI downloaded), go test -race ./internal/exec/runtime/..., make lint, python3 scripts/changelog.py check pass. make docs-check fails only on docs/project/third-party-notices.md linking docs/assets/landing/libavoid-js.LICENSE.txt, which develop does not carry either.

Expectations that moved

Test	develop	This branch	Why
reduction_expected.txt por_state_effect_write, por_state_guard_read	17 18 17 18	15 16 17 20	same finals; reduction now separates a turn's moves
por_state_do_write	34 36 34 36	46 50 56 68	same finals; each do step is a move the read depends on
por_state_send_accept	9 9 9 9	13 13 13 13	one more final outcome
por_state_join_exit	72 72 72 72	96 108 102 120	six more final outcomes
por_state_join_guard	26 24 26 24	34 38 36 42	same finals; more interleavings of the join's guard
por_constructor	19 21 19 22	18 21 18 21	same finals; constructors on two objects commute
repl explore Comms::Craft::ack	2 outcomes, complete	3 outcomes, complete	new seen = 1; sent = 2: look reads sent before tx's count at t=3, which then runs before ack ends
cmd/sysml nested linked pair (explore, machine alone and siblings)	complete (4 runs): received = 1 ×3, received = 2 ×1	complete (5 runs): received = 1 ×4, received = 2 ×1	same 2 outcomes; the received = 2 witness draws the due order at t=3 twice
repl linked pair RunFor	complete (4 runs)	complete (5 runs)	same outcomes
lamp explore -advance (run_test, repl)	complete (2 runs)	complete (3 runs)	same outcomes
lamp -engine check peek+glow	10 states, 9 moves, witness of 1 choice	9 states, 8 moves, witness of 2 choices	same divergence (saw false or true); the witness names the turn's redraw

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/5344039f62464badb7a0a648e6384b08
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/5344039f62464badb7a0a648e6384b08?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

This branch now conflicts with develop. Conflicting files, and the merged PRs that changed them:

• docs/project/spec-compliance.md (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864 and later docs merges)
• internal/exec/runtime/model.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)
• internal/exec/runtime/scheduler.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)
• internal/exec/runtime/testdata/check/reduction_expected.txt (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)
• internal/ir/lower/footprint.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)

To resolve: merge current develop into this branch with an ordinary merge commit (no rebase or force-push).
Reconcile the code conflicts with #864's statement-order scheduling (calc, constraint and case-step bodies) rather than taking one side; a conflict that needs a design decision should be raised on this PR, not guessed.
Regenerate reduction_expected.txt with its test's update flag after the code merge rather than hand-merging it.

Planned merge order for the execution PRs: #844 → #850 → #838 → (#851 → #853 → #857) → #830 → #833 → #842 → #837 → #834 → #816.

Re-run the full gate (go build ./..., go vet ./..., gofmt -l ., make lint, make docs-check, go test ./...) and wait for green CI before marking ready.

[devin-ai-integration]

Hold on pushes: please don't push to this branch, including develop merges or empty commits to retrigger CI, until a maintainer says the CI runners are free. Prepare the conflict resolution locally and push it then.