The reverse direction for §7.2 and §8.2, completing §6–§8 both ways - #24
Merged
Conversation
…ing and cover the rest of §6–§8 The previous commit had katie verify a §6.3 proof built here. This extends the same mechanism to §7.2 and §8.2, so every algorithm implemented in the last several rounds is now checked in both directions rather than one. The three are genuinely different readers of the same structure, which is the point of doing all of them. §6.3 walks the frontier; §7.2 binary-searches from the root and reads the rightmost timestamp before anything else; §8.2 descends to a map entry's parent to learn what is distinguished and then re-proves a version further up. A proof built for one is not a proof for another, and katie's refusals confirm it. Two things came out of getting the positive cases to pass, both about ordering rather than content. §12.3.1's view update consumes the frontier's timestamps before any algorithm starts asking, so §7.1's rightmost-timestamp-first rule applies only to what the search adds — putting it first overall made the sequence non-monotonic from katie's side. And the closing call matters: using katie's DataProvider.Finish rather than its handle's runs the whole sequence a client performs, so it in-fills prefix roots for entries with a timestamp and no proof, hashes every inspected leaf, and evaluates the log tree inclusion proof against them before refusing leftovers. That makes the reverse direction check three things at once — the element ordering, §12.3's exact counts, and whether the log tree proof this side built roots the leaves it names. Six of the nine new cases are deliberately wrong, since those are the ones with something to prove. The last is the one worth naming: a monitoring ladder taken from a log entry that never held the version, which is exactly the rollback §8.2 exists to catch, and katie refuses it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The previous PR had katie verify a §6.3 proof built here. This extends the same mechanism to §7.2 and §8.2, so every algorithm from the last several rounds is now checked in both directions.
Doing all three matters because they're genuinely different readers of the same structure:
A proof built for one isn't a proof for another, and katie's refusals confirm it.
Two ordering lessons from getting the positives to pass
§12.3.1's view update goes first. It consumes the frontier's timestamps before any algorithm starts asking — so §7.1's rightmost-timestamp-first rule applies only to what the search adds. Putting it first overall made the sequence non-monotonic from katie's side.
The closing call matters. Using katie's
DataProvider.Finishrather than its handle's runs the whole sequence a client performs: in-fill prefix roots for entries with a timestamp and no proof, hash every inspected leaf, evaluate the log tree inclusion proof against them, then refuse leftovers. So the reverse direction now checks three things at once — element ordering, §12.3's exact counts, and whether the log tree proof this side built actually roots the leaves it names.Six of nine new cases are deliberately wrong
A timestamp too many; a prefix proof too few; proofs reordered; timestamps descending; a fixed-version proof a timestamp short; and — the one worth naming — a monitoring ladder taken from a log entry that never held the version, which is exactly the rollback §8.2 exists to catch. katie refuses every one, and accepts the three honest proofs.
218 reverse-direction artifacts: 112 accepted, 106 rejected, 0 disagreements. 6706 checks / 789 cases forward.
cargo fmt,clippy -D warnings, tests green.🤖 Generated with Claude Code