§8.3's first algorithm: owner initialization

[OR13]

§8.3's first algorithm is unlike every other operation here in direction. A searcher descends toward a version; contact monitoring follows its versions up and to the right as new nodes are built over them; an auditor moves forward an entry at a time. An owner claiming a label is accepting a history it never saw — so step 1's list is the starting position followed by the entries on its direct path and to its left, ending just before the first expired one.

Two things follow from that direction, both unique to this algorithm:

• The ladders are full. Step 5 says "without omitting redundant lookups", where §6.3 and §7.2 say the opposite — a walk going backwards has no earlier entry for a later ladder to lean on.
• A greatest version per entry, and it must descend. Step 2 requires each to be no greater than the one before: a version count only grows, so a list running backwards through the log that rises means the log is lying about one of the two entries. Nothing else in the protocol has that check, and it's the only thing between an owner and a fabricated history.

Recovering which version each ladder step belongs to meant reproducing step 3's set — version zero plus every version a search ladder for any of the greatest versions would look up, ascending per §13.3 — because the wire carries the steps in that order and names no versions. The count is checked against the response before anything is verified, so a disagreement about the set is a refusal rather than a misreading.

Result

The recorded owner-init case replays and consumes its proof exactly. The version ordering, the expired-start refusal and the too-many-versions case are covered by Rust tests, since katie's recorded response is an honest one and none of them can be provoked from it.

6697 checks / 787 cases / 18 suites, 0 disagreements. cargo fmt, clippy -D warnings, 172 kt-tree tests green; line coverage 97.7%.

🤖 Generated with Claude Code