fix(881): the replacement clause asserted an absolute I had not measured
Build ErsatzTV Image / CI toolchain image resolves (pull_request) Successful in 6s
Build ErsatzTV Image / Delimiter ban (release path) (pull_request) Successful in 20s
PR Gates / CI image pin matches docker/ci (pull_request) Successful in 17s
PR Gates / decisions lifecycle (pull_request) Successful in 23s
PR Gates / Docs update reminder (pull_request) Successful in 14s
PR Gates / Fix proofs (Proves trailers) (pull_request) Successful in 11s
Review verdict / Set review-verdict status (pull_request_target) Successful in 37s
review-verdict/h10 Review-verdict: MERGEABLE @ 0f8e73a (base: main)
Build ErsatzTV Image / Build & test (.NET) (pull_request) Successful in 8m47s
Build ErsatzTV Image / EF migration integrity (SQLite + MySql) (pull_request) Successful in 6m3s
Build ErsatzTV Image / Build & push image (amd64) (pull_request) Skipped
PR Gates / Script lint and tests (ruff + pytest) (pull_request) Successful in 19m41s
Build ErsatzTV Image / Functional E2E (curl + UI contracts) (pull_request) Successful in 5m47s
Build ErsatzTV Image / API docs in sync (OpenAPI + endpoint index) (pull_request) Successful in 8s
Build ErsatzTV Image / Formatting (changed .cs conform to .editorconfig) (pull_request) Successful in 6s
Build ErsatzTV Image / CI toolchain image resolves (pull_request) Successful in 6s
Build ErsatzTV Image / Delimiter ban (release path) (pull_request) Successful in 20s
PR Gates / CI image pin matches docker/ci (pull_request) Successful in 17s
PR Gates / decisions lifecycle (pull_request) Successful in 23s
PR Gates / Docs update reminder (pull_request) Successful in 14s
PR Gates / Fix proofs (Proves trailers) (pull_request) Successful in 11s
Review verdict / Set review-verdict status (pull_request_target) Successful in 37s
review-verdict/h10 Review-verdict: MERGEABLE @ 0f8e73a (base: main)
Build ErsatzTV Image / Build & test (.NET) (pull_request) Successful in 8m47s
Build ErsatzTV Image / EF migration integrity (SQLite + MySql) (pull_request) Successful in 6m3s
Build ErsatzTV Image / Build & push image (amd64) (pull_request) Skipped
PR Gates / Script lint and tests (ruff + pytest) (pull_request) Successful in 19m41s
Build ErsatzTV Image / Functional E2E (curl + UI contracts) (pull_request) Successful in 5m47s
Build ErsatzTV Image / API docs in sync (OpenAPI + endpoint index) (pull_request) Successful in 8s
Build ErsatzTV Image / Formatting (changed .cs conform to .editorconfig) (pull_request) Successful in 6s
The previous commit replaced "the order is load-bearing" with "and that is the whole of what the order buys". What was measured is narrower: with the relevance gate moved first, the three gates are each still witnessed refusing alone. That does not establish the order buys nothing else - the reset placement is a second candidate, unmeasured either way - so the absolute is gone from both sites and what stays is the cost reason, which is readable from the control flow. refs #881 Decisions-Edit: yes Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015QqCpYFsKgnAnx6jVwrKiV
This commit is contained in:
File diff suppressed because one or more lines are too long
@@ -430,13 +430,13 @@ def verify_claim(sandbox: Path, claim: Claim) -> Verdict:
|
||||
disarmed on its own and seen to matter; a single clause covering all three would be a guard
|
||||
nothing can witness failing.
|
||||
|
||||
THE RELEVANCE GATE RUNS LAST BECAUSE IT IS THE EXPENSIVE ONE, and that is the whole of what the
|
||||
order buys: it is the only one of the three that costs a second full run of the proof — under the
|
||||
reach mutation, with a sandbox reset in between — so an entry the status or the vacuity gate has
|
||||
already refused never pays for it. What keeps the three worth three is that each carries its own
|
||||
disarm proof, not the sequence they are written in. The sandbox is reset between the two runs
|
||||
because the first proof run can dirty the tree, and a second result that is a function of the
|
||||
first's is what `reset_sandbox` exists to prevent.
|
||||
THE RELEVANCE GATE RUNS LAST BECAUSE IT IS THE EXPENSIVE ONE: it is the only one of the three
|
||||
that costs a second full run of the proof — under the reach mutation, with a sandbox reset in
|
||||
between — so an entry the status or the vacuity gate has already refused never pays for it. What
|
||||
keeps the three worth three is that each carries its own disarm proof, rather than the position
|
||||
it sits in. The sandbox is reset between the two runs because the first proof run can dirty the
|
||||
tree, and a second result that is a function of the first's is what `reset_sandbox` exists to
|
||||
prevent.
|
||||
"""
|
||||
if claim.outcome == Claim.RED:
|
||||
return verify_mutation(
|
||||
|
||||
Reference in New Issue
Block a user