doctrine: correct 5 overclaims in the zero-copy/memory-safety section - #46
Merged
Merged
Conversation
PR #45 landed with no real review (CodeRabbit posted only its auto- summary since it merged before the review cycle ran; Bugbot hit its usage limit twice and never ran) -- the only check it got was a single audit pass. Convened a 5+3 council (5 savants: citation-truth, abi-membrane-warden, zero-copy-warden, handle-lifecycle-auditor, java-surface-warden; 3 reviewers: overclaim-auditor, dilution-collapse-sentinel, firewall-warden) against the merged doctrine text. Five real overclaims found and fixed in CLAUDE.md: - "stale generation fails closed before dereference" didn't cover the cached-descriptor path (lgj_lane_describe/lgj_mask_describe hand Java a raw addr, read directly thereafter with only a Java closed-boolean guard, not the generation registry). Scoped to handle-mediated ops; the gap tracked as ISS-LGJ-EPOCH-UNCHECKED. - "an older library fails cleanly at the call, not at load" was false for ABI minors 2-4 (fail at Downcalls.<clinit>, a pre-existing tracked gap). Scoped to the minor-5+ lazy-holder pattern. - "checked_mul/checked_add throughout rowstore.rs and kernels.rs" overclaimed kernels.rs, which has zero occurrences (it bounds against an already-allocated slice's real length instead). Scoped and the real mechanism named. - "never segment.set(...)" was contradicted by the already-named Import exception (RowStore.importRows). Cross-referenced instead of left as an absolute the code visibly violates. - The materialization list was a closed enumeration missing two real, bounded call sites. Kept exhaustive (five items now) rather than converted to an unfalsifiable property claim -- the stricter reviewer verdict (dilution-collapse-sentinel BLOCKed the property-claim fix as a checkability regression) won over the looser one. Storno entry in EPIPHANIES.md corrects E-ZERO-COPY-MEMORY-SAFETY- AUDITED-CLEAN-1 without editing its prose. PR_ARC_INVENTORY.md also backfilled for PR #45 itself, which had no arc entry at all.
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Plus Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_21564cc7-7f54-4c94-b255-e7e38af87a60) |
AdaWorldAPI
marked this pull request as ready for review
August 28, 2026 08:18
This was referenced Aug 28, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Aug 28, 2026
CodeRabbit's Major on the epoch re-check design, verified real and absorbed as a council constraint rather than deferred: the epoch fetch and the cached LaneWindow/words read are two steps, so a cross-thread close (or same-slot reuse) between them defeats the check. Two honest frames recorded with it: the race is PRE-EXISTING (the closed-boolean guard carries the identical window — the re-check neither introduces nor widens it), and it is cross-thread-only (unreachable within one thread). The Phase-0 spec now requires the council to choose, as an explicit output: (i) serialize/lease covering both steps + a mandatory interleaving falsifier, or (ii) a written scoped contract with doctrine wording matching that scope — never (ii)'s semantics under (i)'s wording, the exact overclaim class PR #46 corrected. Savant #1's question set upgraded accordingly; W1.1 in the integration plan mirrors the constraint and scopes what 'resolved' means to the chosen arm.
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
2 participants
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.
Why
PR #45 merged with no real review — CodeRabbit posted only its auto-summary (merged before its review cycle ran), Bugbot hit its usage limit twice and never ran. The only check the doctrine text got was my own single-pass audit. Ran the
/5plus3council against it as the fallback review layer.What the council found (5 savants → consolidate → 3 reviewers → fix)
Panel: this repo's own
abi-membrane-warden/zero-copy-warden/handle-lifecycle-auditor/java-surface-wardencards + a citation-truth lens, thenoverclaim-auditor/dilution-collapse-sentinel/firewall-wardenon the consolidated draft.Five real overclaims in the merged
CLAUDE.mddoctrine, each fixed:lgj_lane_describe/lgj_mask_describehand Java a rawaddr, read directly thereafter guarded only by a Javaclosedboolean, not the generation registry). Scoped to handle-mediated ops; gap tracked asISS-LGJ-EPOCH-UNCHECKED.Downcalls.<clinit>, a pre-existing tracked gapDowncalls.java's own comment already names). Scoped to the minor-5+ lazy-holder pattern.kernels.rs(zero occurrences — it bounds against an already-allocated slice's real length instead). Scoped, real mechanism named.RowStore.importRows). Cross-referenced instead of left as a violated absolute.dilution-collapse-sentinelBLOCKed the property-claim fix as a checkability regression; stricter verdict won.Also caught: PR #45 itself had no
PR_ARC_INVENTORY.mdentry — backfilled here.What's in the diff
Doc-only, 0 lines of Rust/Java (confirmed by
git diff --stat):CLAUDE.md(5 bullets reworded),EPIPHANIES.md(storno entry correctingE-ZERO-COPY-MEMORY-SAFETY-AUDITED-CLEAN-1in place per append-only rule),ISSUES.md(ISS-LGJ-EPOCH-UNCHECKED),PR_ARC_INVENTORY.md(PR #45 backfill).Generated by Claude Code