Skip to content

Append gate round 2: base-anchored prefix, av2 assertion addressing, byte-append#89

Merged
MaxGhenis merged 1 commit into
codex/thesis-ledger-factsfrom
thesis-facts-append-gate-2
Jul 10, 2026
Merged

Append gate round 2: base-anchored prefix, av2 assertion addressing, byte-append#89
MaxGhenis merged 1 commit into
codex/thesis-ledger-factsfrom
thesis-facts-append-gate-2

Conversation

@MaxGhenis

Copy link
Copy Markdown
Contributor

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 av2 assertion ids; the gate merged in #86 recomputes av1, 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_prefix trusted the candidate tree's prefixLineCount, and post-cutover binding checks keyed off that candidate-controlled count. A normal PR could append a structurally-valid but completely unbound row (no retrievedAt/ledgerRepoSha/responseArchive/assertionVersion/projection) and extend immutable_prefix.json over it — every binding requirement was skipped and the gate exited 0.

Under --base-ref the gate now loads the base manifest and requires prefixLineCount/prefixSha256/lineSha256s unchanged, 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) — av1 did not bind assertion meaning

av1 projected only measure.{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 with av2, byte-identical to the Brier writer's assertion_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_rows now 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 passed check_rows and then failed CI as a duplicate semantic key, so the documented correction path could not actually merge.

Finding 13 (LOW) — not byte-append-only

_lines discarded 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 -q31 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.py and --base-ref origin/codex/thesis-ledger-facts both pass on the real 128-row file.
  • uv run ruff check clean on touched files.
  • av2 id equality with Brier's writer verified directly: both produce av2:8e26886cd5d2b0c5… for the same row.

Pairs with MaxGhenis/brier@4e65e0c (av2 writer, contract-binding derivation) and #87.

🤖 Generated with Claude Code

…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>
@MaxGhenis MaxGhenis merged commit 47ca684 into codex/thesis-ledger-facts Jul 10, 2026
3 checks passed
@MaxGhenis MaxGhenis deleted the thesis-facts-append-gate-2 branch July 10, 2026 15:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant