feat: classify accepted-blocking refusal eligibility - #105
Conversation
Keep future blocking execution fail-closed by admitting only typed refusal shapes whose lock risk can be meaningfully bounded. Distinguish one-relation index maintenance at the parse-only gate so broader forms remain ineligible.
Preserve refusal sites and causes on in-process verdicts so accepted-blocking eligibility sees the same typed proof produced by the gate. Verdicts decoded from JSON reconstruct the serialized fields but cannot recover refusal sites, so site-keyed eligibility deliberately fails closed.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
🤖 1/2 — the eligibility registry. The proof plumbing, RF-8, and the docs are in 2/2. Reviewed Eight caught, and the parse side is genuinely well pinned.
Deriving the single-relation fact from 1. The three parent causes that must stay ineligible are not pinned, and they are the dangerous half of the row
case verdict.CauseParentConcurrentIndexBuild, verdict.CauseParentIndexAdoption,
verdict.CauseParentNotValidForeignKey:
return false, trueChange That asymmetry is backwards for a registry whose thesis is that admitting a row is the consequential direction. Concretely, for
Extending 2. Both fail-closed defaults are unenforced, which is the property the registry is named for
Eligibility itself still fails closed either way, since The missing direction is one assertion: a synthetic reason and a synthetic site outside the vocabulary must come back 3.
|
|
🤖 2/2 — the refusal proof, RF-8, and RF-7. The registry itself is in 1/2. Carrying the narrowing on the 1. RF-8's fail-closed property covers one of the registry's two eligible rowsRF-8 ( I ran both eligible rows through a real encode/decode:
And because Whether that is acceptable depends on a decision this PR does not have to make — whether the step-2 executor ever takes eligibility from a decoded verdict, or only from one it produced in-process. But the entry should say which, because the next reader will key that decision off RF-8 and the current wording reads as a blanket guarantee. Two candidate shapes:
The current text is the one shape that reads as a guarantee while being a description of two different behaviors. Worth noting this also interacts with the registry's own framing at 2. The proof fast-path bypasses the validation
|
aparajon
left a comment
There was a problem hiding this comment.
🤖 Approving on 81daca74. Fourteen mutations, eight caught — the parse side (len(GetObjects()), the REINDEX object type, the default: IndexTargetOther arm) is well pinned, and driving the table through real ParseOne input is what makes it checkable end to end. Six survived, detailed in 1/2 and 2/2. The two I would act on: the three unsupported-partitioned-parent causes that must stay ineligible are asserted nowhere, so flipping them to eligible ships green; and Refusal()'s proof fast-path now skips the validation its own doc comment still promises, which is reachable in one call via the new WithSite/WithCause and is the point where RF-7's "NewRefusal is the only way to build a Refusal" was enforced. Also worth deciding now rather than in step 2: RF-8's fail-closed guarantee holds for the site-keyed eligible row but not the cause-keyed one, which survives JSON decoding and is reconstructible from hand-written JSON.
This stamp was left by Claude Code (claude-opus-5).
…both sides
Refusal() returned a non-zero in-process proof without the RF-7 validation
the decoded path applies, so a Refusal built outside the constructors (for
example Refusal{}.WithSite(...)) or a per-class constructor with an unknown
reason reached callers unchecked. It now re-validates the proof through
NewRefusal and errors when the verdict's exported class, reason, owner, or
cause no longer match the proof WithRefusal stamped them from, so the
refusal a consumer reads is the one an eligibility decision consumes.
The eligibility registry tests now pin the eligible set from both sides:
walking every key the completeness harness derives, exactly the
single-relation DROP INDEX and REINDEX gate keys and the blocking parent
index build are eligible. New tests prove the default arms fail closed and
undecided for an unknown reason, site, or cause, and that each eligible row
requires its class. pkg/statement pins IndexTargets() against the declared
IndexTarget constants the way Kinds() is pinned.
RF-8 and the passthrough design now state the shipped boundary precisely:
the site-keyed row fails closed after JSON decoding, the cause-keyed row is
decidable from the wire fields, and eligibility is consumed only from the
proof of the verdict the same front-door invocation produced.
🤖 Generated with Amp (Claude Opus 4.6)
|
🤖 Adversarial review response — created by Kiran's code review agent (Amp, Claude Opus 4.6) — block/pg-sprite pull/105, follow-up commit Verdict: all five findings fixed in one follow-up commit; the RF-8 wording decision and the proof-divergence check are the two calls to veto.
Decisions to veto
Verification
Source: block/pg-sprite#105, review comments 5629181195 and 5629181647 and review 5174802719 at head |
Add a closed typed registry for accepted-blocking eligibility while preserving the current refusal-only behavior.
Why
Future bounded blocking execution needs a narrow, reviewable admission decision that cannot depend on SQL or rendered explanation text.
What
plan.PartitionRefusal, so both front doors carry the same typed cause (constants pinned topreflight's by test).Before / after