From f92bfa938de428d3b19e1097646b53d9ee9501d1 Mon Sep 17 00:00:00 2001 From: Christian Wendler Date: Tue, 16 Jun 2026 15:15:03 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20Lumens=20rev=203.5=20=E2=80=94=20Codex?= =?UTF-8?q?=20soundness=20pass=20(totality/bounds/determinism=20+=20fixes)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Independent adversarial review (Codex gpt-5.5, high reasoning; saved verbatim at docs/protocol/reviews/codex-rev3.4.md) tested SOUNDNESS where the internal passes tested expressibility, and found a real layer they missed. rev 3.5 addresses all of it (several default decisions, flagged for veto): Soundness (new §2.9): - Totality: ÷0 / mod0 / overflow / NaN / Infinity → defined result or halt with surface_error; string index/slice clamped; mandatory else. - Bounds: numerics feeding range/pad/size-ops MUST declare max (validator rejects unbounded range(score)); per-op output caps. - Determinism: canonical record-key order (no engine-observable object order); {random}/{now} as seeded nodes (were missing from the AST catalog). Effects + replay: - §6.4: deterministic effectId, declaration-order firing, on:transition XOR on:{when}, logical-time debounce/coalesce recorded in the trace. - §13.5 (new): replay/recording model — logical clock, effect-id-tagged result re-feed, const content-hash in every frame. - §2.6: normative kernel determinism contract (seed/tie-breaks/float); per-kernel numbers stay an L0 deliverable, the contract does not. Contradictions fixed: defs may read state (§2.8); effect args may read {event} (§6.4); assetRef split from dataRef (§1.1, asset handle vs structured projection); captureLongPress in EventBinding (§4); StateDelta transition root + non-overlapping multi-set (§2.5); concept §3 stops calling map/filter/fold std-lib. Security: free-colour chrome/consent SPOOFING closed — consent/auth prompts are host chrome outside the Lumen subtree with unforgeable attribution (§3.1); the state/DataRef-derived → external-effect TAINT rule made a static AST walk (§6). Refinements: PortType + port read/emit + expose addressing (§7); hit-test order/tie-breaks/drag capture (§4.1); loadData lifecycle + cap accounting (§1.1); dirty-track is optimisation-not-semantic (§5); surface_capability_* wire schema (§12); capabilityClasses → brokeredCapabilitySupport (§13); {var path} record- only (§2.2). §11 security table + §14 reclassification updated; walkthrough examples updated to rev-3.5 grammar; concept v0.11. Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/interactivity-concept.md | 19 +- docs/lumens-spec.md | 285 +++++++++++++++++++++++--- docs/protocol/lumen-walkthroughs.md | 27 ++- docs/protocol/reviews/codex-rev3.4.md | 89 ++++++++ 4 files changed, 380 insertions(+), 40 deletions(-) create mode 100644 docs/protocol/reviews/codex-rev3.4.md diff --git a/docs/interactivity-concept.md b/docs/interactivity-concept.md index 4b164f0..0f22eca 100644 --- a/docs/interactivity-concept.md +++ b/docs/interactivity-concept.md @@ -17,6 +17,16 @@ > only** — no implementation, no PR > plan. It extends, and stays inside, the architecture in `CONCEPT.md`. +Version 0.11 — **Codex soundness pass.** An independent adversarial review +(`docs/protocol/reviews/codex-rev3.4.md`) tested *soundness* where the internal +passes tested *expressibility*, and found a real layer: totality (÷0/overflow/ +`NaN`), the static-bound hole (un-`max`'d numerics feeding `range`/`pad`), +determinism (record-key order, effect-replay ordering, `const`-in-replay), plus +self-contradictions and two security findings (free-colour chrome spoofing, the +taint claim). All addressed in `lumens-spec.md` rev 3.5 (§2.9 totality/bounds/ +determinism, §6.4 effect determinism, §13.5 replay, §1.1 `assetRef`, §3.1 anti- +spoofing, §6 taint walk). Lesson reinforced: independent adversarial review finds +a *different axis* than self-review — worth the cost before implementation budget. Version 0.10 — **reference set complete.** Tracing the last three reference Lumens (workflow / defrag / map) in real LX-AST added only **interaction-surface** items, no core-model gaps — the expected convergence: per-event payload schema @@ -287,10 +297,11 @@ Turing-complete in the dangerous direction. - **Values.** numbers, booleans, strings, lists, records, and typed `state` references. No closures over host objects, no `this`, no prototypes. - **Operators & built-ins.** arithmetic, comparison, boolean logic, - `if`/`match`, record/list construction, and a fixed standard library - (`map`, `filter`, `fold`, `range`, `min`, `max`, `len`, string ops, a small - math set). The standard library is a **whitelist** — same discipline as the - primitive vocabulary. + `if`/`match`, record/list construction, dedicated **iteration binder nodes** + (`map`/`filter`/`fold` — *not* higher-order std-lib functions, so no + first-class functions are exposed; `lumens-spec.md` §2.2), and a first-order + std-lib (`range`, `min`, `max`, `len`, `lookup`, string ops, a small math set). + Both are **whitelists** — same discipline as the primitive vocabulary. - **Bounded iteration only.** `map`/`fold`/`range` over collections whose size is bounded by `state` (itself size-capped). No `while`, no general recursion. This is what makes the gas bound a *static* guarantee rather than diff --git a/docs/lumens-spec.md b/docs/lumens-spec.md index 111f036..4eff410 100644 --- a/docs/lumens-spec.md +++ b/docs/lumens-spec.md @@ -88,6 +88,26 @@ is a spike deliverable; where prose and schema disagree, the **schema wins**. > (§6.4) for hot-path effects like persist-on-pan. All five reference Lumens are > now expressible end-to-end ([`protocol/lumen-walkthroughs.md`](protocol/lumen-walkthroughs.md)). +> **Rev 3.5 (Codex soundness pass).** An independent adversarial review +> ([`protocol/reviews/codex-rev3.4.md`](protocol/reviews/codex-rev3.4.md)) tested +> *soundness* where the internal passes tested *expressibility*, and found a real +> layer they missed. Addressed: **§2.9** (new) — **totality** (÷0 / overflow / +> `NaN` → defined result or halt), **provable bounds** (numerics feeding +> `range`/`pad`/size-ops MUST declare `max`), **determinism** (canonical +> record-key order; `{random}`/`{now}` as seeded nodes); **§6.4** effect +> determinism (deterministic `effectId`, declaration-order firing, `on`-XOR, +> logical-time debounce); **§13.5** (new) replay/recording incl. `const`-hash in +> every frame; **§2.6** a normative kernel determinism contract (per-kernel +> *numbers* stay an L0 deliverable, the *contract* does not). Contradictions +> fixed: `defs` may read `state` (§2.8); effect `args` may read `{event}` (§6.4); +> `assetRef` split from `dataRef` (§1.1); `captureLongPress` in the schema (§4); +> `StateDelta` transition root + non-overlapping multi-`set` (§2.5). Security: +> free-colour **chrome/consent spoofing** closed (§3.1 host-only trust surface); +> the **taint** rule made a static walk (§6). Plus refinements (PortType §7, +> hit-test order §4.1, dirty-track semantics §5, capability wire schema §12, +> `brokeredCapabilitySupport` §13). *Several are default decisions, flagged for +> veto.* + A Lumen is the Omadia answer to "an interactive artifact": **declarative data, not code**, run by a small deterministic interpreter on Tier 1, generated and brokered agentically on Tiers 2/3, safe to share and to save as a preset @@ -188,7 +208,8 @@ type StateSchema = { | { type: 'list', of: StateLeaf, maxLen: number, init: unknown[] } | { type: 'record', fields: StateSchema, init: object } | { type: 'grid', w: number, h: number, of: StateLeaf, init?: unknown } // bounded 2D — boards, defrag cells - | { type: 'dataRef', projection: StateLeaf, init?: unknown }; // §6.1; loadData fills the declared projection + | { type: 'dataRef', projection: StateLeaf, init?: unknown } // §6.1 — loadData fills the declared STRUCTURED projection + | { type: 'assetRef', kind: 'pixel'|'audio'|'video'|'tile', init?: null }; // §6.1 — an opaque content-addressed BINARY handle (sprite/tile/media) }; ``` @@ -200,14 +221,24 @@ first-class: a board is a `list>`, a shape table a so total size stays statically capped. `ConstSchema` (§1.2) uses the identical leaf grammar with `value` in place of `init`. -A **`dataRef` leaf** declares the **read-only `projection`** shape that -`loadData` (§6) fills with a size-capped projection of the underlying `DataRef`. -LX reads it **as an ordinary value of that shape** — `{state: ref}` yields the -projected `list`/`record` directly (the runtime resolves the handle; LX sees the -data); before `loadData` resolves it reads as the declared `init`/empty. A -`dataRef` projection is **read-only** — no `set`/`setAt` may target it; local -edits live in a separate `state` field merged in the `view` (the §6.3 optimistic -overlay idiom). +**Two distinct ref leaves — do not conflate them.** A **`dataRef` leaf** is a +**structured** read-only `projection` that `loadData` (§6) fills (a `list`/ +`record` of data — menu rows, places); LX reads it **as an ordinary value of that +shape** — `{state: ref}` yields the `list`/`record` directly (the runtime +resolves the handle; LX sees the data). An **`assetRef` leaf** is an **opaque +binary handle** — the content-addressed `DataRef` of §6.1 (a sprite, tile, +audio); LX never reads its *bytes*, only passes the handle to a `scene` `sprite`/ +`media` node (§3) or a capability. The `scene` `sprite.dataRef` field (§3) and +generated-asset results are `assetRef`s, **not** `dataRef` projections. + +**Both are read-only, and have a defined lifecycle.** No `set`/`setAt` may target +a `dataRef`/`assetRef`; local edits live in a separate `state` field merged in +the `view` (the §6.3 optimistic-overlay idiom). A projection's **size counts +against the capability's own projection cap, not the 256 KB mutable-`state` cap**; +it does **not** persist in undo/replay state (it is re-fetched, content-addressed, +§6.1). Before `loadData`/`generateAsset` resolves, the leaf reads as its declared +`init` (an empty `projection` value, or `null` for an `assetRef`); resolution and +invalidation arrive as `surface_patch`/`surface_data_ref_*` (§6.1). Total serialised `state` size is capped (initial default **256 KB**, spike-tunable). `state` persists in canvas-state (`CONCEPT.md` §"State Model"); @@ -263,7 +294,7 @@ no prototypes, no functions-as-values beyond the named std-lib. | `const` | `{const: path}` | read an immutable `const` slice (§1.2); computed-indexable via `at`, exactly like `state` | | `event` | `{event: field}` | read a field of the triggering event | | `let` | `{let:{name:expr}, in:expr}` | bind a local (readable via `{var}`); lexically scoped, immutable; nest for multiple bindings | -| `var` | `{var:name}` · `{var:name, path:"f.g"}` | **read** a bound local — a `let` name or a `map`/`filter`/`fold` binder (`as`/`acc`); optional dotted sub-path into a record/list. The *only* way to read a binder; without it no `let`/iteration body can reference what it binds | +| `var` | `{var:name}` · `{var:name, path:"f.g"}` | **read** a bound local — a `let` name or a `map`/`filter`/`fold` binder (`as`/`acc`); optional dotted sub-path into **record fields only** (list/grid elements use `at`). The *only* way to read a binder; without it no `let`/iteration body can reference what it binds | | arithmetic | `{"+":[a,b]}` `-` `*` `/` `mod` | numeric | | comparison | `{">":[a,b]}` `>=` `<` `<=` `==` `!=` | boolean | | logic | `{and:[…]}` `or` `not` | boolean | @@ -332,11 +363,16 @@ static pass proves iteration bounds and a gas ceiling. `view` MUST return a vali primitive/scene tree (§3); `transitions` MUST return a value conforming to `state`. Anything else → reject. -**Transition result = delta-merge.** A transition's value is the **current -`state` with its `set`/`setAt` paths applied** — unmentioned fields are carried -over unchanged. A transition does *not* reconstruct the whole record; `{set:{}}` -returns the state untouched (a no-op transition). This keeps transitions small -(touch only what changes) and patches local. +**Transition result = a `StateDelta`.** A transition's root node MUST resolve to a +**`StateDelta`** — a `set`/`setAt`, or an `if`/`match`/`let` whose branches each +resolve to one (a transition never returns a bare value or a full reconstructed +record; the root type is `StateDelta`, not `any`). The delta is **merged onto the +current `state`**: unmentioned fields carry over unchanged; `{set:{}}` is the +no-op. In a **multi-field** `{set:{a:…, b:…}}`, paths MUST be **non-overlapping +and unique** — overlapping (`a` and `a.b`) or duplicate paths are **rejected at +validation**, removing all order-dependence — and **every RHS expression +evaluates against the *pre-transition* state** (a `set` never observes a sibling +field's new value). This keeps transitions small and patches local. ### 2.6 Native kernels — bounded algorithms the host owns @@ -388,6 +424,20 @@ it is **audited native code with a hard internal ceiling**, not agent-authored control flow — so "cannot hang / cannot DoS" (§0.2) and determinism (§0.3) hold for kernels exactly as for the interpreter. +**Kernel determinism contract (normative now; per-kernel algorithms + numeric +defaults are an L0 schema deliverable).** Every kernel MUST be **byte-identical +across machines** for identical inputs. That requires, normatively: a **seed** +from the host context for any randomised kernel (`layoutGraph`'s `force` mode); +**total tie-breaks** (`sortBy` is stable on the original index; `pathfind` visits +neighbours in a fixed canonical order; `groupBy` emits buckets in canonical +record-key order, §2.9); and the **§2.9 numeric domain** (no `NaN`/`Infinity`, +defined rounding — banker's rounding on ties). A kernel `keyExpr`/predicate +callback is an LX expression evaluated in a **fresh scope binding only the +element (and optional index)** — it may `call` std-lib, `apply` defs and read +`const`, **not** `state`/`event`; its per-element cost is budgeted +`elements × eval` against kernel-gas. What stays deferred to the schema spike is +*which* algorithm and *which* numbers — **not** whether determinism holds. + ### 2.7 Declared invariants (silent-wrong → loud-error) A Lumen MAY declare `invariants` — boolean LX expressions over `state` that MUST @@ -431,6 +481,69 @@ They are also the natural shape the idiom library (§8) ships — a vetted `collides` or `scaleAxis` def is reused, not re-emitted. This is purely additive: no `defs` ⇒ identical behaviour to a Lumen that inlines everything. +§2.8 amends the §2.1 "no `state`/`event`" reading rule for defs: a `def` body +**MAY** read `{state}`/`{const}` (both immutable during a single evaluation, so +purity w.r.t. `(state, args)` holds), and **MAY NOT** read `{event}` (events flow +in as args). Passing a value as a **param** is required only to apply a def to a +*non-state, in-flight computed* value (e.g. a game-over check against a not-yet- +committed board). **Cycle detection is syntactic:** the call graph is the set of +`{apply}` targets reachable by a plain AST walk over **every** node of every +`body` (both `if`/`match` branches, regardless of feasibility); a cycle, an +unknown target, or an arity mismatch → reject. `params`, `defs`, std-lib and +kernel names occupy **reserved, non-overlapping namespaces**. + +### 2.9 Totality, bounds & determinism (normative) + +The §0 guarantees ("total", "bounded", "deterministic") are only real if every +operation is closed under them. This section pins the cases the node catalog left +implicit. *(Initial **default decisions**, spike-tunable where noted; flagged for +review.)* + +**Totality — every operation has a defined result on every input.** + +| Partial case | Normative result | +|---|---| +| `/` or `mod` by zero | **halt** the Lumen with `surface_error` (deterministic, loud — never `NaN`/silent) | +| arithmetic overflow / `NaN` / `±Infinity` produced by `*`,`pow`,`/`,… | **halt** with `surface_error` (numbers live in a defined finite domain, below) | +| `at`/`setAt` out-of-bounds | the declared `default` (read) / no-op (write) — already total (§2.2) | +| string index / `slice` out of range | clamped to `[0,len]`; empty where degenerate (never throws) | +| `match` with no matching case and no `else` | **reject at validation** (`else` mandatory unless cases are statically exhaustive) | +| `lookup` / kernel on empty or degenerate input | the declared `default` / identity result (§2.6) — never undefined | + +The **numeric domain** is IEEE-754 `float64` with `NaN`/`Infinity` **forbidden as +results** (their production halts). `int` operations stay exact within ±2^53; a +result outside halts. (Fixed-point is a spike option if cross-platform float +drift proves real; the *contract* — no `NaN`/`Infinity`, halt on overflow — is +normative now.) + +**Bounds — the static gas ceiling must be provable, not hoped.** + +- A **size-producing** op (`range`, `pad`, list/grid construction, a kernel that + emits a collection) takes its count/size from a **statically-bounded** integer: + a literal, or an `int` `state`/`const`/param leaf whose schema declares a finite + `max`. **Numbers that feed a size-producing op MUST declare a `max`** — the + validator **rejects** a `range({state:"score"})` where `score` has no `max`. + (So the §A.0 `score` leaf gains `"max"`.) This is what makes the gas bound a + *static* property rather than a runtime hope. +- Each op also carries a **per-op output cap** (schema-defined, spike-tunable); + exceeding it at runtime halts with `surface_error` (a second, dynamic guard + under the static one). + +**Determinism — identical `(state, const, event, seed)` ⇒ byte-identical result +on every machine.** + +- **Iteration order is defined:** `list`/`grid` in index order; **`record` keys in + canonical order = lexicographic by UTF-8 bytes.** `keys`/`values`/`groupBy` and + any record iteration follow this order, so object-key ordering is **never** + engine-observable. +- **`random()` / `now()` are nodes, not free calls** (closing their absence from + §2.2): `{random}` draws from a **per-Lumen seeded PRNG** advanced once per + evaluation in node-visit order; `{now}` reads a host timestamp that is + **constant within one transition/view evaluation** (per-event granularity). The + seed and the `now` value are part of the recorded `(…, seed)` tuple → replay + re-feeds them (§13.5). +- Kernels carry their own determinism contract (§2.6). + --- ## 3. The `scene` primitive (editor-class, 1.1) @@ -528,6 +641,17 @@ palette?: { [name: string]: ColorToken | sRGBHex }; // bounded, declared bra validated data (no code); `free` node colours are plain sRGB values in the draw-list. Colour freedom touches the *look* only — determinism, gas and default-deny capabilities are unchanged. +- **Anti-spoofing boundary (normative).** Because `free`/`brand` content can draw + *anything*, a Lumen could paint a fake Omadia chrome or a fake consent/auth + dialog (phishing). Two guards make that inert: **(1)** all **consent, + authorization and external-effect prompts are host chrome** rendered **outside** + the Lumen's drawable subtree, in Lume, carrying an **unforgeable host + attribution** — a Lumen can never draw into, overlay, or fabricate them, and a + Lumen-drawn lookalike has no effect (only the real host prompt can grant); + **(2)** the host reserves the consent/auth visual patterns and marks a + `brand`/`free` Lumen's region with a persistent **content-boundary + attribution** so a user can always tell host UI from Lumen-drawn UI. Colour is + opened; the **trust surface is not**. --- @@ -544,6 +668,7 @@ type EventBinding = { key?: string, // for 'key' — declared keys only (e.g. 'ArrowLeft','Space') rate?: number, // for 'tick' — declared, capped (≤60) — see §5 everyMs?: number, // for 'timer' + captureLongPress?: boolean,// for 'longPress' — take priority over the host context-invoke on this target (§4 rules) run: TransitionName, // the transition to evaluate }; ``` @@ -601,6 +726,15 @@ needs **no** per-node listener — one binding plus the payload's `hitId`/ `dropTarget`. All fields are host-supplied and deterministic for a given recorded input (replay-safe, §13.5). +**Hit-test determinism (normative).** "Topmost" = **last in draw order** +(`scene.draw[]` / tree order); on a tie (overlapping equal-depth nodes, inflated +44 pt areas overlapping), the **higher draw-index wins**, then the smaller node +`id` lexicographically — a total order, never ambiguous. A `drag` **captures** the +element resolved at `phase:"start"`: `item` stays fixed for the whole gesture, +`dropTarget` is re-resolved each `move`/`end`. Capture ends at `phase:"end"`. A +binding with no eligible target resolves `hitId`/`item` to `""` (the Lumen as a +whole) — total, never null. + --- ## 5. Cadence & motion @@ -621,7 +755,13 @@ type CadenceSpec = 'static' | 'reactive' | { tick: number /* Hz, ≤60 */ }; The runtime **dirty-tracks** changed `state` slices and re-evaluates only dependent `view` branches (retained-mode + memoisation); `requestAnimationFrame` is scheduled only while a ticking/animating region is live. **At rest a Lumen -costs ~0 % CPU** (kiosk-critical). +costs ~0 % CPU** (kiosk-critical). Dependency tracking is an **optimisation, not a +semantic**: dependencies are derived by **static extraction of the `{state}`/ +`{const}`/`{port}` paths each `view` sub-tree reads**, and a sub-tree whose +dependency set cannot be statically narrowed **falls back to re-evaluation on any +change**. A correct implementation MAY always re-evaluate the whole `view`; the +*result* is identical (determinism, §2.9) — dirty-tracking only changes *cost*, +never *output*. **Declarative animation ≠ LX tick.** *Presentation motion* (fade, glow-pulse, count-up, camera ease, Ken-Burns, parallax) is a **declarative animation** the @@ -672,10 +812,16 @@ compute (§0.2): per-capability **rate + quota**, a **max-in-flight** ceiling, **idempotent de-duplication** of identical in-flight calls, and **backpressure** when a broker saturates — so a ticking Lumen cannot move the DoS or cost problem onto Tier 2/3. Caps are spike-tunable initial defaults (§14). Egress that -carries data **derived from Lumen state or a `DataRef`** (an outbound `fetch`, a -`writeData`) is treated as `external-effect` — per-call confirmation — *unless* -the endpoint **and** request shape were pre-approved at grant time; a bare -`internal` `fetch` may not smuggle state-derived data past the confirmation gate. +carries data **derived from Lumen state or a `DataRef`** is treated as +`external-effect` — per-call confirmation — *unless* the endpoint **and** request +shape were pre-approved at grant time. **The taint rule is static and +mechanically decidable:** a capability `args` expression is **tainted** iff its +AST contains a `{state}`, a `{const}`-of-a-`dataRef`/`assetRef`, an `{event}`, or +an `{apply}`/`{kernel}` that (transitively) reads one; the validator computes this +by the same tree-walk as §2.5. A **tainted** arg to `fetch`/`writeData` ⇒ +`external-effect` (confirm per call) **unless** the grant carries an explicit +**request-shape schema** the args conform to *and* a pre-approved endpoint. A bare +`internal` `fetch` may not smuggle tainted data past the gate. The exact quota/idempotency/backpressure contract is a spike deliverable (§14). ### 6.1 Asset transport & content-addressed caching (never-stale) @@ -749,13 +895,13 @@ capability call. ```ts type EffectBinding = { - on: TransitionName | { when: LXNode }; // fire after this transition runs, or when this state predicate flips true + on: TransitionName | { when: LXNode }; // EXACTLY ONE: after this transition runs, XOR when this predicate flips false→true call: CapabilityName; // a declared §6 capability - args: LXNode; // pure LX over (post-transition) state → the request payload + args: LXNode; // pure LX over POST-transition state + the TRIGGERING event ({event:…}) → request payload onResult?: TransitionName; // the brokered result re-enters here as an event onError?: TransitionName; // failure / denial path (optimistic rollback) - debounceMs?: number; // coalesce rapid fires (e.g. persist-on-pan) — fire on settle - coalesceKey?: LXNode; // collapse in-flight calls sharing this key to the latest + debounceMs?: number; // coalesce rapid fires over LOGICAL time (§13.5), not wall-clock + coalesceKey?: LXNode; // collapse superseded in-flight calls sharing this key to the latest }; ``` @@ -780,6 +926,24 @@ transition (e.g. `persist` on a 60 fps `pan`) declares `debounceMs` to fire on settle and/or a `coalesceKey` to collapse superseded in-flight calls — the clean authoring form on top of the broker's hard egress cap. +**Determinism & ordering (normative).** Effects must replay identically: + +- **Deterministic instance id.** Each fire gets `effectId = + (transitionEvalSeq, effectIndex, fireCounter)` — the monotonic evaluation + sequence, the effect's position in `effects[]`, and a per-binding counter. +- **Ordering.** When one transition triggers several effects, they fire in + **`effects[]` declaration order**. `on:transition` and `on:{when}` are + **mutually exclusive** per binding (the type allows exactly one), so a single + state change never double-fires the same binding. +- **Logical-time debounce.** `debounceMs`/`coalesceKey` operate over the recorded + **logical event clock** (§13.5), not wall-clock; the emit-vs-suppress decision + for each `effectId` is **recorded in the trace**, so replay reproduces exactly + which calls fired. +- **Replay.** A brokered result/error is recorded against its `effectId` and + **re-fed in recorded order** on replay (§13.5) — the running Lumen treats it as + an external input, never re-issuing the real call. This is what lets a + capability-bearing Lumen replay/undo deterministically. + --- ## 7. Ports & wires — cross-element interaction @@ -788,6 +952,7 @@ A Lumen is a node in the same primitive tree; elements interact bidirectionally, deterministically, on Tier 1 (`interactivity-concept.md` §9.1). ```ts +type PortType = StateLeaf; // a port/expose value is a typed LX value — the §1.1 leaf grammar (scalar/list/record/grid), bounded type PortSpec = { name: string, dir: 'in'|'out', type: PortType }; // on primitives & Lumens — explicit, wired type ExposeSpec = { name: string, type: PortType }; // published read-only view-state, bindable by shared id WITHOUT a wire type Wire = { from: { ref: TargetRef, port: string }, to: { ref: TargetRef, port: string } }; // at container/canvas level @@ -815,6 +980,18 @@ type Wire = { from: { ref: TargetRef, port: string }, to: { ref: TargetRef (the agent owns which wires and published interfaces exist; the client owns the values flowing). +**Read/emit grammar & propagation (normative).** A Lumen reads an `in` port via +`{port:name}` (a typed value like `{state}`); it **emits** an `out` port by +including it in a transition's `StateDelta` (`{set:{"@portName": expr}}`, the `@` +prefix marking a port sink). A neighbour reads a published field via +`{exposed: , field: name}` — and **only** if that `` +declared that `field` in its `expose` and the reader is bound to it by shared id; +any other read is a validation reject (un-exposed state is unreadable). **Wire +propagation is single-pass and acyclic per evaluation:** the host topologically +orders wires by stable id; a cycle is rejected at validation; a port with no +wire/expose reads its declared `init`. So cross-element values resolve in a +**defined order**, deterministically, with no feedback loop. + --- ## 8. Lifecycle, presets & reuse @@ -905,6 +1082,10 @@ governs the host regardless of a Lumen's palette choice. | Untrusted shared/imported Lumen | Re-validated on import; capability manifest consent before first run; HMAC scoping; fork lineage | | Cross-element overreach | Port/wire **+ published-interface** least-privilege — a node reads only what is **wired or `expose`-published** to it; un-exposed state is unreadable (an imported Lumen sees no ambient neighbour state); declared, whitelist-validated, stable-id-resolved | | Non-reversible effects | `external-effect` class → confirmation-modal gate before the real call | +| Partial / non-total op (÷0, overflow, `NaN`) | Defined total result or **halt** with `surface_error` — never silent `NaN`/divergence (§2.9) | +| Non-determinism / replay divergence | Canonical record-key order, seeded `random`/`now`, ordered effect ids + recorded result re-feed, `const`-hash in every replay frame (§2.9, §6.4, §13.5) | +| Chrome / consent **spoofing** via `free` colour | Consent/auth/external-effect prompts are **host chrome outside the Lumen subtree** with unforgeable attribution; a Lumen-drawn lookalike is inert (§3.1) | +| Tainted egress (state/`DataRef`-derived) | **Static taint walk** over capability `args` → tainted ⇒ `external-effect` (confirm) unless grant carries endpoint + request-shape schema (§6) | --- @@ -922,6 +1103,10 @@ governs the host regardless of a Lumen's palette choice. agent-owned, bounded, not serialised; the unit the idiom/preset library ships. - **Helpers:** the `defs` section + `{apply}` node (§2.8) — named, parameterised, non-recursive pure functions (a DAG, fully inlinable; no new compute power). +- **Soundness & replay:** §2.9 totality/bounds/determinism rules + `{random}`/ + `{now}` nodes; the `assetRef` leaf (§1.1, split from `dataRef`); §13.5 replay + recording (logical clock, effect-id-tagged results, `const` hash). These pin + existing guarantees — no wire change, validator-enforced. - **Effects:** the `effects` binding list (§6.4) — the declarative trigger by which a *pure* transition causes a brokered capability call; result re-enters as an event; `debounceMs`/`coalesceKey` for hot-path effects. Reuses the §6 broker, @@ -941,7 +1126,11 @@ governs the host regardless of a Lumen's palette choice. - **Events:** `surface_capability_request` (client→Tier 2) and `surface_capability_result` (Tier 2→client) for §6 brokering; results may also arrive as ordinary `surface_patch`. Reuses the effect-classified action path - and `surface_action_result`. One optional new event family. + and `surface_action_result`. One optional new event family. **Wire schema:** + `_request {effectId, cap, argsHash, args}`; `_result {effectId, ok, result?, + error?, revisionId}` — correlated **by `effectId`** (§6.4) so results re-feed in + recorded order (§13.5); `argsHash` lets Tier 2 dedup idempotent in-flight calls + (§6 broker bounds). - **Presets:** `lumen-presets/**` + `lumen-state/**` memoryStore namespaces (§8). - **Handshake (§13):** client declares LX version, gas limits, scene support, granted capability classes, and **input modalities** alongside @@ -968,7 +1157,7 @@ handshake_select += { sceneSupport?: 'none'|'canvas2d'|'webgl', kernels?: KernelName[], // §2.6 native kernels this client implements kernelGasLimit?: number, // client's per-kernel-call gas ceiling - capabilityClasses?: CapabilityName[], // what this client can broker/render + brokeredCapabilitySupport?: CapabilityName[], // what this client can BROKER/RENDER — NOT a grant; grants live in the Lumen manifest + Tier-2 policy (§0.5) inputModalities?: ('touch'|'mouse'|'keyboard'|'pen')[], } ``` @@ -977,6 +1166,28 @@ A client may implement a subset (e.g. `scene` but not `tiles`); Tier 2 routes accordingly and idioms degrade gracefully — the same principle as `localOperations`. +### 13.5 Replay & recording (normative) + +Determinism (§0.3) buys replay/undo only if **every non-deterministic input is +recorded** and re-fed. A Lumen's replayable trace is a sequence of frames; each +frame records: + +- the **event** (type + §4.1 payload) and the **logical clock** tick it occurred + at (a monotonic counter — the basis for `debounceMs`/`coalesceKey`, §6.4, never + wall-clock); +- the host-seeded `(seed, now)` tuple consumed (`{random}`/`{now}`, §2.9); +- every **capability result/error** that arrived, tagged with its `effectId` + (§6.4), in arrival order, plus each effect's recorded emit/suppress decision; +- a **content hash of the `const` section** in force (`const` is not serialised + as state, §1.2 — but transitions depend on it, so a `const` patch changes the + hash and a replay across the change uses the matching `const` version; a hash + mismatch is a replay error, never a silent divergence). + +Replay re-evaluates `(state, const, event, seed, recorded-results)` and MUST +reproduce byte-identical state at every frame. No real capability call is +re-issued on replay; recorded results stand in. This is the single mechanism +behind Trace replay, undo/redo, safe sharing, and v2 lockstep multiplayer. + --- ## 14. Conformance & open questions @@ -1011,10 +1222,18 @@ caught-before-render failure. Preset/idiom **assembly** (§8) stays the primary path; novel cold authoring is a strong-model job with a real failure rate, and this gate plus declared invariants (§2.7) are its safety net. -Open tuning items (gas/frame/state caps, the **kernel-gas schedule and v1.1 -kernel cut**, wakeup-budget caps for `tick`+`timer`, the capability-broker egress -contract — rate/quota/max-in-flight/idempotency/backpressure, **session-scoped -consent budgets**, LX std-lib surface, scene perf ceiling, capability-consent -granularity, determinism-vs-real-time, LLM reliability emitting LX, preset -trust/distribution) are enumerated in `interactivity-concept.md` §13 — research -items, not unspecified holes. +**Reviewed (rev 3.5):** the [Codex adversarial pass](protocol/reviews/codex-rev3.4.md) +hardened the soundness layer. Note the boundary it forced: a **contract** that is +safety-critical is now **normative** (totality §2.9, the kernel determinism +contract §2.6, effect ordering/replay §6.4/§13.5, the egress/consent/taint +*semantics* §6) — only the **numbers and per-kernel algorithms** behind those +contracts remain tuning items. "Research item" is no longer a cover for a missing +*rule*, only for an unset *value*. + +Open tuning items — now strictly numbers/algorithms behind a fixed contract: +gas/frame/state caps, per-op output caps, the **kernel-gas schedule and v1.1 +kernel cut** + per-kernel algorithms, wakeup-budget caps for `tick`+`timer`, the +capability-broker egress numbers (rate/quota/max-in-flight/idempotency/ +backpressure), **session-scoped consent budgets**, LX std-lib surface, scene perf +ceiling, capability-consent granularity, LLM reliability emitting LX, preset +trust/distribution — enumerated in `interactivity-concept.md` §13. diff --git a/docs/protocol/lumen-walkthroughs.md b/docs/protocol/lumen-walkthroughs.md index e3c197f..ffa6ab3 100644 --- a/docs/protocol/lumen-walkthroughs.md +++ b/docs/protocol/lumen-walkthroughs.md @@ -42,7 +42,7 @@ y)` as indices into a `const` shape table. "pRot": { "type":"int","min":0,"max":3,"init":0 }, "pX": { "type":"int","min":-2,"max":11,"init":4 }, "pY": { "type":"int","min":-2,"max":21,"init":0 }, - "score": { "type":"int","min":0,"init":0 }, + "score": { "type":"int","min":0,"max":9999999,"init":0 }, // rev 3.5 §2.9: a numeric needs max if it can feed a size op "frame": { "type":"int","min":0,"init":0 }, "over": { "type":"bool","init":false } } @@ -238,7 +238,11 @@ game is accent-tinted; the 7-distinct-colours limitation noted earlier stands fo "colorMode": "brand", "palette": { "primary":"#DA291C", "ink":"#FFFFFF", "surface":"#1A1A1A", "pop":"#FFC72C" }, "state": { - "menu": { "type":"dataRef" }, // filled by loadData (read-only projection) + "menu": { "type":"dataRef", "projection":{ "type":"list","maxLen":200, + "of":{"type":"record","fields":{ + "sku":{"type":"string","maxLength":32}, + "name":{"type":"string","maxLength":80}, + "price":{"type":"int","min":0,"max":100000} } } } }, // loadData projection (rev 3.5: projection required) "cart": { "type":"list","maxLen":50, "of":{ "type":"record","fields":{ "sku":{"type":"string","maxLength":32}, @@ -499,7 +503,7 @@ camera pan/zoom, marker hit-testing, `persist`. "view": { "type":"record","fields":{ "cx":{"type":"number"},"cy":{"type":"number"},"z":{"type":"int","min":1,"max":19} }, "init":{"cx":0,"cy":0,"z":4} }, "tiles": { "type":"list","maxLen":64, "of":{"type":"record","fields":{ - "x":{"type":"int"},"y":{"type":"int"},"img":{"type":"dataRef"} } }, "init":[] }, + "x":{"type":"int"},"y":{"type":"int"},"img":{"type":"assetRef","kind":"tile"} } }, "init":[] }, // rev 3.5: assetRef, not dataRef "places": { "type":"dataRef", "projection":{ "type":"list","of":{"type":"record","fields":{ "id":{"type":"string","maxLength":32},"lat":{"type":"number"},"lon":{"type":"number"} } } } }, "sel": { "type":"string","maxLength":32,"init":"" } @@ -567,3 +571,20 @@ unchanged and unprovable on paper: **can an LLM emit valid LX reliably** — to measured on a built L1 interpreter, with `defs`/invariants/golden-trace as the net. An independent adversarial pass (Codex, as for rev 2) is the recommended next check before implementation budget. + +## Addendum — the independent Codex pass (rev 3.5) + +That recommended pass was run ([`reviews/codex-rev3.4.md`](reviews/codex-rev3.4.md)) +and it earned its keep: where this trace tested **expressibility**, Codex tested +**soundness** and found a real layer the internal passes missed — totality (÷0, +overflow, `NaN`), the static-bound hole (`range`/`pad` on un-`max`'d numerics — +this doc's `score` among them, now fixed), determinism (record-key order, effect +replay ordering, `const`-in-replay), plus self-contradictions (`defs` reading +`state`; effect `args` reading `{event}`; `menu` missing its `projection`; +`dataRef` overloaded with asset handles) and two security findings (free-colour +chrome spoofing; the taint claim). All are addressed in **rev 3.5** of +`lumens-spec.md` (§2.9 totality/bounds/determinism, §6.4 effect determinism, +§13.5 replay, §1.1 `assetRef` split, §3.1 anti-spoofing, §6 taint walk). The +examples in this doc are updated to the rev-3.5 grammar. The standing risk is +unchanged: **LLM emit-valid-LX reliability**, measurable only on a built L1 +interpreter. diff --git a/docs/protocol/reviews/codex-rev3.4.md b/docs/protocol/reviews/codex-rev3.4.md new file mode 100644 index 0000000..7130695 --- /dev/null +++ b/docs/protocol/reviews/codex-rev3.4.md @@ -0,0 +1,89 @@ +# Codex adversarial review — Lumens spec rev 3.4 + +> Independent adversarial pass (Codex, gpt-5.5, high reasoning) over +> [`lumens-spec.md`](../lumens-spec.md), [`lumen-walkthroughs.md`](../lumen-walkthroughs.md) +> and [`interactivity-concept.md`](../interactivity-concept.md) at rev 3.4 +> (`main` @ `9844b11`). Verbatim findings below; the triage and the resulting +> fixes are **rev 3.5** (see the rev-3.5 note in `lumens-spec.md`). +> +> **Triage summary.** Almost every finding is real. Codex tested *soundness* +> (is the execution model actually total / bounded / deterministic?) where the +> internal passes tested *expressibility* — and found genuine holes at the +> arithmetic / iteration / kernel / effect-replay layer, plus self-contradictions +> and two security findings (free-colour chrome spoofing; the taint claim). +> The one place we filter rather than adopt: the determinism **contract** is made +> normative now, but exact per-kernel algorithms + numeric defaults stay an L0 +> schema-spike deliverable (Codex's "specify everything now" overreaches the +> spec's own radical-restraint discipline). rev 3.5 addresses the rest. + +--- + +**Critical** + +- `docs/lumens-spec.md` §2.3/§2.4 + `docs/protocol/lumen-walkthroughs.md` A.2/D: static gas is not provable because `range`, `concat`, `flatten`, `split`, string ops, and kernel expression callbacks can allocate/iterate from runtime numeric values, while state `int`/`number` max is optional (`score` has no max). Fix: require finite min/max on all numeric state/const values used in size-producing ops and define per-op output caps in schema. + +- `docs/lumens-spec.md` §2.2/§2.3: LX is not total as specified; `/`, `mod`, `pow`, log/time scales, numeric overflow/NaN/Infinity, invalid string indexes/slices, and degenerate kernel inputs have no normative result. Fix: define exact total semantics for every partial operator, or make validation reject inputs that can reach invalid domains. + +- `docs/lumens-spec.md` §6.4 + §13.5 implied by §14 + `docs/protocol/lumen-walkthroughs.md` B.3/E: effect replay is underspecified; no deterministic effect id, ordering, result ordering, retry/idempotency key, or recorded replay envelope exists. Fix: assign monotonically ordered effect instance ids per transition evaluation and specify recorded result/error events replayed in that exact order. + +- `docs/lumens-spec.md` §6.4: multiple effects from one transition have undefined ordering, and `on:"transition"` plus `{when}` can double-fire for the same state change. Fix: define a total ordering over `effects[]`, and specify whether transition-triggered and predicate-triggered effects are mutually exclusive or both fire with distinct ids. + +- `docs/lumens-spec.md` §6.4: `debounceMs` “fire on settle” and `coalesceKey` “latest” depend on wall-clock scheduling and in-flight races, so replay is not deterministic. Fix: make debounce/coalesce operate over recorded logical event times/effect ids, and include the final emitted/suppressed decision in the replay trace. + +- `docs/lumens-spec.md` §2.6/§14: native kernels are normative but their signatures, gas schedule, tie-breaks, floating-point model, and degenerate-input results are deferred to a spike. Fix: move per-kernel deterministic algorithms, limits, and exact fallback/error results into the normative schema before claiming total/bounded/deterministic. + +- `docs/lumens-spec.md` §2.6: `layoutGraph(..., "force")`, `pathfind`, `sortBy`, `groupBy`, and quantile aggregation are not deterministic without seeded initialization, tie-break rules, float precision, stable ordering, and object-key ordering. Fix: mandate integer/fixed-point or canonical float behavior plus deterministic tie-breaks for every kernel. + +- `docs/lumens-spec.md` §2.6/§2.3: `groupBy → record`, `keys`, and `values` make JSON object key order observable without defining canonical record ordering. Fix: canonicalize record keys lexicographically or replace dynamic records with ordered list-of-pairs values. + +- `docs/lumens-spec.md` §1.2/§14: `const` is “not serialised” and “does not appear in undo/replay”, but transitions depend on it; replay after a const patch can diverge. Fix: include a content hash/version of the full `const` section in every trace/snapshot/replay frame. + +- `docs/lumens-spec.md` §6.4 + `docs/protocol/lumen-walkthroughs.md` C/E: effect `args` are specified as LX over post-transition state, but walkthrough effects read `{event:"item"}`/`{event:"dropTarget"}`. Fix: either allow effect args to read the triggering event explicitly, or require transitions to copy needed event fields into state. + +**High** + +- `docs/lumens-spec.md` §2.8 + `docs/protocol/lumen-walkthroughs.md` B.2/C: spec says `defs` cannot read `state`/`event`, but walkthrough defs `menuRow` and `effStatus` read `state`. Fix: make these walkthroughs pass `menu`/`override` as params, or loosen §2.8 and rework the purity claim. + +- `docs/lumens-spec.md` §2.8: acyclic `defs` is underspecified for static analysis; call graph extraction through dead branches, `match`, shadowed names, and invalid arity is not explicitly syntactic. Fix: define cycle detection as a syntactic walk over all reachable AST nodes regardless of branch feasibility, with reserved namespaces for params/defs/std-lib. + +- `docs/lumens-spec.md` §2.2/§2.5: multi-field `set` ordering is undefined for overlapping paths (`a` and `a.b`) and duplicate paths in JSON-source generation. Fix: reject duplicate/overlapping set paths and state that all RHS expressions evaluate against pre-transition state. + +- `docs/lumens-spec.md` §2.5: “transitions MUST return state” conflicts with “transition result = delta-merge with `set`/`setAt` paths applied”; arbitrary expressions returning full records versus delta nodes are not distinguished. Fix: define transition root type as `StateDelta` only, or allow full-state returns with an explicit discriminator. + +- `docs/lumens-spec.md` §4.1: event payload determinism is incomplete; overlapping inflated 44 pt hit areas, equal z-order scene nodes, drag start target, move/end sequencing, and pointer capture are undefined. Fix: specify hit-test order, tie-breaks, capture lifetime, and exact payloads for every drag phase. + +- `docs/lumens-spec.md` §4: `captureLongPress` is referenced but not in `EventBinding`, `TargetRef`, or `SceneNode`. Fix: add it to a concrete schema location or delete the exception. + +- `docs/lumens-spec.md` §1.1 + `docs/protocol/lumen-walkthroughs.md` B.0: walkthrough declares `"menu": {"type":"dataRef"}` without required `projection`; the reference Lumen is invalid under the spec. Fix: add the projection in B.0 or make projection optional with a defined opaque-handle type. + +- `docs/lumens-spec.md` §1.1/§3/§6.1 + `docs/protocol/lumen-walkthroughs.md` E: `dataRef` is overloaded as a projected structured state leaf and as an image/token handle (`tiles[].img`), but the schema only defines the projection form. Fix: split `dataProjectionRef` from `assetRef`/`DataRefHandle`. + +- `docs/lumens-spec.md` §1.1/§6.1: `loadData` timing and state interaction are undefined; it is unclear whether projection data counts against the 256 KB state cap, persists in undo, or arrives via patch/event. Fix: define projection lifecycle, empty defaults per type, cap accounting, invalidation, and replay behavior. + +- `docs/lumens-spec.md` §6/§6.3/§14: broker egress bounds and session-scoped consent budgets are listed as open tuning items, but they are security-critical to the default-deny claim. Fix: make minimum required rate/quota/max-in-flight/idempotency/consent-budget semantics normative, leaving only numeric defaults tunable. + +- `docs/lumens-spec.md` §6/§11: “state/DataRef-derived outbound requests are external-effect unless pre-approved” is not mechanically decidable as written. Fix: define taint rules for LX values flowing into capability args and require grant-time schemas for pre-approved request shapes. + +- `docs/lumens-spec.md` §7 + `docs/interactivity-concept.md` §9.1: `PortType` is never defined, and there is no LX node/event form for reading input ports or emitting output ports. Fix: define port types, state binding semantics, propagation order, and conflict handling. + +- `docs/lumens-spec.md` §7: `expose` says neighbours may read published fields by shared `DataRef` + stable IDs, but no addressing syntax, privacy boundary, or authorization rule is specified. Fix: require explicit reader declarations or wires, and define the exact lookup/read grammar. + +- `docs/lumens-spec.md` §3.1/§11: `colorMode:"free"` permits rendering arbitrary Omadia-looking UI inside the Lumen, enabling consent-modal/chrome spoofing despite the “chrome stays Lume” boundary. Fix: reserve host chrome/consent visual patterns and require an unforgeable Lumen boundary/attribution on external-effect prompts. + +**Medium** + +- `docs/lumens-spec.md` §2.3: `random()` and `now()` are mentioned but absent from the AST catalog and have no seed/time granularity semantics. Fix: add explicit nodes or std-lib signatures and define whether values are per event, per evaluation, or per call. + +- `docs/lumens-spec.md` §2.2: `{var:name, path:"f.g"}` allows paths into records/lists but only static dotted form; list indexing through `path` is ambiguous. Fix: restrict `path` to record fields only and require `at` for list access. + +- `docs/lumens-spec.md` §2.3/§2.6: kernel `keyExpr`/predicate callback scope is undefined. Fix: specify binder names, allowed captures, gas accounting, and whether callbacks may call other kernels/apply defs. + +- `docs/lumens-spec.md` §5: dirty-tracking “only dependent view branches” is impossible without a defined dependency-analysis model for arbitrary LX. Fix: either require whole-view reevaluation or define static dependency extraction and fallback behavior. + +- `docs/lumens-spec.md` §12/§13: `surface_capability_request/result` are named but no wire payload schema, correlation fields, or relation to `surface_action_result` is defined. Fix: add concrete event schemas with effect ids, capability name, args hash, result/error payload, and revision semantics. + +- `docs/lumens-spec.md` §13: `capabilityClasses?: CapabilityName[]` in client handshake conflates client support with Tier-2/user grants. Fix: rename to `brokeredCapabilitySupport` and keep grants exclusively in the Lumen manifest/grant state. + +- `docs/interactivity-concept.md` §3 vs `docs/lumens-spec.md` §2.2: concept still describes `map`/`filter`/`fold` as std-lib, while spec makes them AST binder nodes. Fix: update concept language to avoid implementers exposing higher-order std-lib functions. + +- `docs/interactivity-concept.md` §13 vs `docs/lumens-spec.md` §14: core parameters are called “research items, not unspecified holes” while the normative spec depends on them for safety. Fix: classify gas schedules, kernel limits, broker egress, and consent budgets as blocking normative deliverables.