Repository navigation
Retip #38: refuse a non-zero residual on an OUTSIDE cell (controls 33 and 34) - #104
Closed
d6g8k5htny-coder wants to merge 2 commits into
Closed
d6g8k5htny-coder wants to merge 2 commits into
d6g8k5htny-coder wants to merge 2 commits into
Conversation
…cards
`Ledger.reject` validated the kind, the reason and the boundary-area bound and
never the residual. `total()` skips every OUTSIDE cell with `continue` before
it reaches the branch that sums one. So a caller could reject a cell OUTSIDE
while handing over a non-zero residual: the number was stored on the record,
dropped from every total, and the run still reported itself sound.
Reproduced on a two-cell unit cover, one cell accepted at exactly 1 and the
other rejected OUTSIDE carrying [10**6, 10**6]:
total.certified True
total.covers_region True
total.caveats ()
certified_enclosure Interval(1, 1)
A certified enclosure of [1, 1] while holding a discarded possible
contribution of a million. THIS WAS A LIVE PATH. Nothing had to be mutated to
produce those four lines, which is what separates it from the recorded
surviving mutants in the same README.
`reject` now refuses a non-zero residual on an OUTSIDE cell. The two
statements cannot both be true: OUTSIDE asserts the cell is proved disjoint
from the region and therefore contributes exactly zero, so a non-zero possible
contribution denies the very rejection the call is recording. Whichever of the
two is wrong, the caller must say which rather than have the ledger keep both
and silently believe one.
The guard is scoped so it closes the hole without removing the feature:
`None` and an exact [0, 0] are still accepted on OUTSIDE, and EXCLUDED and
UNRESOLVED_BOUNDARY -- the two kinds whose residuals ARE summed -- still take
a non-zero one.
Controls 33 and 34 in `tests/test_cover.py` (retip of 1796d28, whose controls
were 41 and 42; the tip suite ended at 32, so 33 and 34 were free). Control 33
asserts the refusal and was confirmed to FAIL against a copy of the package
under the scratchpad with the guard deleted, never by editing the library.
Control 34 rebuilds the pre-guard record by hand and asserts the old behaviour,
so the defect stays demonstrable after the fix instead of surviving only as
prose. Source-branch tests that already occupied numbers 33-40 were not part
of 1796d28 and were not taken.
`research/cover/README.md` records it with the four lines above, under a
heading naming the date it was found.
This establishes no mathematics and closes nothing. `D3-LEMMA-RN-UNIF` Piece 1
and Piece 2 remain OPEN, every integrand here is still a labelled reference,
and no cell of the program's actual cover is certified. A ledger that refuses
to discard a number it was handed is not a cover certificate.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Cz7WZybv8znP64SpPj6sWY
Co-authored-by: Dylan Roy <d6g8k5htny@privaterelay.appleid.com>
… review The guard is unchanged; its justification was wrong for a case it refuses. I wrote that a non-zero residual on an OUTSIDE cell and the rejection itself "cannot both be true". That holds for the witness that motivated the guard -- [10**6, 10**6] excludes zero, so it does deny "proved disjoint". It is false for a non-singleton enclosure that CONTAINS zero, such as [-eps, eps]: that is a conservative statement of a zero contribution, not a denial of OUTSIDE. Reported by the ChatGPT agent reviewing PR #38, who also reproduced the original witness independently at hardening 6f0f061 -- stored [1000000, 1000000], returned certified [1,1]. The contract stays exactly None or exactly [0, 0], now resting on the reason that is actually true of every value it refuses: total() DISCARDS an OUTSIDE cell's residual before it reaches the summing branch, so a residual of non-zero WIDTH loses the uncertainty it expresses, silently, even when it contains zero. Requiring exact zero makes the discard lossless. A caller who means "zero, conservatively" writes [0, 0]; a caller who means "possibly non-zero" is describing a cell that is not OUTSIDE. Changed in the three places that carried the bad argument -- the guard comment in research/cover/ledger.py, the docstring of control 41, and the README section -- each naming the review rather than quietly rewording. The error message now separates the two cases and gives the remedy for each: reject it UNRESOLVED_BOUNDARY or EXCLUDED if it can contribute, or say [0, 0] and carry the uncertainty on a cell whose residual survives. Also recorded from the same review, and NOT acted on here: research/cover/ ledger.py is pinned twice by research/rn/candidates/inner_wedge_20260920_v1 .json at 37974 bytes / 58ebe18f…, and hardening's copy matches that pin exactly. This edit must not be transported there. The migration branch's copy was already 37269 bytes against that pin, so this branch does not change the binding's status either way -- the hazard is entirely in the transport. The source-compatible integration on that side is an additive checked-total boundary, which catches strictly more than an input guard can. 10/10 checkers pass; 1,927 passed, 1 skipped. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Cz7WZybv8znP64SpPj6sWY
cursor
Bot
force-pushed
the
cursor/retip-38-outside-residual-guard-077464ef
branch
from
September 25, 2026 17:30
4e3cd79 to
ec3b426
Compare
Owner
Author
|
Closing this parked branch as BLOCKED/NONMERGEABLE by its own documented owner ruling. The head edits pinned |
This was referenced Sep 25, 2026
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.
Parked. Do not merge.
Owner ruling: do not modify
research/cover/ledger.py, and do not re-pin it. It is a source identity ofresearch/rn/candidates/inner_wedge_20260920_v1.json(37974 bytes /58ebe18fbc3fc44e1ba9566e19494fbf906b8579e5dca96b414fb0f309d866c9) and must stay byte-identical to hardening @388a22caff13c449f0e3264b0aff314d456d6659.This head does not obey that ruling. It still contains the earlier retip, which edits
research/cover/ledger.py(worktree 40293 bytes /7971c74c91ec44674fc5c0708dbd38115b3337d328e866663824813a6d1765c6). No follow-up was pushed. A wrapper cannot close the hole without that edit, and pushing this tree breaks the pin.Why the guard cannot move off
ledger.pyThe live path is
Ledger.reject. It validates kind, reason, andboundary_area_bound, then assignsrec.residual. There is no hook, callback, strategy, or subclass injection point onrejector ontotal.totalthen skips everyOUTSIDEcell withcontinuebefore the summing branch, so a stored non-zero residual is dropped and the run can still reportcertified=True.research/cover/driver.pycallsledger.rejectdirectly. ForOUTSIDEit already passes exact[0, 0]. A new module that wrapsrejectis not on that call, and it is not on any other call ofLedger.reject. Importing a wrapper does not changeLedger.rejectunless something replaces the method. That replacement is not a hookledger.pyoffers; installing it on the real call path means editingledger.py, or editing another always-imported file (__init__.pyordriver.py) to monkeypatch the class. Either way the check is no longer an opt-in wrapper around an untouched ledger.The publication-boundary form of this check is already on the tip, in
research/cover/audit.pychecked_total. It refuses anOUTSIDEresidual that is notNoneor[0, 0](refusing to discard a stored interval) and does not changeledger.py.tests/test_cover_audit.py::test_outside_noncanonical_residual_refused_before_publicationcovers that, including the note that mutating the record bypasses any entry-only guard.Ledger.total()itself still certifies the discarded residual. That is the hole, and it is insidereject/total.What this head still is
Controls 33 and 34, plus the in-method guard, from draft #38. Superseded source: #38. This PR does not close #38. Draft. Base is
chatgpt/drive-github-hardening-20260919, notmain.Base:
388a22caff13c449f0e3264b0aff314d456d6659. Head:ec3b4260b07ea31fb7ebc7c6c7bd554d58622d81.