The setup exclusion landed for the model arm only, because only a model
pick stamped a source. A seeded run returned setup's action through the
same entry with no marker, so its denominator still counted the login
while the model arm's did not, and the two are compared.
serializeAction names setup and seeded on the wire, so both arms are
counted by one rule. An already-recorded trace names nothing and keeps
exactly the count it was reported with; unattributed_actions counts those
steps so the old denominator cannot pass as the new one. TraceVersion is
deliberately unbumped: oracle-reduction refuses a differing version, and
a bump would make all 169 recorded runs unreplayable.
Setup runs through the picker with the rng under both policies, so a generator
there is legitimate and must keep working. Interleaving enumeration and setup
catches the flag leaking out of the model's walk.
Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX
Candidates returns an error now. The refusal is thrown at the draw and wrapped
with the source of the leaf that made it, since generate() cannot know which
leaf it is inside. Only that marked refusal is fatal: this walk calls every
leaf on every step, so promoting the rest would kill model runs the seeded arm
survives.
Authored actions on a disabled target are no longer dropped from the model's
candidate list. The seeded picker executes whatever the leaf authored, and a
control the application forgot to re-enable is exactly where boundary defects
live, so a policy that cannot attempt it cannot find them.
Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX
Candidates takes the label source as an argument rather than storing it, which
is what keeps the asymmetry structural: the seeded picker selects by index and
never calls Candidates, so the mode cannot reach it. That asymmetry is
load-bearing, because it makes the two seeded cells of the factorial a
manipulation check with identical draw streams.
The identifier ladder deliberately has no text rung. A fallback that reached
for text would silently turn one arm back into the other.
Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX
* fix(ltl): give every thunk a construction identity
Two distinct unnamed predicates both described as "Thunk(...)", so obligation
collapse merged their residuals and could drop a live violation. Identity is
assigned at construction and the fields are unexported, so a thunk cannot be
built without one.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(ltl): reduce a thrown-predicate residual instead of panicking
The verifier substitutes an ErrorFormula for the residual of a property whose
predicate threw, and that residual is fed back in on the next step. reduce had
no case for it, so the run crashed. It re-reports the same failure now.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(ltl): make a bounded always the dual of a bounded eventually
G<=n(f) and not F<=n(not f) disagreed on traces where the inner was still
pending when the window closed, so nnf's negation normal form was not semantics
preserving. Both sides now range over the observations at which their inner can
definitely resolve: the eventually keeps a pending inner as a disjunct, and the
always discharges vacuously at window close.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(ltl): arm a one-shot root once per run
A root that carries its own horizon is one obligation for the whole run, not one
per observation. Re-instantiating a top-level eventually monitored G F<=n(p)
instead of F<=n(p) and left one live obligation per step behind; a bounded
always restarted its window every step and never closed.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(verifier): stop wrapping a top-level eventually in always
`eventually(p).within(300, "seconds")` as a property meant "within 300 seconds
of every step", which spawned an obligation per step with its own resolved
deadline. A 553-step run carried 553 of them and serialized a 75 KB residual.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(ltl): serialize the resolved deadline of a bounded window
Two obligations spawned at different steps from one duration-bounded formula
differ only in the deadline the evaluator resolved for them, so they serialized
identically and the trace erased a distinction the evaluator makes. The authored
window stays in amount/unit; the resolved deadline rides alongside.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(verifier): split a witness's origin step from its detection step
A deferred obligation spans two steps: the one that armed it and the one whose
reduction failed. They were conflated under one index, so the extractor snapshot
(which is the detecting step's state) was reported against the origin step.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(runner): record a witness's detection step in the trace
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* feat(replay-ui): show the step a violation was detected at
The witness evidence is the detecting step's state, so say which step that is
and let a reader jump to it.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(verifier): record the extractor state the predicates actually read
On the web path extractor bodies are evaluated in V8 and injected here, but only
the goja value was replaced. The trace diff and the violation witness therefore
described a state no property ever saw.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* refactor(spec): one candidate producer over one target-eligibility rule
Both hosts routed verbs themselves and both policies enumerated their own
actions, and all four drifted. Web sent `swipes` to scrollable containers only,
so swipe-to-dismiss on a list row was reachable on native and unreachable on
web; the model policy folded gestures its own way and could not reach what the
seeded picker drew.
A host now reports facts about every element and never decides which verb may
act on it: targets.ts acceptsTarget owns that for both. pick.ts builtinCandidates
is the single enumeration, and the model policy reads it through
__sanderlingEnumerateBuiltin__ instead of reimplementing it in Go.
Gesture verbs change with it: scrolls stay vertical over scrollable containers,
swipes go free-form in all four directions from any element with real bounds.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(runner): name a builtin scroll by its drag origin
A builtin gesture carries endpoints and no selector, so every scroll rendered as
"Scroll down " in the prompt's recent-action memory and two scrollable regions
were indistinguishable.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(chrome): clear storage over cdp instead of scripting an opaque origin
Launch runs while the tab is still on about:blank, whose opaque origin denies
storage access, so localStorage.clear() threw SecurityError and every web run
died at launch. Storage.clearDataForOrigin needs no navigation. The exception
helper lands here because "Uncaught" is what hid this for so long.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(chrome): enable the swiftshader webgl fallback
Headless Chrome runs with --disable-gpu, and without this flag it refuses the
software WebGL backend: getContext returns null, so a canvas-rendered app paints
nothing and every screenshot is identical black.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* fix(web): resolve testTag through data-testid or id
Compose Multiplatform emits its testTag into the element id, which the native
table already accepts via the resource-id alias. The two web selector tables
were the only place that rejected it.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* test(spec): type-check the spec api as part of make test
The fake runtime in api.test.ts did not return a chainable handle from extract,
so the file had not type-checked since named() was added. Wiring the check into
make test stops it drifting again.
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
* docs(manual): one-shot eventually and the gesture verbs
Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
pj