Skip to content

Accepted-receipt continuity wall: a vanished acceptance receipt with no explicit revocation witness must refuse - #7771

Merged
briansrls merged 2 commits into
mainfrom
session/crisp-ferret-54
Aug 4, 2026
Merged

briansrls merged 2 commits into
mainfrom
session/crisp-ferret-54

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 4, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Closes the accepted-state continuity fail-open called out after PR #7739: a roadmap node could silently return to the active frontier when its RoadmapAcceptanceReceipt row was deleted, lost in conflict resolution, or omitted during regeneration — with no refusal and no way to distinguish "revoked" from "missing."

This PR adds:

  • RoadmapAcceptanceReceiptRevocation — explicit, typed revocation witness (node, criteria digest, reason, who/when)
  • A monotone baseline ledger (roadmap_acceptance_receipt_baseline_nodes) — closed subject universe of every node ever accepted; grows only when a new acceptance lands, never shrinks
  • acceptance_receipt_continuity_holds / acceptance_receipt_continuity_verdict — each baseline node must still carry a current receipt or a revocation; vanished-without-revocation refuses with AcceptanceReceiptContinuityRefusedVanishedWithoutRevocation

Validation residue (construction ceiling documented in acceptance_receipt_continuity_wall_note): append-only receipt history would make silent deletion unwritable; this slice keeps the editable receipt list and enforces continuity via witnesses.

Test plan

  • claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/roadmap_authority_test.dag --functions witness_acceptance_receipt_continuity_holds_on_live_authority,witness_vanished_receipt_without_revocation_refuses,witness_explicit_revocation_authorizes_vanished_receipt --claim-run — 3/3 PASS
  • CI floor (gunbc ci) on PR head

Worker attestation

  • Title describes the change
  • PR body summarises what and why
  • Tests run (see above)
  • No secrets / credentials / large binaries

gunbc-ci-auto-heal and others added 2 commits August 4, 2026 02:31
Use a named refusal variant instead of a single-variant coproduct the
compiler rejected; remove the live witness population-count pin per DESIGN
section 5 and document the validation-residue ceiling in the wall note.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 4, 2026 02:43
@briansrls
briansrls merged commit 772d92d into main Aug 4, 2026
5 checks passed
@briansrls
briansrls deleted the session/crisp-ferret-54 branch August 4, 2026 05:21
@gunbai-bot

gunbai-bot Bot commented Aug 4, 2026

Copy link
Copy Markdown
Contributor Author

Before merging: the approval on this PR is against a superseded head, and one gap remains

The approving review (artifact 47918) examined 7959866d. At that head this branch still carried roadmap_acceptance_receipt_baseline_nodes() — a second hand-maintained list beside the receipts — and the wall could be bypassed by deleting a receipt and its baseline row together: every remaining baseline node still had a receipt, every remaining receipt was still in the baseline, and no vanished node survived in either population to refuse. The review's "cross-checks that keep the monotone baseline and live receipts aligned" describes exactly that mechanism. It approved the version with the hole.

The current head bdb9117a has since fixed it, and the fix is good. Verified by content, not by the note:

  • roadmap_acceptance_receipt_baseline_nodes — 0 refs at bdb9117a, 3 refs at 7959866d. The dual list is gone.
  • roadmap_acceptance_event_history is the single authority; roadmap_acceptance_receipts is now a projection through project_live_acceptance_receipts.
  • replay_acceptance_event refuses correctly: revocation requires the exact prior receipt to be live (receipt_present_exact, so a wrong digest refuses), duplicate revocation refuses, and re-recording a live node refuses.

That is construction over validation, and it dissolves the delete-both hole structurally rather than detecting it.

The remaining gap

acceptance_history_extends_prior is the base/head prefix law that makes deletion refuse. The live consumer short-circuits it — dag/gunbc/roadmap_authority.dag:

prior_history: [],

and extends_prior returns true immediately when count(prior) == 0. Every non-empty prior in the tree is in a test (roadmap_receipt_continuity_acceptance_test, roadmap_authority_test). So the prefix law is proven on fixtures and not executed on the production path.

That leaves the live defence as the sealed pin alone — roadmap_acceptance_history_sealed_event_count() (16) and roadmap_acceptance_history_sealed_chain_digest(). It does refuse a bare deletion. But both are hand-editable values in the same authority as the history, so delete one event + decrement the count + recompute the digest passes. That is the original defect's shape — two hand-maintained values that must be edited together — moved from (receipts, baseline) to (history, seal). Narrower, since recomputing a chain digest is harder than deleting a row, but the same class.

It is weakened further by the conjunct immediately below:

&& count(roadmap_acceptance_event_history()) == roadmap_acceptance_history_sealed_event_count()

which forces the seal to be updated on every ordinary acceptance. Resealing is therefore routine rather than exceptional, and a delete+reseal is not distinguishable in review from an append+reseal. A bypass that looks exactly like normal operation is the one review cannot catch.

roadmap_acceptance_history_note currently reads as though prior events cannot be deleted. Today that holds only against an editor who does not also update the seal.

Suggested disposition

Not a request to weaken or remove the seal — keep it as defence in depth. Either wire prior_history from a real base observation so the live consumer executes the prefix law, or state explicitly that the base/head observation substrate is not reachable yet and name it as this node's next-rung trigger, so prior_history: [] stops reading as if the check runs.

The authoring session (crisp-ferret-54) was archived and its work item closed, so this will not be picked up by its author. I am dispatching a follow-on for the wiring; flagging here so this is not merged on the strength of a review that predates the recut.

— sent from loyal-ram-550

gunbai-bot Bot pushed a commit that referenced this pull request Aug 4, 2026
Review 47973 added the authority note to std.occurrence_binding_candidates
but the stage0 projection was not regenerated; regen_verify_gate_passes failed
on std_occurrence_binding_candidates.rs. Also includes merge of origin/main
(#7773 roadmap rows, #7771 accepted-receipt continuity).

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Aug 4, 2026

Copy link
Copy Markdown
Contributor Author

Closing as superseded by #7787, which is a strict superset of this branch.

Verified by content, not by claim: dag/gunbc/roadmap_model.dag on #7787 contains all of this branch's event-history work, plus two improvements — take_acceptance_events moved from recursion to a fold (DESIGN §6 bare-minimum cost), and the AcceptanceNodeReopensActiveFrontier declaration fixed.

What this branch got right and #7787 carries forward: roadmap_acceptance_event_history as the single authority with roadmap_acceptance_receipts reduced to a projection, replacing the earlier roadmap_acceptance_receipt_baseline_nodes list. That was the real fix — the dual-list design was bypassable by deleting a receipt and its baseline row together, and the event history dissolves that structurally rather than detecting it.

What #7787 adds: prior_history wired to a real git.Inspect.MergeBase + git.Core.Show base observation instead of the stubbed [] that short-circuited acceptance_history_extends_prior on the production path, a typed AcceptanceHistoryIntegrityRefusedPriorHistoryObservation so a failed git observation refuses rather than fabricating a prior, and the closing contract function promoted to test fn so the bound validation actually executes.

Note for anyone reading the approval on this PR: it was made against 7959866d, the head that still carried the deletable baseline list. It approved the design that has since been replaced and did not see the recut. My detailed finding is in the comment above.

No work is lost. The authoring session was archived before #7787 opened; the successor branch picked this one up rather than restarting.

— sent from loyal-ram-550

@gunbai-bot

gunbai-bot Bot commented Aug 4, 2026

Copy link
Copy Markdown
Contributor Author

Correction to my previous comment, and a finding that matters more than the correction.

I wrote that above as if closing this PR. It was already merged (772d92d18b, 2026-08-04T05:21:47Z) — I was working from a stale view. Disregard the "closing as superseded" framing.

The substantive part is worse than a wording slip: what merged here is the pre-recut version. At the merge commit itself, dag/gunbc/roadmap_authority.dag has roadmap_acceptance_receipt_baseline_nodes present (3 refs) and roadmap_acceptance_event_history absent (0 refs). The recut at bdb9117a — event history as the single authority, receipts reduced to a projection — is not an ancestor of main. It was pushed to this branch but never landed.

So the design currently on main is the one with the documented bypass: deleting an acceptance receipt and its baseline row together still passes, because every remaining baseline node still has a receipt, every remaining receipt is still in the baseline, and no vanished node survives in either population to refuse. That is the fail-open this node exists to close, and it is live in the tree right now.

Two things follow:

  1. The approval on this PR was against 7959866d — the same pre-recut head that merged. It did not see the recut, and its stated basis ("cross-checks that keep the monotone baseline and live receipts aligned") describes exactly the bypassable mechanism. Recorded so the approval is not read as validating a design it never examined.

  2. Repair live acceptance-receipt deletion bypass on main (772d92d18b) #7787 is not a follow-up, it is the repair. It carries the recut (roadmap_acceptance_receipt_baseline_nodes → 0 refs), plus prior_history wired to a real merge-base observation, a typed refusal when that observation fails, and the closing contract promoted to test fn so the bound validation actually executes. It is CLEAN and out of draft.

roadmap-receipt-continuity should not be treated as delivered by this merge. Even after #7787 it lands a declared ceiling — the prefix law still does not execute when the authority file actually changes — but #7787 at minimum removes the live bypass, which this merge did not.

— sent from loyal-ram-550

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