Append gate round 2: base-anchored prefix, av2 assertion addressing, byte-append#89
Merged
Merged
Conversation
…byte-append Address ledger review findings 3, 6, and 13 in the thesis-facts append gate. Finding 3 (HIGH): the immutable-prefix manifest is candidate-controlled, so a PR could grow prefixLineCount over its own append and have every post-cutover binding skipped. Under --base-ref the gate now loads the base manifest and requires prefixLineCount/prefixSha256/lineSha256s to be unchanged, and it uses the BASE prefix count as the post-cutover binding boundary so a candidate-controlled count can never move it. On push (no base ref) the candidate manifest is trusted for the full-file invariants only, which base-anchoring cannot cover without a witness. Finding 6 (HIGH): replace the incomplete av1 content address with the av2 projection (byte-identical to the Brier writer's assertion_version): it binds the complete measure concept mapping, exact source file/digest, row/cell lineage, and the archived response digest. check_rows now reserves the effective id (explicit or recomputed) of EVERY row, closing legacy synthetic-id reuse and A->B->A restoration. Add effective_current_rows() and validate the aggregate-fact journal as its supersede-aware current view so a legitimate correction no longer fails as a duplicate semantic key. Finding 13 (LOW): _lines dropped blank lines, so a blank line inserted into the frozen JSONL normalized away. reject_non_append_bytes rejects any blank/whitespace-only line in the covered region and a non-single trailing newline. Ports Sol's adversarial counterexamples into tests/test_thesis_append_adversarial.py: the finding 3/6/13 cases are now real asserts; the remaining strict-xfails document out-of-scope boundaries (provenance-format validation, no-base-ref full-file mode, per-commit history walking). Co-Authored-By: Claude Fable 5 <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
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.
Follow-up to #86, closing the gaps a verification review (Sol, gpt-5.6) found in that gate. Merge-order note: MaxGhenis/brier already writes
av2assertion ids; the gate merged in #86 recomputesav1, so the next resolver append proposal will be rejected until this lands. Fails closed, but it blocks the daily resolve loop.Finding 3 (HIGH) — the manifest could grandfather an unbound append
check_prefixtrusted the candidate tree'sprefixLineCount, and post-cutover binding checks keyed off that candidate-controlled count. A normal PR could append a structurally-valid but completely unbound row (noretrievedAt/ledgerRepoSha/responseArchive/assertionVersion/projection) and extendimmutable_prefix.jsonover it — every binding requirement was skipped and the gate exited 0.Under
--base-refthe gate now loads the base manifest and requiresprefixLineCount/prefixSha256/lineSha256sunchanged, and applies post-cutover requirements to every row after the base prefix count. Growing the frozen prefix is an explicit reviewed migration, never an automated append.Finding 6 (HIGH) —
av1did not bind assertion meaningav1projected onlymeasure.{concept,unit}and four source fields, so a row could change its concept mapping, authority, source file, source digest, or row/cell lineage and keep the same id; different archived response bytes also collided. Replaced withav2, byte-identical to the Brier writer'sassertion_version: it binds the full measure concept mapping, exact source file + digest, row/cell lineage, and the archived response digest (Brier now archives before computing the version so the bytes are in identity).check_rowsnow reserves the effective id — explicit or recomputed — of every row, closing legacy synthetic-id reuse and A→B→A restoration of a superseded value.effective_current_rows()gives the supersede-aware current view, and the required aggregate-fact test validates that view: previously a legitimate correction passedcheck_rowsand then failed CI as a duplicate semantic key, so the documented correction path could not actually merge.Finding 13 (LOW) — not byte-append-only
_linesdiscarded blank lines, so a blank line inserted into the frozen JSONL normalized away. Blank/whitespace-only lines in the covered region and a non-single trailing newline are now rejected.Verification
uv run pytest tests/test_thesis_append_adversarial.py tests/test_policyengine_ledger.py -q→ 31 passed, 5 xfailed. The xfails are deliberate specifications of out-of-scope boundaries (no-base-ref full-file mode, per-commit history walking, provenance-format validation), not unrun tests.python3 scripts/check_thesis_facts_append.pyand--base-ref origin/codex/thesis-ledger-factsboth pass on the real 128-row file.uv run ruff checkclean on touched files.av2:8e26886cd5d2b0c5…for the same row.Pairs with MaxGhenis/brier@4e65e0c (av2 writer, contract-binding derivation) and #87.
🤖 Generated with Claude Code