Open
Conversation
New case study page for the formally verified inListReachable invariant of the Safe OwnerManager linked list, proven using Verity and Lean 4. 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}
| </div> | ||
| </div> | ||
| ) | ||
| } |
There was a problem hiding this comment.
SafeGuarantee duplicates Guarantee toggle logic and structure
Low Severity
SafeGuarantee is a near-complete copy of Guarantee — the state management (useState, useRef, useEffect with 5-second timer), handleToggle handler, toggle button with identical SVG icon, and the grid-based opacity-swap layout are all line-for-line identical. Only the inner content and one label string ("Switch to formal" vs "Switch to math") differ. A shared wrapper component accepting the formal/English content, toggle label, and Lean link as props would eliminate ~60 lines of duplication and make future case study pages trivial to add.
Reviewed by Cursor Bugbot for commit 934c77e. Configure here.
Reflects verity-benchmark PR #18 which extends the Safe case from addOwner-only to all four ownership-mutating functions (setupOwners, addOwner, removeOwner, swapOwner) and three invariant families (inListReachable, ownerListInvariant, acyclicity). Key changes: - Title broadened to "Safe Owner List Invariants" - SafeGuarantee now shows the ownerListInvariant biconditional - "What these invariants cover" lists all three invariant families - "How this was proven" describes all four function models - Added proof status table (1 proven, 11 open benchmark tasks) - Hypotheses updated: added hPrevLink (GS205), hClean (setupOwners), reclassified hAcyclic and hFreshInList as provable properties - Links updated for new Specs.lean line numbers and OpenProofs.lean Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
changed the title
Display inListReachable, ownerListInvariant, and acyclic as a stacked list with English/formal toggle. Each invariant label links to its definition in Specs.lean. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
There are 2 total unresolved issues (including 1 from previous review).
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 25a1c88. Configure here.
- Extract shared Hypothesis component from duplicated code in both research pages (bugbot fix) - Move safe-owner-reachability to top of research list as newest entry (bugbot fix) - Update page content: all 4 functions modeled (setupOwners, addOwner, removeOwner, swapOwner), 6/6 benchmark proofs complete - Update SafeGuarantee to show ownerListInvariant (biconditional) instead of just inListReachable - Add proof status table, stronglyAcyclic hypothesis, and updated hypothesis descriptions (hOwnerInList, hOldNePrev, hStrongAcyclic) - Update page title and metadata to "Safe Owner List Invariants" Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The INVARIANTS-based multi-row layout uses plain <a> tags for invariant labels, so ExternalLinkIcon is no longer referenced. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Reflects the new stronglyAcyclic definition (antisymmetry of reachability) added in verity-benchmark PR #18, which captures Certora's reach_invariant axiom and is required by removeOwner and swapOwner proofs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The table was showing only 6 benchmark tasks and incorrectly listing removeOwner/swapOwner acyclicity and setupOwners ownerListInvariant as open. Cross-referencing Proofs.lean (0 sorry) shows 9 theorems are proven. Only 3 ownerListInvariant preservation theorems (addOwner, removeOwner, swapOwner) remain open. Switched to a compact function x invariant grid matching the actual proof state. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- SafeGuarantee: English summary wording, formal-only math (no Lean names), centered sizing tuned vs Lido hero - Page: disclosure lists four invariants; prose and links (OwnerManager.sol, Verity Contract.lean); remove em dashes; How this was proven intro ties Verity model to Solidity source Made-with: Cursor
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
/research/safe-owner-reachabilityfor the Safe OwnerManager linked list invariantssetupOwners,addOwner,removeOwner,swapOwnerinListReachable(forward reachability),ownerListInvariant(combined biconditional), andacyclic(no cycles)SafeGuaranteecomponent with English/formal notation toggle showing theownerListInvariantbiconditionaldata/research.jsgetSortedResearch()for consistent date-sorted research listsHypothesiscomponent.github/workflows/ci.yml)The page covers:
acyclic,freshInList)Aligned with verity-benchmark PR #18 which extends the Safe case to model all four functions and adds the new invariant families.
Test plan
next buildsucceeds with the new page/research/safe-owner-reachabilityNote
Low Risk
Low risk: primarily adds new content/pages and small UI refactors; the only behavioral change is consistently date-sorting research lists and introducing a CI build step.
Overview
Adds a new research case study page at
/research/safe-owner-reachability, including aSafeGuaranteeEnglish/formal toggle and a sharedHypothesisdisclosure UI.Introduces
getSortedResearch()and updates the research index and existing research pages to use the date-sorted list for the “More research” sections. Registers the new entry indata/research.jsand refactors the Lido page to import the sharedHypothesiscomponent.Adds a GitHub Actions CI workflow (
.github/workflows/ci.yml) that installs with Bun, restores the Next.js cache, and runsbun run buildon PRs andmainpushes.Reviewed by Cursor Bugbot for commit 33f9da6. Bugbot is set up for automated code reviews on this repo. Configure here.