[devin-ai-integration]

What and why

Two families of result values were left bare in the default run although -schedule explore proves more than one outcome. Both are fixed with the existing orderMarks representation (no second marking mechanism, no explore re-run). The rule throughout: a value is marked if and only if exploration proves more than one outcome for it.

A. Values reached through a part (sensor.raw written by racing branches, sensor.scaled = raw * 10, z := sensor.raw, zz := sensor.scaled): none carried a mark — not even plain attributes once the action declared a part. Root cause: ActionExecutor.ResultsWithError derives what each part's object holds (collectPartsHeld → GetFeatureValue), and every top-level derivation begins a run of its own (beginRun → nestRun → a fresh runState that stays installed), so the marks and choice points of the run just ended were gone before any surface read them. ResultsWithError now reads under the executor's own run (enterRun(e.driven.state)). Separately, an object's feature valued by an expression recorded nothing of what it read: Instance.materializeDerived now calls the same Context.deriveMarks the action's own bound attributes use, so sensor.scaled stands where raw does. placeNamed accepts <part>.<name> for a feature no performer owns.

A place is the part's: lower.Place.Via is the feature a chain reaches the place through (footprintBuilder.place), and for a write-order choice or a derivation the run makes on an object, the part that object is held as (Instance.heldBy). Whether two such places hold one value is the run's to decide, not the declarations' — features may alias (ref part twin = cell), so Place.Conflicts, the checker's independence relation, stays conservative and ignores Via. Context.heldAlike (the two parts denote an object in common) is applied where marks are read (orderMarks.of), replaced (at/rewrite), met at a choice point (ChoicePoint.meets) and reported (placeNamed → partNamedHolds): left.raw racing leaves right.raw, right.scaled and a read of them bare, while twin.mark written beside cell.mark races it.

B. A sibling branch reading a feature its sibling writes in the same step (a { x := 1 } beside b { z := x }): touchMeeting touched only the place written. It now touches what the reading alternative writes from the read — the body statements whose data flow reads the place (lower.Footprint.Flows, one flow per statement, built in footprintBuilder.statements; Footprint.WritesReading), or every write when the read is a guard's or the move is described whole. The place read is no longer touched by a write/read meeting: one write of it stands whichever order ran, and explore shows x = 1 in every linearization — a mark on it would be the false positive the rule keeps out. A pin is each performance's own, delivered to rather than raced for, and is neither touched nor a read that touches (shared).

Specification basis

KerML 1.1 §9.2.4 Occurrences / §9.2.6 Performances (HappensBefore holds between the occurrences a succession joins and between a send and its accept; nothing orders concurrent branches), so a bare default-run value asserts a determinism the specification does not give. A feature chain names the feature it reaches (KerML 1.1 §7.3.4.6), so sensor.raw is one place whatever path writes or reads it — the feature of the object the part denotes, which another part of the same definition does not denote and a reference part bound to it does. Moves the order-dependence marking row in docs/project/spec-compliance.md (status unchanged, ✅; implementation and test columns extended).

Behaviour changes

• sensor.raw, sensor.scaled, z, zz (chained fixture) report orderDependent: 2 on every surface (REPL text, -json, gRPC order_dependent, trace Touches); the two-level chain car.engine.rpm marks the value read from it; a chained read of a place no branch races stays bare; with two parts of one definition, a race on left.raw leaves right.raw, right.scaled and a value read from them bare; a reference part bound to a part (twin = cell) races it.
• A once-written feature read by a racing sibling is no longer marked; the reader is. Rule: a value is marked iff exploration proves more than one outcome for it — x := 1 beside z := x gives z orderDependent: 1 and x bare (develop marked x and left z bare). Trace choice … order-dependent: <names> lines move the same way (details below).
• An action with parts no longer loses its marks at reporting time (previously every value of such an action printed bare).
• The checker's reduction is unchanged: Place.Conflicts is as conservative as before.

Fallout (measured)

• New fixtures (7): action_order_chained_write_of_racing_writers, action_order_chained_two_level_write, action_order_chained_read_of_unraced_stays_bare, action_order_sibling_read_of_racing_write, action_order_chained_parts_apart (two parts of one definition), action_order_chained_alias_of_racing_writers (ref part twin = cell), state_order_guard_and_effect_read_racing_write (a junction branch's two effects under a guard read racing the sibling's write: both marked, both vary) — each with .expected.json (explored admissible set), .check.expected.json, three trace goldens, and sections in docs/project/behavior-semantic-oracle.md.
• New test: order_marks_differential_test.go:TestOrderMarksAgreeWithExploredOutcomes — over every action_order_* and state_order_* case with an admissible set (23), the names the default run marks equal the names exploration finds at more than one value. Two pre-existing disagreements are pinned by name with their reason (not re-recorded): action_order_explicit_argument_binds_pin marks fixed/lit.result because a performed action's footprint is dynamic and stands on every mark; action_order_send_payload_from_racing_writer reports the accept's payload twice, marked as receiver.msg and bare as msg.
• Existing trace goldens moved: 34 files / 14 fixtures, 1 line each, all order-dependent: name lists; every movement matches the fixture's .check.expected.json divergent set:
  • statement-order choices (4: action_explore_statement_order_{calc,dependent,if,read_first} seed-1): x/v → y/doubled — the once-written place is fixed, the value written from the read varies.
  • due-order (clock_action_state_due_together, 3): lit → sawLit (the watcher's read result varies; lit is written once).
  • do-step vs dispatch (state_concurrent_inline_do_bodies 3, state_do_step_cuts_nested_perform 3, state_do_step_cuts_typed_do 3): + i / + n — the do body's counter written from a read the other move writes.
  • junction fixtures (state_junction_{guards_read_once,beyond_a_draw_read_once,drawn_as_its_transition_fires} + _metadata, 18): d/armed → route — the guard read makes the branch's effect dependent; the guarded attribute itself is written once.
• Unit test expectations changed (2): choice_test.go:TestNotesOfATransitionBlockedBeforeFiringAreDropped — the region-order choice now stands order-dependent with no names (level is written once; the blocked guards write no feature); cmd/sysml/check_engine_test.go:TestEngineCheckWitnessOfBehaviorsOnOneClockReplays — the lamp witnesses' choice line names saw (the action's read result, which the check's own line reports as ends as false or true) instead of lit, which the machine writes once at t=3. Each test's subject is unchanged.
• No .expected.json of an existing fixture moved; no "schedule": "declared" pinning was needed.
• PSSM referee (pssm-referee -check): pass 56 / fail 6 / not-expressible 34 / differs-by-design 7 — reproduces the committed baseline.
• Pilot execution referee (pilot-exec-diff, 514 cases, develop → branch): identical buckets — agree 229, kind-only 1, order-only 0, disagree 38, differs-by-design 5, pilot-unevaluated 167, pilot-silent 24, pilot-error 7, ours-error 10, ours-undetermined 17, both-error 16, nondeterministic 0.
• WASM (GOOS=js -tags sysml_re, gzip -9): develop 15,251,297 → branch 15,257,496 bytes (+6,199, +0.04%); budget 15,600,000 untouched.
• make test-shard SHARD=runtime (-race): green at the current head (2593 s); no allocation bound moved.

Pre-existing gaps met and left alone

• Pins are never marked (touch excludes them), so keep.v in object_flow_merge_shared_input varies under explore but prints bare.
• The accept payload's bare alias (msg) is unmarked while receiver.msg is marked (pinned in the differential test).
• A performed action's outputs stand on every mark (dynamic footprint), e.g. lit.result from a literal argument (pinned).
• The %check surface reports only the action's own features, not part.attribute names; a reference part's features are not among the reported results.
• Running the explore-vs-marks differential over every state fixture with an admissible set (100 cases) disagrees on 31, all but one bare where exploration varies (log/hits/order appended by both regions at a completion-pool, do-step or run-to-completion choice; state_join_segment_reads_its_payload marks left/right that do not vary). None of their trace goldens moved in this PR; the state-surface marking of those choice kinds is a separate gap.
• Not met: the SMT engine's refusal of = expr attributes; %satisfy label format.

How it was verified

go build ./..., go vet ./..., gofmt -l . empty, go test ./internal/exec/runtime/ ./internal/ir/... ./internal/exec/... ./internal/frontend/... ./tests/grpc/... ./cmd/sysml/, the -race runtime shard, make docs-check, scripts/check-doc-ids.py, scripts/changelog.py check; the explore-vs-marks differential above; both referees before/after; manual CLI runs of both finding models (-action, -json, -schedule explore).

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (docs/internals/design/scheduling.md, oracle sections, compliance row)
• Changelog entry added as changes/unreleased/order-marks-chained-places.fixed.md
• baselines regenerated and make docs-counts run if a gate count moved (no gate count moved)
• No internal work-item labels in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/dd66ed592fb6499ea1ffe0ec2fbe8493
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/dd66ed592fb6499ea1ffe0ec2fbe8493?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