Record L1 Cut 3's landing, verdicts and findings

Cut 3 landed at dfb3c52..2bf8164. Soul's first pass confirms that
boundary sessions now resume after unrelated commits, that a resumed
session keeps its recorded lens across a weight change, that admission is
the same under every lens, and that the catalog and session identity are
unchanged. It also observed all three illegal transitions (lens, text,
ancestry), and a stale adopted draft is still refused by the kernel.

Going to a test-only fix batch:
- the illegal-transition test is flaky, failing roughly one run in eight;
- nothing pins that the call-site draw reads the command id;
- nothing pins that a session resumes with its stored instruction text,
  which was the whole point of the Q7 ruling.

Recorded: stored text is not tied to the recorded lens (inside Q7's
accepted cost); a route cost change re-rolls a boundary session's lens and
orphans its row; the seed lane orphans rows the same way deficits do
(L1.f13). The ledger text no longer doubles "recorded".

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
Meta Vens 2026-09-16 16:42:12 +02:00
commit ef6400884a

View file

@ -1205,12 +1205,58 @@ not repo artifacts.
code's still opens (the (a) trade, stated).
- P3.7 Deficit rediscovery after an unrelated commit is Cut 4's promise
(P4.6), not this cut's; no test in this cut is ignored.
- **Landed:**
- **Verdicts:**
- **Landed:** `dfb3c52` (c1.s1.f2, the draw's divisor guarded directly),
`4334dd7` (c2.s2.f1, lens sets compared by effective weight), `18b1098`
(Cut 3 proper; carries two unfulfilled-expectation warnings that the next
commit removes), `4457fde` (c1.s1.f3, markers removed), `2bf8164`
(non-adoption across world or jurisdiction). `session_command_id` now takes
`(world_id, jurisdiction, &answer_digest)`, so the lens is absent by
signature; the derivation bytes are unchanged.
- **Verdicts:** Soul pass 1 against `2bf8164`.
| Promise | Verdict | Evidence | Mutations |
|---|---|---|---|
| | | | |
| P3.1 | HOLDS for identity; UNPROVEN that the call-site draw reads the command id (c3.s1.f2) | The UUID pin equals Cut 0's `56dbcdb2…`; `session_command_id` takes no session | M3.6a, M3.6b kill; Soul S3 (draw with `CommandId::new()`) survives |
| P3.2 | HOLDS; its illegal-transition pin is flaky (c3.s1.f1) | At `1a402e1` the boundary test failed as Superseded; it now commits through a store reopen with the refusal intact. The weights test keeps the recorded lens across reopen. Lens, text and ancestry transitions are each observed accepted under M3.4 and refused without it | M3.1, M3.2, M3.4; Soul S1 kills |
| P3.3 | HOLDS | Eight-lens admission equals `base-mismatches.json`; prompts byte-equal | M3.3 |
| P3.4 | HOLDS | Catalog signatures and digest rerun, equal to Cut 0; no `patch.rs` or sidecar diff | signature proof |
| P3.5 | HOLDS | v15 row refused at open; the same payload under v16 opens | none |
| P3.6 | HOLDS | Disagreeing stored text and invocation refused; agreeing arbitrary text opens. Nothing pins that resume uses the stored text (c3.s1.f3) | M3.5 kills; Soul S5 survives committed tests |
| P3.7 | HOLDS | Deficit orphan reproduced as base behaviour; no ignores added | none |
| c1.s1.f2 | HOLDS | Divisor guarded (`lens.rs:195-203`); no panic with `draws()` weakened | MF2.1 |
| c2.s2.f1 | HOLDS | `weighs_the_same_as` over `Lens::ALL`; padded twins refused in both directions through the mailbox | MF21.1 |
| c1.s1.f3 | HOLDS | Markers gone; forced-rebuild warnings identical to Cut 2 | none |
- **Soul findings, pass 1:**
- **c3.s1.f1 (introduced, medium, fix):** flaky pin.
`controllers.rs:10221` rewrites `session.lens = Lens::Numen`, but
`refused_checkpoint()` draws under uniform weights with a random world id.
About one run in eight the recorded lens is already Numen, and
`assert_ne!(next, checkpoint)` (`:10230`) fails. Soul observed 2 failures
in 9 runs.
- **c3.s1.f2 (introduced, low, fix):** every lens-observing test uses a
single-lens world, so the draw is forced. A call site that draws with an
unrelated command id (S3) survives. Only `lens.rs` unit tests pin the
recipe.
- **c3.s1.f3 (introduced, low, fix; the untested Q7 ruling):** mutation S5,
which rebuilds the resumed text from `session.lens.instructions()` (`:476`),
survives every committed test. No test proves that a session resumes
with its stored text after the lens's text changes in code, which was the
purpose of L1-Q7 (a). Recorded cost within Q7: nothing ties a row's stored
text to its recorded lens. A row with arbitrary text or another lens's
text, invocation prepared to match, opens and drives inference with that
text. Only the local store file can write it (`pub(super)` fields).
- **c3.s1.f4 (pre-existing, low-medium, recorded):** see L1.f13 (seed lane).
- **c3.s1.f5 (pre-existing orphaning, lens re-roll introduced, low,
recorded):** the boundary's scope preimage includes the route record
(`lib.rs:3892-3899`). A caller with patch authority who alters a lane's
cost moves the digest while the boundary survives. The next session
re-rolls its lens and the in-flight row is orphaned. Containment,
occupant or incident changes remove the boundary outright
(`lib.rs:3878-3884`). A fresh session after a real structural change is
arguably correct; the orphan row adds to orphan hygiene.
- **c3.s1.f6 (info):** dropping `answer_digest` from `same_answer` (S2) is an
equivalent mutant, because the id already carries the digest.
## Cut 4. Concurrent sessions over a per-sweep claim set, under the elaboration ceiling
@ -1516,14 +1562,14 @@ not repo artifacts.
| 0 | — | — | scratch captures only | scratch captures only, no repo change |
| 1 | 0 | `lens.rs` ~150 + tests ~130; `lib.rs` 2 lines + test helper ~6 | 0 deps; 0 targets | `lens.rs` +372 (217 code, 155 tests; the tool tables are one name per line under rustfmt); `lib.rs` +7; `elaboration.rs` 1 line changed; 0 deps; 0 targets |
| 2 | ~6 (doc lines replaced, the v2 denial case) | library: state field, command, effect, two reducer arms, resolve param, mismatch variant, snapshot field, replay check ~90; 19 literal sites × 1 line; tests ~220; Dungeon: payload field, policy fn, Eve control and binding, three schema strings, harness ~40; tests ~60; docs ~8 | 0 deps; `consumer.v4` → `v5`; `world_create.v3` → `v4` | 12 files, +825 / −40: production ~130 across `lib.rs`, `patch.rs`, `journal.rs`, `mailbox.rs`, `action.rs`, `runtime.rs`, `eve.rs` plus 20 construction sites; tests ~650 (refusal matrix, direct `apply_effect` half, forged rows, state rows, replay). 0 deps; the two schema bumps as estimated |
| 3 | ~4 (the constant as integrity reference, the whole-session supersession equality) | session fields, draw and text in `select_answer`, adoption rule, request param ~60; tests ~200; docs ~3 | `controller_work.v15` → `v16` | |
| 3 | ~4 (the constant as integrity reference, the whole-session supersession equality) | session fields, draw and text in `select_answer`, adoption rule, request param ~60; tests ~200; docs ~3 | `controller_work.v15` → `v16` | 6 files, +1071 / −113: production about +100 / −60 (`elaboration.rs` session fields, `same_answer`, adoption, draw in `select_answer`, request parameter, id signature, the constant deleted; `lens.rs` the constant moved in, the divisor guard, `weighs_the_same_as`, markers removed; `lib.rs` one call; `controllers.rs` two constants); tests about +890 (real-store tests, fixture generalization, two added tests); docs 1 line. `controller_work.v15` → `v16` as estimated |
| 4 | ~35 (sequential sweep, `Inactive`, doc lines) | `sweep` + `demand_entries` with rediscovery ~110; trait method + three store impls ~45; second pool and its config ~25; tests ~360; docs ~14 | public `sweep` signature gains a `Semaphore`; `ControllerWorkStore` gains one required method; one new env variable | |
| 5 | ~14 | ~25 | 0 | |
Net for L1: about +1,300 lines, of which about two thirds are tests, no new
dependency, no new crate, no new binary, four schema strings replaced, one
environment variable added, one required method on the store trait. The growth buys the capabilities the target
names (lenses, world-owned weights and their owner command, a recorded
names (lenses, world-owned weights and their owner command, a
replayable draw recorded on the session, concurrent sessions under a
ceiling that cannot starve simulation, an explicit weights payload) and
retires one liability: a sweep whose only protection against a second
@ -1557,6 +1603,15 @@ session on one answer was that nobody wrote one.
approvals are effectively the owner approving their own world. If
approvals are bound then, bind them to the world's structure, excluding
lens weights. **Authority:** operator. **Ruled:** 2026-09-16.
- **L1.f13 (pre-existing, low-medium, operator):** the seed lane has the
deficit-shaped rediscovery defect. `seed_command_id`
(`elaboration.rs:1381-1386`) hashes ancestry, so an owner Draft commit after
a refused seed round moves the key. The next seed session misses the row,
repeats the inference without the refusal it earned, and orphans the old
row (Soul's probe: rows = 2, no refusal carried). The whole-session
comparison at `:1650` can only be reached for same-ancestry rows and is
effectively inert. L1-Q9 (A) fixes the elaborator lane only; the seed lane
is outside L1.
- **L1.f1 (pre-existing, medium, operator-triaged, not blocking L1):** a
sweep error whose `requires_quarantine()` is true reaches