Guaranteed / Possible envelopes

The envelope answers a proactive question: by the time control reaches node X, what state is actually set? This is distinct from what’s legal to read (governed by schema import). The envelope tracks two sets per node, scoped to run.* / user.* only — the tiers whose writes are monotonic (“once set, stays set,” so union/intersect over predecessors is sound). Quest scratch fields (quest.<id>.*) are excluded; “was it reachable at X” is answered directly by completed(Q) / active(Q) in the route structure.

• Guaranteed(X) — set on every declared route to X.
• Possible(X) — set on some declared route to X.

Both are a graph-lift of defassign’s own lattice: each node’s guaranteed-write set is computed by the definite-assignment walk, then propagated by structural recursion over the formula AST:

visited(Y):   G = Guaranteed(Y) ∪ G(Y)      P = Possible(Y) ∪ P(Y)
completed(Q): G = P = writesOnComplete(Q)
active(Q):    G = ∅                         P = writesOnComplete(Q)
X && Y:       G = G(X) ∪ G(Y)               P = P(X) ∪ P(Y)
X || Y:       G = G(X) ∩ G(Y)               P = P(X) ∪ P(Y)
entry node:   G = P = D

D, the entry base case, is the set of run.*/user.* paths carrying a schema default — reused verbatim from the import layer. D ⊆ Guaranteed(n) at every node, matching definite-assignment’s “a defaulted path is always assigned” invariant lifted to the whole graph. This structural recursion is provably identical to a per-route ∩/∪ computation, never materializing the exponential route set.

active(Q) is strictly weaker than completed(Q)

This is the one place the two quest atoms diverge. completed(Q) licenses the assumption quest.Q.state == complete, so everything the quest’s required objectives and its <on quest complete> handlers write — writesOnComplete(Q) — lands on both sides of the table. active(Q) licenses only “Q reached active”: those completion writes have not necessarily run, so they contribute to Possible and to Guaranteed not at all.

Take a quest findkai whose required objective writes run.kaiFound, a scene gated after: 'active("findkai")' that reads it, and a second scene gated after: 'completed("findkai")'. Only the second one is safe:

$ lute scenario --project . envelope --node narrator.s01ep02
project root: .
envelope for scene(narrator.s01ep02) (pre-entry — state available when control REACHES this node, before its own writes):
  Guaranteed (safe to read under your declared routes):
    - run.greeted   written by: (nothing on a declared route reaching here — schema default only)
  Possible (set on SOME but not every declared route reaching this node; the Guaranteed paths above are not repeated):
    - run.kaiFound   written by: …
  Guaranteed facts (hold on every declared route reaching this node):
    (none)
  Possible \ Guaranteed -- warning-grade reads (set on SOME but not every declared route; suppressed by default in whole-project `check`, surfaced here):
    - ./scenes/whileActive.lute:13:36: state path `run.kaiFound` is set under your declared routes on SOME routes reaching this node, but not every one — not yet guaranteed; order this scene `after:` a scene every route passes that sets it, or guard the read with `has(run.kaiFound)`

Swap that node’s after to completed("findkai") and run.kaiFound moves into Guaranteed, leaving Possible \ Guaranteed empty. (run.greeted carries a schema default, so it is in D and guaranteed under both.)

Reading a quest’s completion write from a scene gated on active is therefore the Possible \ Guaranteed warning-grade class — which is correct, and is exactly the mistake the atom exists to make visible rather than to hide.

Reading the tables

lute scenario --project <DIR> envelope --node <NODE> prints both tables. The diagnostic reads for a state path P at node X:

• P ∈ Guaranteed(X) → safe under your declared routes; no diagnostic.
• P ∉ Possible(X) → no declared route ever sets P before X — error grade, E-STATE-MAYBE-UNAVAILABLE, shipped by default in whole-project lute check.
• P ∈ Possible(X) \ Guaranteed(X) → set on some but not all routes — warning grade, default-suppressed to this command’s output only. This is the Possible \ Guaranteed read whole-project lute check computes and drops by default.

Every message carries the verbatim “under your declared routes” qualifier (A-hybrid posture).

Writers on alternative edges

Each Guaranteed path lists who wrote it (written by:). A writer counts only when it is provably before the node: a scene on an alternative edge — one of several that may have led here, where any one suffices — is listed apart, under also written, but not provably before this node:. The alternative edges are the [raises] edges and, since 0.52 (#209), the [accept] edges. An edge that also carries an ordering kind (an after: atom, [start]) still orders. With scenes a and b each running ::set{run.x = 1} and ::accept{quest="q"}:

$ lute scenario --project . envelope --node quest:q
envelope for quest(q) (pre-entry — state available when control REACHES this node, before its own writes):
  Guaranteed (safe to read under your declared routes):
    - run.x   written by: (nothing on a declared route reaching here — schema default only); also written, but not provably before this node: scene(a), scene(b)
  Possible (set on SOME but not every declared route reaching this quest; the Guaranteed paths above are not repeated) -- inventory only: unlike a scene's, this list is not a set of warned read sites; a quest's guard reads are checked where they are written, not against this table:
    (none)
  note: this quest declares no `follows` attribute, so this is the defaults-only `D` table; quest:q is accept-driven, and an accept activates it whatever `follows` says, so `follows` is never an entry route and would not enrich this table.

On 0.51 both scenes were listed as writers provably before q.

Guaranteed facts

Beside the scalar tables, the envelope carries the fact envelope (dsl 0.20.0): the relational facts that hold on every declared route reaching the node. It is the same must-set whole-project lute check uses to decide relational guards (see how whole-project lute check analyzes relational guards), propagated over after: with the same structural recursion as Guaranteed — visited(A) contributes what holds when A ends, && unions, || intersects, completed(Q)/active(Q) contribute nothing. Only monotone facts cross a scene boundary: nothing may retract them, no other assert may share their key: with a different value, and their relation is neither reserved: nor engine-open; tier: scene/tier: quest facts never cross. Each fact names what establishes it — an assert site, a facts: seed, or a rule.

From the Haven example, the purser scene (ep09):

$ lute scenario --project docs/examples/haven envelope --node haven.s01ep09
…
  Guaranteed facts (hold on every declared route reaching this node):
    - awake(ottavio) (docs/examples/haven/scenes/stowaway.lute:20)
    - awake(vesna) (`facts:` seed)
    - found(ottavio) (docs/examples/haven/scenes/stowaway.lute:19)
    - knows(ottavio, manifest) (docs/examples/haven/scenes/stowaway.lute:23)
…

Episode 6 asserts all three of Ottavio’s facts outside any branch, and every route to ep09 passes through it, so a guard holds('found', ['ottavio']) in ep09 could never close — which is why that scene’s listTheMass choice carries none. knows(vesna, manifest) is absent even though three other documents assert it: none of them lies on every route to ep09 (hydroponics is one of two alternatives, the archive is optional, and the purser ledger’s assert holds only inside its own lore entry, which the engine presents at a time of its choosing). When whole-project lute check reports W-FACT-GUARANTEED on a guard, this table is where the fact comes from. With --json the same list is envelope.guaranteedFacts, an array of { "fact", "establishedBy" } objects.

Quest addressing

lute scenario --project <DIR> envelope --node quest:<id> prints a real table for every quest:

• A quest whose follows is its route — one with a start, or a subquest that activates with its parent — and that declares it → the full Guaranteed/Possible tables, computed exactly like a scene’s.
• An accept-driven quest (no start) → the defaults-only D table, follows or not. An accept activates it in the middle of whatever accepted it, so nothing that scene writes is guaranteed at its entry, and since 0.53 its follows is ordering metadata, never an entry route; without follows the note says that declaring one would not enrich the table.
• Any other quest without follows → the defaults-only D table (never empty, never an error), plus a one-line note that declaring follows would enrich it beyond defaults-only.

A quest is reactive — <quest start> may fire at the earliest possible instant, so nothing beyond schema defaults can be soundly guaranteed at quest entry unless the author opts into a graph position with follows. The reactive diagnostic side (“is this specific guard’s read safe?”) is already handled by defassign on the quest’s own guards.