Add Safe owner list invariants research page#17
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>
- 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
- Add TikZDiagram (TikZJax) for owners linked-list figure - Disclosure: describe invariant as proper loop-free circular linked list - SafeGuarantee and intro copy adjustments Made-with: Cursor
PR #18 landed the remaining three ownerListInvariant proofs and replaced the unprovable stronglyAcyclic (antisymmetry of reachable, false on Safe's circular list) with uniquePredecessor. Update the article to match: - Proof status: 9/12 -> 12/12, Proofs.lean sorry-free; all table cells flipped to "proven" - "What these invariants cover": four properties -> three (drop the stronglyAcyclic bullet) - "How this was proven": rewrite the strong-acyclicity paragraph around unique-predecessor, with the SENTINEL -> o -> SENTINEL counter-example - Hypotheses: collapse eight entries into four. Solidity require guards merged; hPreInv absorbs hClean; hOwnerInList and hOldNePrev combined; hStrongAcyclic removed; uniquePredecessor added as the new load-bearing structural fact - Drop the "view open theorems" link (OpenProofs.lean is now an index)
…bility-page # Conflicts: # data/research.js
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e1fbac691b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| All 12 theorems are proven.{' '} | ||
| <ExternalLink href="https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Proofs.lean"> |
There was a problem hiding this comment.
This paragraph states that all 12 OwnerManager theorems are proven, but the linked benchmark artifacts currently only define/prove the addOwner reachability result (in_list_reachable_spec / in_list_reachable), so this overstates verification coverage for setupOwners, removeOwner, swapOwner, and the other invariant families. Publishing this as-is misleads readers about what is actually verified and can invalidate the benchmark status shown on the page.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 3 potential issues.
There are 4 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 e1fbac6. Configure here.
| </details> | ||
| </li> | ||
| ) | ||
| } |
There was a problem hiding this comment.
New shared Hypothesis duplicates existing inline component
Low Severity
The newly extracted components/research/Hypothesis.jsx is an exact duplicate of the inline Hypothesis function still present in pages/research/nexus-mutual-book-value.jsx (lines 11–43). The Lido page was refactored to use the shared component, but the Nexus Mutual page was missed, leaving two identical implementations. Any future fix to one copy risks not being applied to the other.
Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.
|
|
||
| export function getSortedResearch() { | ||
| return [...research].sort((a, b) => b.date.localeCompare(a.date)) | ||
| } |
There was a problem hiding this comment.
Nexus Mutual page missed getSortedResearch migration
Low Severity
Every research page was migrated from import { research } to getSortedResearch() except nexus-mutual-book-value.jsx, which still imports the raw research array directly. This means the "More research" section on that page uses raw array order instead of the date-sorted order all other pages guarantee, creating an inconsistency that could produce different orderings if the data file is reordered in the future.
Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.
| const FORMAL_INVARIANTS = [ | ||
| '\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)', | ||
| '\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)', | ||
| '\u2200 a b, reachable(a, b) \u2227 reachable(b, a) \u2192 a = b' |
There was a problem hiding this comment.
Formal invariant displays property page says is false
Medium Severity
The third entry in FORMAL_INVARIANTS — ∀ a b, reachable(a, b) ∧ reachable(b, a) → a = b — is antisymmetry of reachability, which the page's own text explicitly calls out as false on Safe's circular list ("antisymmetry is false on Safe's circular list (SENTINEL → o → SENTINEL makes both directions reachable)"). This formula is meant to represent the acyclic invariant but instead shows a property the page says doesn't hold, creating a direct contradiction on a research page about mathematical proofs.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.
2 participants
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
Medium Risk
Mostly content/UI additions, but it introduces a new GitHub Actions CI workflow and a client-side
TikZDiagramthat loads third-party scripts/styles at runtime, which could affect build stability and page security/performance.Overview
Adds a new research case study page
pages/research/safe-owner-reachability.jsx(and entry indata/research.js) covering Safe OwnerManager linked-list invariants, including an English/formal invariant toggle (SafeGuarantee), hypothesis disclosures (Hypothesis), and embedded TikZ diagrams rendered via TikZJax (TikZDiagram).Refactors research listing/"More research" sections to use a shared
getSortedResearch()helper for consistent date ordering, and extracts the Lido page’s inline hypothesis UI into the reusableHypothesiscomponent.Introduces 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 e1fbac6. Bugbot is set up for automated code reviews on this repo. Configure here.