fix(runtime): explore every order of unordered statements in calc, constraint and case bodies

[devin-ai-integration]

Depends on #840 and #829 and must merge after both. Both are merged into this branch, so until they land the diff against develop also shows their commits; the changes of this PR are the two commits fix(runtime): explore every order of a calc or constraint body's unordered statements and fix(lower): leave the steps of a case stating no succession unordered plus the merge resolutions, the self-model's scheduler choice-kind count (now thirteen, for the new guard-order choice) and the pilot baseline's re-recorded examples digest.

What and why

A calc body ran its statements in declaration order inside one step, and explore/-engine check reported that single answer as proved. For

calc def Ord { return : Integer;
  attribute y : Integer := 1;
  assign y := y * 10;
  assign y := y + 2;
  y }

the library admits 12 and 30, but explore said r = 12, proved over schedules: 1 linearization, and check said no violation, exhaustive. Constraint bodies (#829), guards evaluating them, and analysis/verification case steps with no succession hid orders the same way.

• Calc and constraint bodies. Statements no then relates are unordered among themselves. explore, -engine check, replay and seeded schedules reach every order; the body stays atomic (no other performance runs between its statements) and the result expression / condition is evaluated after them. Independence reuses fix(runtime): explore the order of a body's statements no succession orders #840's footprints (lower/statement_order.go CalcBodyStatementOrder, ConstraintBodyStatementOrder), so commuting statements add no choice. Nested if/while/for and action-usage blocks inside calcs are covered. then between two of a constraint body's own statements now orders them instead of being refused.
• One choice per invocation. A pure calc or constraint whose body reorders, itself or through a callee (runtime/order_analysis.go reordersTransitively), is one statement order choice point between the distinct results its orders produce (runtime/invocation_statement_order.go), memoized per arguments within the outermost such invocation. A recursive order-dependent calc therefore explores its two outcomes in two runs instead of one choice per level.
• Guards. A decision/transition guard, change trigger, entry guard or terminal condition whose verdict depends on statement order chooses between the distinct verdicts, an evaluation error being its own alternative (runtime/guard_statement_order.go). Inside a nested preview an order-dependent verdict, and a guard whose constraint body may write outside its performance, fail with a typed not-covered error. A check property is violated when any order violates it.
• Bounds. A local order sweep is capped at 1024 evaluations; hitting it is reported as the statement orders bound by check and as incomplete by explore, never as proved or exhaustive.
• Compiled calcs. Under the ordering schedules a calc whose body (or callee) reorders is interpreted instead of compiled; run keeps compiled speed.
• Case steps. An analysis or verification case stating no succession leaves its steps unordered, as an action definition's subactions are, so explore/check interleave them.
• Fixed schedules. declared and reverse (the default) run calc and constraint bodies and unordered case steps in declaration order, as they do nested action bodies, so default results do not move. (Reversing case steps would have moved an existing Monte Carlo test, so they keep declaration order.)
• A stated succession in a calc body is refused naming the construct ( `first` statement) instead of a Go type name.

Existing fixtures whose bodies meant an order got an explicit then: calc_iterative_factorial, calc_output_assigned_in_body, calc_block_flow_node_unvalued_pin, calc_collection_ops_in_while_loop, calc_rk4_lunar_descent, constraint_body_steps, constraint_body_steps_order. No existing expectation or trace golden changed.

Not in this PR: -constraint, -requirement and -validate still evaluate once under the default schedule when -schedule explore is given (they label the result observed).

Specification basis

SysML v2 7.19/7.20: a calculation body is an action body, and Actions.sysml makes assignments, ifSubactions and loops subactions, which no succession orders. Cases.sysml makes case steps subactions likewise. Rows moved in docs/project/spec-compliance.md: a new calc/constraint unordered-statement row (⚠️ Approximate: the fixed schedules use declaration order, a tool-defined linearization), the constraint-body row, and the case-steps row (✅ → ⚠️ for the same reason).

How it was verified

• Conformance: calc_explore_statement_order ({12, 30}; default 12; trace goldens under default, declared, seed-1), _commuting, _declared, _derived, _recursive, _recursive_deep, _then, _then_unordered; constraint_explore_statement_order; action_guard_statement_order; state_transition_guard_statement_order; analysis_explore_step_order (+ traces, _declared), verification_explore_step_order (+ _declared), analysis_case_step_order_commuting, analysis_case_step_order_stated.
• TestRuntimeRobustnessAtomicBodyOrder (budget exhaustion reports incomplete under explore and a bound under check, construct-named refusal, SMT not covered, deep recursion ends in a typed budget error, impure guard refused, enclosing-binding calls not memoized) and the case-step robustness test.
• lower unit tests for calc/constraint/case orders; parser golden calc_statement_succession; SMT atomic_body_order_test.go.
• go build ./..., go vet ./..., gofmt -l . (empty), make lint, make docs-check, python3 scripts/changelog.py check, go test ./internal/exec/... ./internal/ir/... ./internal/check/... ./internal/translate/... ./internal/frontend/repl/... ./tests/..., go test -race ./internal/exec/runtime/.
• Run counts (TestExecutionConformance$|TestCheckConformance, against develop + fix(runtime): explore the order of a body's statements no succession orders #840 + feat(runtime): execute constraint-body steps and complete model-determined extents #829 without this PR): no existing case's outcome or run count changed across 128 counter-bearing cases; the new fixtures run in 2–3 runs each.

Checklist

• make test and make lint pass locally (make lint and the package suites above pass; full make test is left to CI)
• 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/27169e4b94084c969cd9f23e601f6d11
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/27169e4b94084c969cd9f23e601f6d11?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