From f7fee7a77f5e2d09ee90981751a2199eff9b60c4 Mon Sep 17 00:00:00 2001 From: Sylpheed port agent Date: Sun, 30 Aug 2026 21:17:59 +0000 Subject: [PATCH] port: check the walk as well as the contract, and a defect I nearly filed off a debug pin docs/game/navigation.md is a second document unreachable from main, and authored/flow.json is its executable form -- nothing in the port fails when a label drifts from it. Three more checks in contract-check, anchored on the walk's own text: the five main-menu labels in order, EXTRAS' three items, the cursor wrap. Ten checks now, ten known negatives, all passing. The manual audit behind them found nothing else: initial focus is already kind:authored citing Q5's instability, left_right is an explicit no-op, auto_repeat is measured, unexported destinations are marked blocked with reasons. Refutation target: the walk's claim that the ring is the ONLY thing moving on the settled menu. Cannot be tested against the game from here, but can be tested against my renderer, which is the direction that matters. Five renders across a full ring cycle: 1428 of 921600 pixels vary, 0.155 %, one 46x44 cluster beside the focused item. The port animates one ring, not five -- worth checking, since all five ptbtn01f..05f declare the same 120-unit cycle and a renderer running all of them would look identical until you diffed frames. Then I nearly filed a serious P5 defect against myself: sweeping --leaf-time with the ring pinned moves 10.4 % of the frame, full-screen. It is not a defect. That pin addresses the build-in -- ptloop01 runs t=0..600, ptloop02 t=0..720 -- and at settle both park off-screen at x=1521 and x=-839, with loop_leaf_on_screens scoped to the title alone. The general form: a pin that can address states the screen never occupies will manufacture defects on demand, which inverts what the three pins are for. The +0x08 ask came back answered and is not consumable. ui_layout::loop_length_units is public at b5df02a and byte-for-byte what screen.rs holds, so the deletion is one line -- but Cargo.toml pins a tag, no tag carries that commit, and swapping a deliberate pin for a bare rev on an unmerged branch is not a move to make alone. Asked for a tag; keeping the guarded local read. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01N7FiFFFwbvG2uxdcEh8HyF --- docs/port/BLOCKED.md | 2 +- docs/port/DECISIONS.md | 70 ++++++++++++++++++++++++++++++++- tools/port/contract-check | 83 +++++++++++++++++++++++++++++++++++++-- 3 files changed, 149 insertions(+), 6 deletions(-) diff --git a/docs/port/BLOCKED.md b/docs/port/BLOCKED.md index 5ba04aea..9012d04a 100644 --- a/docs/port/BLOCKED.md +++ b/docs/port/BLOCKED.md @@ -157,7 +157,7 @@ HANDOFF. | Milestone | Needs | HANDOFF | State | |---|---|---|---| -| P3/P5 โ€” the record loop length | **expose `+0x08` in `sylpheed_formats`' public API** | `27938aa` | ๐Ÿ”ด **the port cannot obey the instruction with anything published.** HANDOFF says *"stop shipping 105"*, which presumes the port can read the loop length. It is decoded in `examples/record_loop_length.rs`, asserted in `tests/ui_record_loop_length_disc.rs`, written up in `docs/re/structures/ui-record-loop-length.md` โ€” and exposed in the crate's API **on no ref at all** (checked against every ref touching `crates/sylpheed-formats/src/`). `screen.rs` reads the four bytes itself, guarded on the `RATC` magic, because `parse_build` publishes each record's `(offset, size)`. That works and it is **the port holding a format detail it should not own**: one `pub` field on the record type takes it back where it belongs, and the exporter's helper is documented to be deleted the day it appears. Not blocking โ€” the value is shipping. | +| ~~P3/P5 โ€” the record loop length~~ **now: a tag** | ~~expose `+0x08` in the API~~ **cut a `formats-pin-*` tag carrying `b5df02a`** | `27938aa` | โœ… **ANSWERED IN CODE 2026-08-30, and still not consumable.** `ui_layout::loop_length_units` is public at `b5df02a` and is byte-for-byte what `screen.rs` holds โ€” same guard, same offset, same BE read โ€” so the deletion is one line. โš ๏ธ But `Cargo.toml` pins a **tag**, and no tag carries that commit; moving to a bare `rev` on an unmerged branch swaps a deliberate pin for an incidental one, and this pin is recorded load-bearing. Keeping the guarded local read until a tag exists. Original text: ๐Ÿ”ด **the port could not obey the instruction with anything published.** HANDOFF says *"stop shipping 105"*, which presumes the port can read the loop length. It is decoded in `examples/record_loop_length.rs`, asserted in `tests/ui_record_loop_length_disc.rs`, written up in `docs/re/structures/ui-record-loop-length.md` โ€” and exposed in the crate's API **on no ref at all** (checked against every ref touching `crates/sylpheed-formats/src/`). `screen.rs` reads the four bytes itself, guarded on the `RATC` magic, because `parse_build` publishes each record's `(offset, size)`. That works and it is **the port holding a format detail it should not own**: one `pub` field on the record type takes it back where it belongs, and the exporter's helper is documented to be deleted the day it appears. Not blocking โ€” the value is shipping. | | P3/P5 โ€” the other focus records | **do `ptbtn01fโ€ฆ05f` and `ptbtn11fโ€ฆ13f` animate while focused?** | `27938aa` | โ” **open, and deliberately not inferred.** The export shows all eleven declaring the same 120-unit cycle, and `looping_focus_records` names only the plate. A declared cycle is not evidence that the game runs it โ€” `authored/timing.json` already argues the pulse rule matches 82 of 212 elements and would make the copyright notice pulse. Whether a focused menu button glows is **behavioural**: outside my role, asking. | ## Answered since this file was last written โ€” no longer blocking diff --git a/docs/port/DECISIONS.md b/docs/port/DECISIONS.md index 2cc3239c..ba1d1fc2 100644 --- a/docs/port/DECISIONS.md +++ b/docs/port/DECISIONS.md @@ -9,7 +9,7 @@ dies, which is what this file is for. -237 sections. Search this before re-deriving anything. +239 sections. Search this before re-deriving anything. * [P0 โ€” the exporter, 2026-08-28](#p0--the-exporter-2026-08-28) * [P1 โ€” Godot draws the screen, 2026-08-28](#p1--godot-draws-the-screen-2026-08-28) @@ -248,6 +248,8 @@ dies, which is what this file is for. * [A refutation attempt on `+0x08 is the loop length` โ€” it survives, and the port adopts it](#a-refutation-attempt-on-0x08-is-the-loop-length--it-survives-and-the-port-adopts-it) * [The contract is checked now, not read โ€” `tools/port/contract-check`](#the-contract-is-checked-now-not-read--toolsportcontract-check) * [A refutation attempt on the fade numbers โ€” it survives, from a third reader](#a-refutation-attempt-on-the-fade-numbers--it-survives-from-a-third-reader) +* [The walk is checked too, and "only the ring moves" tested against my own renderer](#the-walk-is-checked-too-and-only-the-ring-moves-tested-against-my-own-renderer) +* [The `+0x08` ask came back answered โ€” and is not consumable yet](#the-0x08-ask-came-back-answered--and-is-not-consumable-yet) ## P0 โ€” the exporter, 2026-08-28 @@ -12415,3 +12417,69 @@ record-layout fix โ€” which is precisely what their helper had *not* had. caused by my recomputation, and the export now re-derives 190 and 145 from the keyframe times a third time. A retraction confirmed by the party that provoked it is worth less than one confirmed by a third reading; this is the third reading. + +## The walk is checked too, and "only the ring moves" tested against my own renderer + +`docs/game/navigation.md` โ€” the screen-by-screen walk written from the committed +oracle frames โ€” is a **second document unreachable from `main`**, and +`authored/flow.json` is its executable form. Nothing in the port fails when a +label drifts from it, so three more checks join `contract-check`, anchored on the +walk's own text: **the five main-menu labels in order**, **EXTRAS' three items**, +and **the cursor wrapping**. All three agree; all three fail their known +negative. Ten checks now, ten controls. + +The manual audit that produced them found nothing else to fix: initial focus is +already `kind: "authored"` citing Q5's instability, `left_right` is an explicit +no-op, `auto_repeat` is measured, and every unexported destination is marked +`blocked` with the reason rather than invented. + +### The refutation target: *"it is the only thing moving on this screen"* + +The walk says the focus ring turns continuously and is **the only** thing moving +on the settled main menu โ€” labels, bracket and footer at temporal std **exactly +0.000 over 20 s**. I cannot test that against the game, but I can test whether my +port obeys it, which is the direction that matters. Five renders across a full +ring cycle (`--loop-phase` 0โ€ฆ96, `--leaf-time` pinned): + +| | | +|---|---| +| pixels varying by > 2 | **1 428 of 921 600 โ€” 0.155 %** | +| bounding box | 46 ร— 44 at x 498โ€“543, y 158โ€“201 | +| distinct clusters | **1** | + +One region, beside the focused item. โœ… **The port animates one ring, not five** โ€” +worth checking, because the export shows all five `ptbtn01fโ€ฆ05f` declaring the +same 120-unit cycle and a renderer that ran them all would look identical to one +that ran the right one until you diffed frames. + +### ๐Ÿ”ด And I nearly filed a defect against myself off a debug pin + +Sweeping the **other** free clock โ€” `--leaf-time` 0โ€ฆ8 s with the ring pinned โ€” +moved **10.4 % of the frame, full-screen bounding box**. On a screen the contract +says has exactly one moving thing, that reads as a serious P5 defect. + +It is not one. `--leaf-time` is a **debugging pin**, and 0โ€ฆ8 s is 0โ€ฆ480 units, +which lands *inside the build-in*: `ptloop01`'s sweep runs t=0โ†’600 and `ptloop02` +t=0โ†’720. At settle they are parked at **x = 1521** and **x = โˆ’839**, both +off-screen on a 1280-wide frame, and `loop_leaf_on_screens` scopes the replay to +`title` alone. So the settled menu moves exactly the ring, and the 10.4 % was me +driving an animation the settled screen has already finished. + +๐Ÿ“Œ **The general form is worth more than the incident: a pin that can address +states the screen never occupies will manufacture defects on demand.** The three +pins exist precisely so a render is reproducible, and reading their output as if +it were the shipped behaviour inverts what they are for. Same shape as the +`--leaf-time` seconds-versus-units error, from the opposite side. + +## The `+0x08` ask came back answered โ€” and is not consumable yet + +The Decoder exposed `ui_layout::loop_length_units` at **`b5df02a`**, and it is +byte-for-byte the logic `screen.rs` holds: same `RATC` guard, same `0x08`, same +big-endian read. So the deletion my doc comment promises is a one-line switch. + +โš ๏ธ **Not taken this iteration, and not for a reason about the code.** +`crates/sylpheed-export/Cargo.toml` pins `tag = "formats-pin-2026-08-30"` and +**there is no tag carrying `b5df02a`**. Moving to a bare `rev` on an unmerged +branch would replace a deliberate pin with an incidental one โ€” and `BLOCKED.md` +already records this pin as load-bearing. **Asked for a tag; keeping the local +read, which is guarded and controlled, until one exists.** diff --git a/tools/port/contract-check b/tools/port/contract-check index b30b640c..ff6e7693 100755 --- a/tools/port/contract-check +++ b/tools/port/contract-check @@ -175,25 +175,99 @@ CONTROLS = [ ] + +def fn_nav_perturbed(fn, old, new): + """Run a walk-anchored check against a perturbed copy of the walk. + + `nav()` reads from git, so the perturbation is injected by swapping the + function out rather than by editing a file -- nothing on disk is touched. + """ + global nav + real = nav + nav = lambda: (real()[0].replace(old, new, 1), real()[1]) + try: + fn(None) + finally: + nav = real + + def control(h): global FAIL import io, contextlib ok = True print(" known negatives -- every check must notice a perturbed contract:\n") - for fn, old, new in CONTROLS: - if old not in h: + for fn, old, new in CONTROLS + [(f, o, n) for f, o, n in NAV_CONTROLS]: + src = h if (fn, old, new) in CONTROLS else nav()[0] + if old not in src: print(f" {fn.__name__:<22} ๐Ÿ”ด the control's own anchor is gone") ok = False continue before, FAIL = FAIL, 0 with contextlib.redirect_stdout(io.StringIO()): - fn(h.replace(old, new, 1)) + if src is h: + fn(h.replace(old, new, 1)) + else: + fn_nav_perturbed(fn, old, new) noticed, FAIL = FAIL > 0, before print(f" {fn.__name__:<22} {'โœ… fails as it must' if noticed else '๐Ÿ”ด PASSES A WRONG CONTRACT -- it checks nothing'}") ok = ok and noticed return ok +def nav(): + """The player's-eye walk, from the newest ref that carries it. + + A second unreachable document: `docs/game/navigation.md` was filled in from + the committed oracle frames and, like HANDOFF, is not on `main`. The port's + `authored/flow.json` is the executable form of that walk, so the two must not + drift -- and the drift would be invisible, because nothing in the port fails + when a label is wrong. + """ + sha = git("log", "--all", "--format=%h", "--", "docs/game/navigation.md").split()[0] + return git("show", f"{sha}:docs/game/navigation.md"), sha + + +def flow_buttons(screen): + d = jload("authored/flow.json") or {} + b = ((d.get("screens") or {}).get(screen) or {}).get("buttons") or {} + return [v.get("label") for _, v in sorted(b.items())] + + +def check_menu_labels(_h): + """The five main-menu labels, in order, off the walk's own table.""" + n, sha = nav() + rows = re.findall(r"^\| [1-5] \| \*\*([A-Z ]+)\*\* \|", n, re.M) + want = rows or None + report(f"main menu labels ({sha})", want, flow_buttons("main_menu"), + want is not None and want == flow_buttons("main_menu")) + + +def check_extras_labels(_h): + """EXTRAS' three items, written as prose rather than a table.""" + n, _ = nav() + m = re.search(r"Three items: `([A-Z ]+)` ยท `([A-Z ]+)` ยท `([A-Z ]+)`", n) + want = [m.group(i) for i in (1, 2, 3)] if m else None + report("extras labels", want, flow_buttons("extras"), + want is not None and want == flow_buttons("extras")) + + +def check_wrap(_h): + """The cursor wraps, and it is a MENU rule -- the walk says so in two places.""" + n, _ = nav() + want = True if re.search(r"one item, and it \*\*wraps\*\* at both ends", n) else None + got = ((jload("authored/flow.json") or {}).get("navigation") or {}).get("wrap") + report("cursor wraps", want, got, want is not None and want == got) + + +# The walk's controls perturb `navigation.md` instead of HANDOFF, so they are +# applied to a different document and kept separate rather than folded in. +NAV_CONTROLS = [ + (check_menu_labels, "| 1 | **NEW GAME**", "| 1 | **NEW GAMES**"), + (check_extras_labels, "`MISSION SELECT` ยท `MOVIE THEATER`", "`MISSION SELECTS` ยท `MOVIE THEATER`"), + (check_wrap, "one item, and it **wraps** at both ends", "one item, and it stops at both ends"), +] + + def main(): if not os.path.exists("export/manifest.json"): sys.exit("no export/ -- run the exporter first; this check reads what is shipped") @@ -203,7 +277,8 @@ def main(): return 0 if control(h) else 1 for fn in (check_fade_quads, check_fade_out, check_plate_period, check_bgm_window, check_black_hold, check_menu_bank, - check_splash_dwell): + check_splash_dwell, check_menu_labels, check_extras_labels, + check_wrap): fn(h) print() print(" A passing run means the port agrees with the contract ON THESE VALUES.")