[devin-ai-integration]

What and why

The SMT engine refused every action holding a feature valued by an expression over other features (attribute y : Integer = x + 1): the states carried only values written, so before the refusal the encoder held y at its initial value and proved y = 1 where the interpreter computes y = x + 1 at every read (explore: y ∈ {2, 3}, z ∈ {12, 13} on the reproducer). The refusal was sound but left all such actions outside SMT coverage — the referee stood at 17 encoded / 53 refused, the six most recent refusals being the fixtures that exposed the gap.

This PR encodes the binding and keeps refusing only what the encoding does not cover.

Design

Representation: a per-state defined term, plus substitution where a move's writes make the state's value stale.

• Each derived feature y = expr keeps its state variable y@k (so results, witnesses, -check-property, enumeration and the two-copy sensitivity queries read it exactly as any other feature), but it is never framed by featureValues: every state k = 0 … K asserts y@k = ⟦expr⟧(s_k), the expression evaluated over the state's own feature variables (Encoding.deriveValues). A chain (v = y * 2) defines v@k over y@k.
• Inside a move, a read of y before any write uses y@k; after a write in the same move (env.written, kept across the merge of if branches and of loop iterations) the read is substituted by ⟦expr⟧ over the move's current symbolic environment (env.evaluate), so a statement that writes x and then reads y in one body sees the fresh value, as the interpreter's read-time evaluation (deriveBodyCell) does; chains substitute recursively. Guards are evaluated over the post-body environment, so a guard reading y after a write of x sees the derived term too.
• Definedness: a derived feature whose value may be undefined — a side condition such as a divisor, or a read of a feature that may hold none — is refused (Encoding.checkDerived): the interpreter settles every still-tracking binding when the performance completes (freezeBodyCells) and fails then even if nothing read it (y : Rational = 10 / x; assign x := 0 ends in error: division by zero), a failure the relation does not carry. Every encoded derived feature is therefore always defined.
• A derived feature is not an input: it is neither pinned at a value nor free in state 0 (Result.Inputs no longer lists it); state 0 asserts the same defined term over the initial values, which is where -check-input free features and -check-assume meet it — an assumption over y constrains expr over the released inputs it reads (tested).
• A result of a feature the interpreter holds as a one-element sequence (a bare out p : Integer parameter, see below) is spelled as such (Output.Sequence, [2]), so the solver's outcome identities match explore's.

Loops and -check-unroll. Nothing specific: a loop condition is evaluated over the current environment at every unrolled iteration, which gives it y@k before the body writes and the substituted term after; the past-bound flag is untouched. -check-unroll only changes how many iterations are evaluated.

Result and -check-property reads. Both read the state variables: a property over y at step k reads y@k, which the defined term ties to x@k; a result reads y@K. Outputs() is unchanged apart from the sequence spelling.

What is refused, each naming the feature and its reason

• a derived feature whose footprint the lowering cannot resolve (Footprint.Dynamic: a chain through a computed object);
• a derived feature whose declared type narrows its sort (attribute y : Natural = x + 1): the interpreter checks the bound value against the type at each read, which the encoding does not perform;
• a derived feature whose value may be undefined (attribute y : Rational = 10 / x, or one reading an optional feature): settled by the interpreter at completion, failing then even unread;
• an assignment to a derived feature (assign y := 7): the interpreter then holds the written value until the next write, a mark the encoding does not carry;
• -check-input releasing a derived feature (free a feature it reads instead).
• A cycle among derived features (y = w + 1; w = y * 2) never reaches the encoder: the interpreter refuses it at the start of the performance (cyclic feature value dependency: y), which -engine smt reports as not covered; pinned by TestDerivedFeatureRefusals/cycle.

Finding left alone: a bare out parameter is held as a one-element sequence

The interpreter holds out yBase : Integer = 5 (no multiplicity, no attribute keyword) as the sequence [5] and spells it so in explore and in run results; out yBase : Integer[1] = 5 and out attribute r : Integer are scalars, and an out parameter without a value of its own that redefines one by position (out yRace : Integer; over out yBase : Integer = x + 1) is a scalar even when yBase is [2]. That is internal/exec/runtime behaviour, unchanged here; the encoder now spells such a result as the interpreter does (Output.Sequence) so the referee compares like with like, and action_order_positional_bound_read_of_racing_writer.expected.json lists yBase as a Sequence among its outcomes (it listed yBase under orderDependent but not under outputs, which the referee's sensitivity check requires). Whether a bare out parameter should be scalar-valued is the maintainer's call.

Specification basis

KerML 1.1 §7.3.4.2 Feature values (a feature-value binding = expr values the feature by the result of expr; an initial value := expr is evaluated once), §7.3.4.5 (a redefining feature valued by nothing of its own is bound as the redefined one is) and §7.4.2 (parameters redefine positionally) — the interpreter implements the binding as read-time evaluation (deriveBodyCell). Moves the SMT model-checking row of docs/project/spec-compliance.md (coverage of feature values; 🧩 Extension unchanged) and the order-dependence row's smt/encode.go pointer (it named the refusal).

Behaviour changes

• sysml -engine smt (and %engine smt, the gRPC engine) now encodes actions holding features valued by an expression over other features; the refusal a feature valued by an expression over other features is computed as it is read; the states carry only values written is gone. No fixture, golden or test pinned that message (only the changelog fragment bound-feature-read-marks.fixed.md and the compliance row mentioned it).
• New refusals: a feature valued by an expression whose reads the lowering cannot resolve is not encoded; a feature valued by an expression that may have no value (a side condition, or a feature it reads holding none) is not encoded: the interpreter settles it when the performance completes, failing then even unread; …, with a declared type narrowing its sort, is not encoded: the value is checked against the type at each read; assignment to <f>: a feature valued by an expression over other features holds the value written until written again; …; -check-input <f>: action <a> values it by an expression over other features; free a feature it reads instead.
• Result.Inputs of an smt answer no longer lists a derived feature among the inputs (it was listed pinned at its starting value).
• A witness or outcome value of a feature the interpreter holds as a one-element sequence is spelled [v] as explore spells it.

Fallout

Category	Moved	Why
Conformance .expected.json	6	solverBudget: {"moves": 20} on the six fixtures holding a derived feature: every run of theirs ends within 8 moves; at the default 40 moves cvc5 1.3.4 answers unknown to the referee's fixed-outcome query within the default 10 s solver timeout (z3 decides it in 3–7 s; cvc5 decides it in 3 s at 20 moves). This is the knob the corpus README documents for exactly that case; the referee's completion query still proves every run ends within 20.
Conformance .expected.json	1 (of the 6)	action_order_positional_bound_read_of_racing_writer lists yBase (Sequence of one Integer) in both outcomes, which the referee's sensitivity check requires of every feature the encoding holds.
Runtime, traces, CLI/REPL/gRPC goldens	0	—
SMT referee	17 encoded / 53 refused → 23 encoded / 47 refused, 23 agreeing; 49 witnesses, 49 replayed; 62 features compared across schedules, 41 sensitive with both witnesses replayed, 21 not sensitive (before: 37/37, 42/24/18; yBase of the positional fixture is the extra feature compared)	the six fixtures encode; no other case moved. The remaining 47 refusals are the pre-existing ones (statement order, body interleaving, nested flows, messages, repeated-step features, pin bindings, invocations).
Referee oracle (sensitivity_test.go)	oracleValue reads Sequence values	the positional fixture's yBase

How it was verified

• Failing-first: TestDerivedFeaturesAgreeWithExplore refused the six fixtures at the first commit; it now encodes each, enumerates the solver's completed outcomes, replays every witness and asserts the solver's value set per feature equals explore's, with y ∈ {2, 3}, z ∈ {12, 13}, x ∈ {1, 2}, w = 1 pinned on the reproducer; the seventh case holding a derived feature is a calculation with no flow (ErrMalformedFlow, logged, not a pass).
• TestDerivedFeatureInGuardAndProperty: a guard reads the derived value after the write (y > 3 takes the branch), a chained feature follows (v = 12), a loop condition over the derived value sees each iteration's write (while y < 4 { assign x := x + 1; } completes at x = 3; y = 4; before the merge kept the written mark it was bounded), a property over the derived feature is proved (y == x + 1) and another violated (v < 12), and an assumption over y constrains a released input n (violated without it, proved with it).
• TestDerivedFeatureRefusals: the assignment, release, narrowing-type and may-be-undefined refusals, and the interpreter's cycle refusal.
• TestRefereeCorpus whole corpus under z3 4.8.12 (counts above). The derived tests also pass under cvc5 1.3.4 (OPENSYSML_SMT=cvc5).
• CI: internal/exec/smt runs in the suite (quick tier and the model race shard) with OPENSYSML_REQUIRE_SMT=1 set workflow-wide, so an absent solver fails rather than skips; solve.Discover prefers z3, which the workflow installs. The dedicated "solver gate" steps that grep for --- SKIP cover internal/exec/solve and internal/frontend/repl under z3 and cvc5 but not this package — so under cvc5 the SMT engine's own tests are not gated in CI (they pass locally).
• go build ./..., go vet ./..., gofmt -l . empty, go test ./..., make docs-check, python3 scripts/check-doc-ids.py, python3 scripts/changelog.py check.
• No runtime code changed (no PSSM/pilot referee or WASM delta to report).

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