Update Safe owner list page with reduced hypotheses and functional correctness#19
Merged
Update Safe owner list page with reduced hypotheses and functional correctness#19
Conversation
…s, reduced hypotheses - Replace false antisymmetry invariant with provable uniquePredecessor in SafeGuarantee component - Add isOwner functional correctness column to proof status table (15 theorems) - Update hypotheses section: SafeOwnerInvariant bundle (3 fields), derived properties (noSelfLoops, freshInList, acyclic) noted as internalized rather than assumed - Simplify hOwnerInList hypothesis (hOldNePrev was derived away) - Update "What these invariants cover" disclosure with 4 property families Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 724c3ab. Configure here.
The proof status table said "inListReachable" but the disclosure section above describes four property families: ownerListInvariant, uniquePredecessor, acyclic, and isOwner correctness. Rename the column to "uniquePredecessor" so the table and text are consistent. Fixes Bugbot review thread on PR #19. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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.
Summary
reachable(a,b) ∧ reachable(b,a) → a = b) with the provableuniquePredecessorproperty in the SafeGuarantee componentSafeOwnerInvariantis now just 3 fields (ownerListInvariant, uniquePredecessor, zeroInert); properties likenoSelfLoops,freshInList, andacyclicare derived inside the proofs rather than assumedhOwnerInListhypothesis (the oldhOldNePrevwas derived away)These changes correspond to the proof improvements in verity-benchmark PR #18.
Test plan
🤖 Generated with Claude Code
Note
Low Risk
Low risk: changes are limited to research-page copy and UI tables, with no runtime/business logic changes beyond rendering updated invariant text.
Overview
Updates the Safe owner-list research page to replace the previously stated (and false) reachability antisymmetry invariant with the provable
uniquePredecessorproperty, and to describe the invariants as four property families.Expands the proof-status section to reflect 15 proven theorems (from 12) by adding
isOwnerfunctional correctness coverage, and revises the hypotheses narrative to a smaller bundledSafeOwnerInvariant(3 fields) with several properties now described as derived rather than assumed.Reviewed by Cursor Bugbot for commit 61ecd7d. Bugbot is set up for automated code reviews on this repo. Configure here.