fabi/Sylpheed
1
0
Fork 0
Code Issues 9 Pull Requests Actions Packages Projects Releases Wiki Activity

port: check the walk as well as the contract, and a defect I nearly filed off a debug pin

Browse Source 
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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7FiFFFwbvG2uxdcEh8HyF
This commit is contained in:
Sylpheed port agent
2026-08-30 21:17:59 +00:00
parent ad80938efc
commit f7fee7a77f
3 changed files with 149 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
docs/port/BLOCKED.md
View File

@@ -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

70
docs/port/DECISIONS.md
View File

@@ -9,7 +9,7 @@ dies, which is what this file is for.
<!-- INDEX: generated by tools/port/index-decisions -- do not hand-edit -->
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)
<!-- /INDEX -->
## 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.**

83
tools/port/contract-check
View File

@@ -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.")