feat(smt): encode features valued by an expression over other features

changes/unreleased/smt-derived-features.added.md

@@ -0,0 +1 @@
+- The `smt` engine encodes a feature valued by an expression over other features (`attribute y : Integer = x + 1`) as the interpreter computes it, at every read over the current values: each state defines the feature by its expression and every read within a move substitutes it, through features so valued in turn, so guards, loop conditions, properties, assumptions and results all see the derived value. Such an action was refused (`a feature valued by an expression over other features is computed as it is read`). One whose reads the lowering cannot resolve, one whose declared type narrows its sort, one whose value may be undefined (the interpreter settles it at completion), an assignment to one and a `-check-input` release of one are still refused, each naming its reason; a cycle among such features is refused by the interpreter at the start, before any encoding.

docs/internals/design/smt-model-checking.md

@@ -135,6 +135,7 @@ verdict names it.
 | Tokens | `ActionExecutor.tokens`, ids assigned on spawn | `T` **token slots**, `T` computed from the graph: the widest set of tokens `k` moves can hold, one per fork branch reachable within the bound, plus one per nested flow. `at_i[t]` is a finite datatype over the graph's nodes with `Absent`, `Done` and `Parked` |
 | Node performances | `stepToken`, `stepJoinNode`, `stepMergeNode` | `joined_i[j]` — how many of join `j`'s incoming successions have delivered. A merge keeps no state: it is one performance per arrival, so a token at a merge is described by its slot alone |
 | Feature values | `Instance.FeatureValues`, `actionFrame.data` | one variable per scalar feature per state, `x_i`, in the sort the translator already gives the feature; a frame-local feature is one per (node performance, feature) |
+| Features valued by an expression | `deriveBodyCell`: `attribute y : Integer = x + 1` is computed at every read over the values then held (a FeatureValue that is not initial, KerML 1.1 §7.3.4.2; `:= expr` is evaluated once and then written like any value) | `y_i` is kept for every state so results, properties and the two-copy query read it as any feature, but never framed: every state asserts `y_i = ⟦x + 1⟧(s_i)` instead, and a read of `y` within a move — a body statement, a guard, a loop condition — substitutes the expression over the move's current environment, so a statement writing `x` and then reading `y` in one body sees the fresh value as the interpreter does. A chain (`v = y * 2`) substitutes recursively. The feature is no input: state 0 asserts the same term over the initial values, which is where `-check-input` free features and `-check-assume` meet it. Refused, each naming its reason: one whose reads the lowering cannot resolve (`Footprint.Dynamic`), one whose declared type narrows its sort (the interpreter checks the bound value at each read), one whose value may be undefined — a side condition such as a divisor, or a read of a feature that may hold none — which the interpreter settles at completion and fails then even unread, an assignment to one (the interpreter then holds the value written) and a `-check-input` release of one; a cycle among such features (`y = w + 1; w = y * 2`) never reaches the encoding, the interpreter refusing it at the start of the performance (`cyclic feature value dependency`) |
 | Pins and object flows | `PinBinding`, `DataFlows`, delivered `out` pins | the value carried on an object flow is a variable set by the source node's move and read by the target's |
 | Messages | `Context.messages`, oldest first | a bounded bus of `M` slots, each `(present, signal type, payload, posted-at)`, `M` computed as the number of `Send` statements reachable in `k` moves |
 | Clock | `Context.Clock()`, `accept after`/`at` | `now_i : Real` (seconds) and a due time per parked token; `now` never decreases and advances only when no token is enabled, to the earliest due time — time is not a choice, only ties are, as the explicit note says. There is no horizon: `k` moves alone bound the run. The library's `Clocks` and `Occurrences`, and `accept after`/`accept at` over them, fix *when* a timed accept becomes enabled and say nothing about how far a run proceeds; fUML, PSCS and PSSM define no clock at all. A horizon would be a bound the specification does not name, so the rule that adds nothing is the one taken, and `-advance` stays refused for `smt` as `check` refuses it |
@@ -362,6 +363,7 @@ solver answers and `explore` confirms.
 | Successions, fork, join, decision with translatable guards | encoded | yes | — |
 | Merge, merge-loop | encoded; a back edge is a succession like any other, so a merge-loop's iterations are bounded by `k`, not unrolled | yes, to `depth` | a loop still live at `k` sets `cut_k`: *no violation within k moves*, not *proved* — unless k-induction closes it |
 | Body `assign` of Boolean, Integer, Natural, Rational, Real, enumeration, variation features; `if`; local `Declare` | encoded through the existing translator | yes | — |
+| Features valued by an expression over other features (`attribute y : Integer = x + 1`), chains of them | encoded as a per-state defined term and substituted at every read within a move | yes | an unresolvable footprint, a narrowing declared type, a value that may be undefined, an assignment to one or a release of one: *not covered* naming the feature; a cycle among them is the interpreter's refusal at the start |
 | Quantities with units | encoded, normalized to base units as exact rationals | yes | proof is qualified *over exact arithmetic* when the evaluator rounds |
 | Feature chains grounding in a scalar of the performing object | encoded | yes | — |
 | Object-valued pins, chains through an object a pin carries, `new` | not encoded: no heap | yes | *not covered: dynamic target at node* — a bounded heap of `N` objects per type is a later stage |