-
Notifications
You must be signed in to change notification settings - Fork 0
Add Safe owner list invariants research page #17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
Th0rgal
wants to merge
13
commits into
main
Choose a base branch
from
add-safe-owner-reachability-page
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
13 commits
Select commit
Hold shift + click to select a range
4526bad
Add Safe owner list reachability invariant research page
claude 934c77e
Fix research ordering and shared hypothesis UI
Th0rgal 87f4a99
Add Bun-based CI workflow
Th0rgal e77b635
Pin GitHub Actions to Node 24 runtime
Th0rgal 5a6392d
Update GitHub Actions to current major versions
Th0rgal 0cc0c5a
Optimize CI workflow execution
Th0rgal c9afafb
Update Safe research page for expanded OwnerManager benchmark
claude 25a1c88
Show all three invariants in hero guarantee toggle
claude b2f4b7a
Update Safe research page to reflect full benchmark state
claude 3990fff
Remove unused ExternalLinkIcon import from SafeGuarantee
claude d548284
Add stronglyAcyclic invariant to hero and disclosure
claude dbcdbf3
Fix proof status table: 9 of 12 theorems proven
claude 33f9da6
Polish Safe owner reachability research page and hero
Th0rgal File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,51 @@ | ||
| name: CI | ||
|
|
||
| on: | ||
| pull_request: | ||
| paths-ignore: | ||
| - 'README.md' | ||
| - 'CLAUDE.md' | ||
| - 'agent.md' | ||
| push: | ||
| branches: | ||
| - main | ||
| paths-ignore: | ||
| - 'README.md' | ||
| - 'CLAUDE.md' | ||
| - 'agent.md' | ||
|
|
||
| env: | ||
| FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true | ||
| NEXT_TELEMETRY_DISABLED: 1 | ||
|
|
||
| concurrency: | ||
| group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | ||
| cancel-in-progress: true | ||
|
|
||
| jobs: | ||
| build: | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 10 | ||
|
|
||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v6 | ||
|
|
||
| - name: Setup Bun | ||
| uses: oven-sh/setup-bun@v2 | ||
| with: | ||
| bun-version: 1.3.9 | ||
|
|
||
| - name: Restore Next.js cache | ||
| uses: actions/cache@v5 | ||
| with: | ||
| path: .next/cache | ||
| key: ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}-${{ hashFiles('pages/**/*', 'components/**/*', 'lib/**/*', 'data/**/*', 'styles/**/*', 'content/**/*', 'public/**/*', 'next.config.js', 'postcss.config.js', 'tailwind.config.js') }} | ||
| restore-keys: | | ||
| ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}- | ||
|
|
||
| - name: Install dependencies | ||
| run: bun install --frozen-lockfile | ||
|
|
||
| - name: Build site | ||
| run: bun run build |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,39 @@ | ||
| export default function Hypothesis({ | ||
| name, | ||
| constraint, | ||
| source, | ||
| children, | ||
| border = true | ||
| }) { | ||
| return ( | ||
| <li | ||
| className={`list-none ${border ? 'border-b border-gray-200/50' : ''}`} | ||
| > | ||
| <details className="group/hyp"> | ||
| <summary className="px-5 py-3 cursor-pointer select-none list-none flex items-center gap-3 [&::-webkit-details-marker]:hidden"> | ||
| <svg | ||
| viewBox="0 0 24 24" | ||
| className="w-3.5 h-3.5 text-muted/50 transition-transform group-open/hyp:rotate-90 flex-shrink-0" | ||
| fill="none" | ||
| stroke="currentColor" | ||
| strokeWidth="1.5" | ||
| strokeLinecap="round" | ||
| strokeLinejoin="round" | ||
| > | ||
| <polyline points="9 6 15 12 9 18" /> | ||
| </svg> | ||
| <code className="font-mono text-[12px] font-medium">{name}</code> | ||
| <span className="text-muted text-[13px]">{constraint}</span> | ||
| </summary> | ||
| <div className="px-5 pb-3 pl-12 text-[13px] text-muted leading-relaxed"> | ||
| <p className="mb-1"> | ||
| <span className="text-[11px] font-mono uppercase tracking-wider text-muted/60"> | ||
| {source} | ||
| </span> | ||
| </p> | ||
| <p>{children}</p> | ||
| </div> | ||
| </details> | ||
| </li> | ||
| ) | ||
| } |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,89 @@ | ||
| import { useState, useEffect, useRef } from 'react' | ||
|
|
||
| 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' | ||
| ] | ||
|
|
||
| export default function SafeGuarantee() { | ||
| const [showEnglish, setShowEnglish] = useState(true) | ||
| const timerRef = useRef(null) | ||
|
|
||
| useEffect(() => { | ||
| timerRef.current = setTimeout(() => setShowEnglish(false), 5000) | ||
| return () => clearTimeout(timerRef.current) | ||
| }, []) | ||
|
|
||
| const handleToggle = () => { | ||
| if (timerRef.current) { | ||
| clearTimeout(timerRef.current) | ||
| timerRef.current = null | ||
| } | ||
| setShowEnglish((prev) => !prev) | ||
| } | ||
|
|
||
| return ( | ||
| <div className="py-6"> | ||
| <button | ||
| onClick={handleToggle} | ||
| className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-muted hover:text-heading transition-colors cursor-pointer mb-4" | ||
| > | ||
| <svg | ||
| viewBox="0 0 24 24" | ||
| className="w-[13px] h-[13px]" | ||
| fill="none" | ||
| stroke="currentColor" | ||
| strokeWidth="1.5" | ||
| strokeLinecap="round" | ||
| strokeLinejoin="round" | ||
| > | ||
| <path d="m5 8 6 6" /> | ||
| <path d="m4 14 6-6 2-3" /> | ||
| <path d="M2 5h12" /> | ||
| <path d="M7 2h1" /> | ||
| <path d="m22 22-5-10-5 10" /> | ||
| <path d="M14 18h6" /> | ||
| </svg> | ||
| {showEnglish ? 'Switch to formal' : 'Switch to English'} | ||
| </button> | ||
|
|
||
| <div className="grid text-center [&>*]:col-start-1 [&>*]:row-start-1"> | ||
| <div | ||
| className="flex flex-col items-center justify-center gap-4 md:gap-5 transition-opacity duration-200 text-[0.945rem] md:text-[1.18125rem] font-mono text-primary leading-snug" | ||
| style={{ | ||
| opacity: showEnglish ? 0 : 1, | ||
| pointerEvents: showEnglish ? 'none' : 'auto' | ||
| }} | ||
| aria-hidden={showEnglish} | ||
| > | ||
| {FORMAL_INVARIANTS.map((formal, i) => ( | ||
| <code | ||
| key={i} | ||
| className="block w-full max-w-full overflow-x-auto px-1" | ||
| > | ||
| {formal} | ||
| </code> | ||
| ))} | ||
| </div> | ||
| <div | ||
| className="flex items-center justify-center transition-opacity duration-200" | ||
| style={{ | ||
| opacity: showEnglish ? 1 : 0, | ||
| pointerEvents: showEnglish ? 'auto' : 'none' | ||
| }} | ||
| aria-hidden={!showEnglish} | ||
| > | ||
| <p className="text-xl md:text-2xl leading-snug font-serif max-w-prose mx-auto px-1"> | ||
| The owners mapping forms a proper loop-free linked list starting at | ||
| a special node called{' '} | ||
| <code className="font-mono text-[0.92em] text-primary"> | ||
| SENTINEL | ||
| </code> | ||
| , and the owners are exactly the addresses on that list. | ||
| </p> | ||
| </div> | ||
| </div> | ||
| </div> | ||
| ) | ||
| } | ||
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,5 @@ | ||
| import { research } from '../data/research' | ||
|
|
||
| export function getSortedResearch() { | ||
| return [...research].sort((a, b) => b.date.localeCompare(a.date)) | ||
| } |
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
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
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
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
SafeGuarantee duplicates Guarantee toggle logic and structure
Low Severity
SafeGuaranteeis a near-complete copy ofGuarantee— the state management (useState,useRef,useEffectwith 5-second timer),handleTogglehandler, 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.