concept-collection / proofery-web
initial
Jeremy Magland <jmagland@flatironinstitute.org> committed commit c1bee1121f3b Browse files
21 changed files+4797−0
.gitignoreadded+24−0View file
@@ -0,0 +1,24 @@
1+# Logs
2+logs
3+*.log
4+npm-debug.log*
5+yarn-debug.log*
6+yarn-error.log*
7+pnpm-debug.log*
8+lerna-debug.log*
9+
10+node_modules
11+dist
12+dist-ssr
13+*.local
14+
15+# Editor directories and files
16+.vscode/*
17+!.vscode/extensions.json
18+.idea
19+.DS_Store
20+*.suo
21+*.ntvs*
22+*.njsproj
23+*.sln
24+*.sw?
README.mdadded+73−0View file
@@ -0,0 +1,73 @@
1+# React + TypeScript + Vite
2+
3+This template provides a minimal setup to get React working in Vite with HMR and some ESLint rules.
4+
5+Currently, two official plugins are available:
6+
7+- [@vitejs/plugin-react](https://github.com/vitejs/vite-plugin-react/blob/main/packages/plugin-react) uses [Babel](https://babeljs.io/) (or [oxc](https://oxc.rs) when used in [rolldown-vite](https://vite.dev/guide/rolldown)) for Fast Refresh
8+- [@vitejs/plugin-react-swc](https://github.com/vitejs/vite-plugin-react/blob/main/packages/plugin-react-swc) uses [SWC](https://swc.rs/) for Fast Refresh
9+
10+## React Compiler
11+
12+The React Compiler is not enabled on this template because of its impact on dev & build performances. To add it, see [this documentation](https://react.dev/learn/react-compiler/installation).
13+
14+## Expanding the ESLint configuration
15+
16+If you are developing a production application, we recommend updating the configuration to enable type-aware lint rules:
17+
18+```js
19+export default defineConfig([
20+ globalIgnores(['dist']),
21+ {
22+ files: ['**/*.{ts,tsx}'],
23+ extends: [
24+ // Other configs...
25+
26+ // Remove tseslint.configs.recommended and replace with this
27+ tseslint.configs.recommendedTypeChecked,
28+ // Alternatively, use this for stricter rules
29+ tseslint.configs.strictTypeChecked,
30+ // Optionally, add this for stylistic rules
31+ tseslint.configs.stylisticTypeChecked,
32+
33+ // Other configs...
34+ ],
35+ languageOptions: {
36+ parserOptions: {
37+ project: ['./tsconfig.node.json', './tsconfig.app.json'],
38+ tsconfigRootDir: import.meta.dirname,
39+ },
40+ // other options...
41+ },
42+ },
43+])
44+```
45+
46+You can also install [eslint-plugin-react-x](https://github.com/Rel1cx/eslint-react/tree/main/packages/plugins/eslint-plugin-react-x) and [eslint-plugin-react-dom](https://github.com/Rel1cx/eslint-react/tree/main/packages/plugins/eslint-plugin-react-dom) for React-specific lint rules:
47+
48+```js
49+// eslint.config.js
50+import reactX from 'eslint-plugin-react-x'
51+import reactDom from 'eslint-plugin-react-dom'
52+
53+export default defineConfig([
54+ globalIgnores(['dist']),
55+ {
56+ files: ['**/*.{ts,tsx}'],
57+ extends: [
58+ // Other configs...
59+ // Enable lint rules for React
60+ reactX.configs['recommended-typescript'],
61+ // Enable lint rules for React DOM
62+ reactDom.configs.recommended,
63+ ],
64+ languageOptions: {
65+ parserOptions: {
66+ project: ['./tsconfig.node.json', './tsconfig.app.json'],
67+ tsconfigRootDir: import.meta.dirname,
68+ },
69+ // other options...
70+ },
71+ },
72+])
73+```
eslint.config.jsadded+23−0View file
@@ -0,0 +1,23 @@
1+import js from '@eslint/js'
2+import globals from 'globals'
3+import reactHooks from 'eslint-plugin-react-hooks'
4+import reactRefresh from 'eslint-plugin-react-refresh'
5+import tseslint from 'typescript-eslint'
6+import { defineConfig, globalIgnores } from 'eslint/config'
7+
8+export default defineConfig([
9+ globalIgnores(['dist']),
10+ {
11+ files: ['**/*.{ts,tsx}'],
12+ extends: [
13+ js.configs.recommended,
14+ tseslint.configs.recommended,
15+ reactHooks.configs.flat.recommended,
16+ reactRefresh.configs.vite,
17+ ],
18+ languageOptions: {
19+ ecmaVersion: 2020,
20+ globals: globals.browser,
21+ },
22+ },
23+])
index.htmladded+13−0View file
@@ -0,0 +1,13 @@
1+<!doctype html>
2+<html lang="en">
3+ <head>
4+ <meta charset="UTF-8" />
5+ <link rel="icon" type="image/svg+xml" href="/vite.svg" />
6+ <meta name="viewport" content="width=device-width, initial-scale=1.0" />
7+ <title>proofery-web</title>
8+ </head>
9+ <body>
10+ <div id="root"></div>
11+ <script type="module" src="/src/main.tsx"></script>
12+ </body>
13+</html>
package-lock.jsonadded+4001−0View file
This diff is 4,006 lines long and is not shown.
package.jsonadded+36−0View file
@@ -0,0 +1,36 @@
1+{
2+ "name": "proofery-web",
3+ "private": true,
4+ "version": "0.0.0",
5+ "type": "module",
6+ "scripts": {
7+ "dev": "vite",
8+ "build": "tsc -b && vite build",
9+ "lint": "eslint .",
10+ "preview": "vite preview"
11+ },
12+ "dependencies": {
13+ "@emotion/react": "^11.14.0",
14+ "@emotion/styled": "^11.14.1",
15+ "@monaco-editor/react": "^4.7.0",
16+ "@mui/icons-material": "^7.3.6",
17+ "@mui/material": "^7.3.6",
18+ "proofery": "^0.1.1",
19+ "react": "^19.2.0",
20+ "react-dom": "^19.2.0"
21+ },
22+ "devDependencies": {
23+ "@eslint/js": "^9.39.1",
24+ "@types/node": "^24.10.1",
25+ "@types/react": "^19.2.5",
26+ "@types/react-dom": "^19.2.3",
27+ "@vitejs/plugin-react": "^5.1.1",
28+ "eslint": "^9.39.1",
29+ "eslint-plugin-react-hooks": "^7.0.1",
30+ "eslint-plugin-react-refresh": "^0.4.24",
31+ "globals": "^16.5.0",
32+ "typescript": "~5.9.3",
33+ "typescript-eslint": "^8.46.4",
34+ "vite": "^7.2.4"
35+ }
36+}
public/vite.svgadded+1−0View file
@@ -0,0 +1 @@
1+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" aria-hidden="true" role="img" class="iconify iconify--logos" width="31.88" height="32" preserveAspectRatio="xMidYMid meet" viewBox="0 0 256 257"><defs><linearGradient id="IconifyId1813088fe1fbc01fb466" x1="-.828%" x2="57.636%" y1="7.652%" y2="78.411%"><stop offset="0%" stop-color="#41D1FF"></stop><stop offset="100%" stop-color="#BD34FE"></stop></linearGradient><linearGradient id="IconifyId1813088fe1fbc01fb467" x1="43.376%" x2="50.316%" y1="2.242%" y2="89.03%"><stop offset="0%" stop-color="#FFEA83"></stop><stop offset="8.333%" stop-color="#FFDD35"></stop><stop offset="100%" stop-color="#FFA800"></stop></linearGradient></defs><path fill="url(#IconifyId1813088fe1fbc01fb466)" d="M255.153 37.938L134.897 252.976c-2.483 4.44-8.862 4.466-11.382.048L.875 37.958c-2.746-4.814 1.371-10.646 6.827-9.67l120.385 21.517a6.537 6.537 0 0 0 2.322-.004l117.867-21.483c5.438-.991 9.574 4.796 6.877 9.62Z"></path><path fill="url(#IconifyId1813088fe1fbc01fb467)" d="M185.432.063L96.44 17.501a3.268 3.268 0 0 0-2.634 3.014l-5.474 92.456a3.268 3.268 0 0 0 3.997 3.378l24.777-5.718c2.318-.535 4.413 1.507 3.936 3.838l-7.361 36.047c-.495 2.426 1.782 4.5 4.151 3.78l15.304-4.649c2.372-.72 4.652 1.36 4.15 3.788l-11.698 56.621c-.732 3.542 3.979 5.473 5.943 2.437l1.313-2.028l72.516-144.72c1.215-2.423-.88-5.186-3.54-4.672l-25.505 4.922c-2.396.462-4.435-1.77-3.759-4.114l16.646-57.705c.677-2.35-1.37-4.583-3.769-4.113Z"></path></svg>
\ No newline at end of file
src/App.cssadded+42−0View file
@@ -0,0 +1,42 @@
1+#root {
2+ max-width: 1280px;
3+ margin: 0 auto;
4+ padding: 2rem;
5+ text-align: center;
6+}
7+
8+.logo {
9+ height: 6em;
10+ padding: 1.5em;
11+ will-change: filter;
12+ transition: filter 300ms;
13+}
14+.logo:hover {
15+ filter: drop-shadow(0 0 2em #646cffaa);
16+}
17+.logo.react:hover {
18+ filter: drop-shadow(0 0 2em #61dafbaa);
19+}
20+
21+@keyframes logo-spin {
22+ from {
23+ transform: rotate(0deg);
24+ }
25+ to {
26+ transform: rotate(360deg);
27+ }
28+}
29+
30+@media (prefers-reduced-motion: no-preference) {
31+ a:nth-of-type(2) .logo {
32+ animation: logo-spin infinite 20s linear;
33+ }
34+}
35+
36+.card {
37+ padding: 2em;
38+}
39+
40+.read-the-docs {
41+ color: #888;
42+}
src/App.tsxadded+134−0View file
@@ -0,0 +1,134 @@
1+import { useState, useEffect, useRef } from 'react';
2+import { Box, Paper } from '@mui/material';
3+import { ThemeProvider, createTheme } from '@mui/material/styles';
4+import CssBaseline from '@mui/material/CssBaseline';
5+import AppBar from './components/AppBar';
6+import ProofEditor from './components/ProofEditor';
7+import ResultsPanel from './components/ResultsPanel';
8+import { verifyProofContent } from './utils/verification';
9+import type { VerificationResult } from './utils/verification';
10+import { getContentFromUrl, updateUrlWithContent } from './utils/urlState';
11+
12+const theme = createTheme({
13+ palette: {
14+ mode: 'light',
15+ primary: {
16+ main: '#1976d2',
17+ },
18+ },
19+});
20+
21+const DEFAULT_EXAMPLE = `axiom my_axiom
22+ suppose a : Nat
23+ conclude eq(a, a)
24+
25+theorem reflexivity
26+ suppose x : Nat
27+ conclude eq(x, x)
28+ proof
29+ exact my_axiom
30+`;
31+
32+function App() {
33+ // Load content from URL on mount using lazy initialization
34+ const [content, setContent] = useState<string>(() => {
35+ const urlContent = getContentFromUrl();
36+ return urlContent || DEFAULT_EXAMPLE;
37+ });
38+ const [verificationResult, setVerificationResult] = useState<VerificationResult | null>(null);
39+ const [isVerifying, setIsVerifying] = useState(false);
40+ const verificationTimeoutRef = useRef<number | null>(null);
41+ const urlUpdateTimeoutRef = useRef<number | null>(null);
42+
43+ // Debounced verification
44+ useEffect(() => {
45+ if (verificationTimeoutRef.current) {
46+ clearTimeout(verificationTimeoutRef.current);
47+ }
48+
49+ const contentToVerify = content.trim();
50+
51+ verificationTimeoutRef.current = window.setTimeout(() => {
52+ if (!contentToVerify) {
53+ setVerificationResult(null);
54+ setIsVerifying(false);
55+ } else {
56+ setIsVerifying(true);
57+ const result = verifyProofContent(contentToVerify);
58+ setVerificationResult(result);
59+ setIsVerifying(false);
60+ }
61+ }, 500); // 500ms debounce
62+
63+ return () => {
64+ if (verificationTimeoutRef.current) {
65+ clearTimeout(verificationTimeoutRef.current);
66+ }
67+ };
68+ }, [content]);
69+
70+ // Debounced URL update
71+ useEffect(() => {
72+ if (urlUpdateTimeoutRef.current) {
73+ clearTimeout(urlUpdateTimeoutRef.current);
74+ }
75+
76+ urlUpdateTimeoutRef.current = window.setTimeout(() => {
77+ updateUrlWithContent(content);
78+ }, 1000); // 1 second debounce for URL updates
79+
80+ return () => {
81+ if (urlUpdateTimeoutRef.current) {
82+ clearTimeout(urlUpdateTimeoutRef.current);
83+ }
84+ };
85+ }, [content]);
86+
87+ const handleDownload = () => {
88+ const blob = new Blob([content], { type: 'text/plain' });
89+ const url = URL.createObjectURL(blob);
90+ const link = document.createElement('a');
91+ link.href = url;
92+ link.download = 'proof.prf';
93+ document.body.appendChild(link);
94+ link.click();
95+ document.body.removeChild(link);
96+ URL.revokeObjectURL(url);
97+ };
98+
99+ return (
100+ <ThemeProvider theme={theme}>
101+ <CssBaseline />
102+ <Box sx={{ height: '100vh', display: 'flex', flexDirection: 'column' }}>
103+ <AppBar onDownload={handleDownload} />
104+ <Box sx={{ flex: 1, display: 'flex', overflow: 'hidden', p: 2, gap: 2 }}>
105+ <Paper
106+ elevation={2}
107+ sx={{
108+ flex: 1,
109+ display: 'flex',
110+ flexDirection: 'column',
111+ overflow: 'hidden',
112+ p: 2,
113+ }}
114+ >
115+ <ProofEditor content={content} onChange={setContent} />
116+ </Paper>
117+ <Paper
118+ elevation={2}
119+ sx={{
120+ flex: 1,
121+ display: 'flex',
122+ flexDirection: 'column',
123+ overflow: 'hidden',
124+ }}
125+ >
126+ <ResultsPanel result={verificationResult} isVerifying={isVerifying} />
127+ </Paper>
128+ </Box>
129+ </Box>
130+ </ThemeProvider>
131+ );
132+}
133+
134+export default App;
src/assets/react.svgadded+1−0View file
@@ -0,0 +1 @@
1+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" aria-hidden="true" role="img" class="iconify iconify--logos" width="35.93" height="32" preserveAspectRatio="xMidYMid meet" viewBox="0 0 256 228"><path fill="#00D8FF" d="M210.483 73.824a171.49 171.49 0 0 0-8.24-2.597c.465-1.9.893-3.777 1.273-5.621c6.238-30.281 2.16-54.676-11.769-62.708c-13.355-7.7-35.196.329-57.254 19.526a171.23 171.23 0 0 0-6.375 5.848a155.866 155.866 0 0 0-4.241-3.917C100.759 3.829 77.587-4.822 63.673 3.233C50.33 10.957 46.379 33.89 51.995 62.588a170.974 170.974 0 0 0 1.892 8.48c-3.28.932-6.445 1.924-9.474 2.98C17.309 83.498 0 98.307 0 113.668c0 15.865 18.582 31.778 46.812 41.427a145.52 145.52 0 0 0 6.921 2.165a167.467 167.467 0 0 0-2.01 9.138c-5.354 28.2-1.173 50.591 12.134 58.266c13.744 7.926 36.812-.22 59.273-19.855a145.567 145.567 0 0 0 5.342-4.923a168.064 168.064 0 0 0 6.92 6.314c21.758 18.722 43.246 26.282 56.54 18.586c13.731-7.949 18.194-32.003 12.4-61.268a145.016 145.016 0 0 0-1.535-6.842c1.62-.48 3.21-.974 4.76-1.488c29.348-9.723 48.443-25.443 48.443-41.52c0-15.417-17.868-30.326-45.517-39.844Zm-6.365 70.984c-1.4.463-2.836.91-4.3 1.345c-3.24-10.257-7.612-21.163-12.963-32.432c5.106-11 9.31-21.767 12.459-31.957c2.619.758 5.16 1.557 7.61 2.4c23.69 8.156 38.14 20.213 38.14 29.504c0 9.896-15.606 22.743-40.946 31.14Zm-10.514 20.834c2.562 12.94 2.927 24.64 1.23 33.787c-1.524 8.219-4.59 13.698-8.382 15.893c-8.067 4.67-25.32-1.4-43.927-17.412a156.726 156.726 0 0 1-6.437-5.87c7.214-7.889 14.423-17.06 21.459-27.246c12.376-1.098 24.068-2.894 34.671-5.345a134.17 134.17 0 0 1 1.386 6.193ZM87.276 214.515c-7.882 2.783-14.16 2.863-17.955.675c-8.075-4.657-11.432-22.636-6.853-46.752a156.923 156.923 0 0 1 1.869-8.499c10.486 2.32 22.093 3.988 34.498 4.994c7.084 9.967 14.501 19.128 21.976 27.15a134.668 134.668 0 0 1-4.877 4.492c-9.933 8.682-19.886 14.842-28.658 17.94ZM50.35 144.747c-12.483-4.267-22.792-9.812-29.858-15.863c-6.35-5.437-9.555-10.836-9.555-15.216c0-9.322 13.897-21.212 37.076-29.293c2.813-.98 5.757-1.905 8.812-2.773c3.204 10.42 7.406 21.315 12.477 32.332c-5.137 11.18-9.399 22.249-12.634 32.792a134.718 134.718 0 0 1-6.318-1.979Zm12.378-84.26c-4.811-24.587-1.616-43.134 6.425-47.789c8.564-4.958 27.502 2.111 47.463 19.835a144.318 144.318 0 0 1 3.841 3.545c-7.438 7.987-14.787 17.08-21.808 26.988c-12.04 1.116-23.565 2.908-34.161 5.309a160.342 160.342 0 0 1-1.76-7.887Zm110.427 27.268a347.8 347.8 0 0 0-7.785-12.803c8.168 1.033 15.994 2.404 23.343 4.08c-2.206 7.072-4.956 14.465-8.193 22.045a381.151 381.151 0 0 0-7.365-13.322Zm-45.032-43.861c5.044 5.465 10.096 11.566 15.065 18.186a322.04 322.04 0 0 0-30.257-.006c4.974-6.559 10.069-12.652 15.192-18.18ZM82.802 87.83a323.167 323.167 0 0 0-7.227 13.238c-3.184-7.553-5.909-14.98-8.134-22.152c7.304-1.634 15.093-2.97 23.209-3.984a321.524 321.524 0 0 0-7.848 12.897Zm8.081 65.352c-8.385-.936-16.291-2.203-23.593-3.793c2.26-7.3 5.045-14.885 8.298-22.6a321.187 321.187 0 0 0 7.257 13.246c2.594 4.48 5.28 8.868 8.038 13.147Zm37.542 31.03c-5.184-5.592-10.354-11.779-15.403-18.433c4.902.192 9.899.29 14.978.29c5.218 0 10.376-.117 15.453-.343c-4.985 6.774-10.018 12.97-15.028 18.486Zm52.198-57.817c3.422 7.8 6.306 15.345 8.596 22.52c-7.422 1.694-15.436 3.058-23.88 4.071a382.417 382.417 0 0 0 7.859-13.026a347.403 347.403 0 0 0 7.425-13.565Zm-16.898 8.101a358.557 358.557 0 0 1-12.281 19.815a329.4 329.4 0 0 1-23.444.823c-7.967 0-15.716-.248-23.178-.732a310.202 310.202 0 0 1-12.513-19.846h.001a307.41 307.41 0 0 1-10.923-20.627a310.278 310.278 0 0 1 10.89-20.637l-.001.001a307.318 307.318 0 0 1 12.413-19.761c7.613-.576 15.42-.876 23.31-.876H128c7.926 0 15.743.303 23.354.883a329.357 329.357 0 0 1 12.335 19.695a358.489 358.489 0 0 1 11.036 20.54a329.472 329.472 0 0 1-11 20.722Zm22.56-122.124c8.572 4.944 11.906 24.881 6.52 51.026c-.344 1.668-.73 3.367-1.15 5.09c-10.622-2.452-22.155-4.275-34.23-5.408c-7.034-10.017-14.323-19.124-21.64-27.008a160.789 160.789 0 0 1 5.888-5.4c18.9-16.447 36.564-22.941 44.612-18.3ZM128 90.808c12.625 0 22.86 10.235 22.86 22.86s-10.235 22.86-22.86 22.86s-22.86-10.235-22.86-22.86s10.235-22.86 22.86-22.86Z"></path></svg>
\ No newline at end of file
src/components/AppBar.tsxadded+29−0View file
@@ -0,0 +1,29 @@
1+import { AppBar as MuiAppBar, Toolbar, Typography, Button, Box } from '@mui/material';
2+import { Download } from '@mui/icons-material';
3+
4+interface AppBarProps {
5+ onDownload: () => void;
6+}
7+
8+const AppBar: React.FC<AppBarProps> = ({ onDownload }) => {
9+ return (
10+ <MuiAppBar position="static" elevation={1}>
11+ <Toolbar>
12+ <Typography variant="h6" component="div" sx={{ flexGrow: 1 }}>
13+ Proofery - Proof Verification (WIP)
14+ </Typography>
15+ <Box>
16+ <Button
17+ color="inherit"
18+ startIcon={<Download />}
19+ onClick={onDownload}
20+ >
21+ Download .prf
22+ </Button>
23+ </Box>
24+ </Toolbar>
25+ </MuiAppBar>
26+ );
27+};
28+
29+export default AppBar;
src/components/ProofEditor.tsxadded+109−0View file
@@ -0,0 +1,109 @@
1+import { Box } from '@mui/material';
2+import Editor, { type OnMount } from '@monaco-editor/react';
3+
4+interface ProofEditorProps {
5+ content: string;
6+ onChange: (content: string) => void;
7+}
8+
9+const ProofEditor: React.FC<ProofEditorProps> = ({ content, onChange }) => {
10+ const handleEditorChange = (value: string | undefined) => {
11+ onChange(value || '');
12+ };
13+
14+ const handleEditorDidMount: OnMount = (editor, monaco) => {
15+ // Register the proofery language
16+ monaco.languages.register({ id: 'proofery' });
17+
18+ // Define syntax highlighting
19+ monaco.languages.setMonarchTokensProvider('proofery', {
20+ keywords: [
21+ 'axiom',
22+ 'theorem',
23+ 'suppose',
24+ 'conclude',
25+ 'proof',
26+ 'exact',
27+ 'unpack-and',
28+ 'cases',
29+ 'witness',
30+ 'calculate',
31+ 'consider',
32+ 'forall-apply',
33+ 'deconstruct-exists',
34+ 'we-have',
35+ 'focus-or',
36+ 'define',
37+ 'assert',
38+ 'assert-goal',
39+ 'goal',
40+ ],
41+
42+ operators: ['=', '==', ':'],
43+
44+ tokenizer: {
45+ root: [
46+ // Keywords
47+ [
48+ /\b(axiom|theorem|suppose|conclude|proof|exact|unpack-and|cases|witness|calculate|consider|forall-apply|deconstruct-exists|we-have|focus-or|define|assert|assert-goal|goal)\b/,
49+ 'keyword',
50+ ],
51+
52+ // Types (capitalized words)
53+ [/\b[A-Z][a-zA-Z0-9_]*\b/, 'type'],
54+
55+ // Operators
56+ [/[=:]/, 'operator'],
57+
58+ // Identifiers
59+ [/[a-z_][a-zA-Z0-9_]*/, 'identifier'],
60+
61+ // Whitespace
62+ [/[ \t\r\n]+/, 'white'],
63+ ],
64+ },
65+ });
66+
67+ // Define theme colors
68+ monaco.editor.defineTheme('proofery-theme', {
69+ base: 'vs',
70+ inherit: true,
71+ rules: [
72+ { token: 'keyword', foreground: '0000FF', fontStyle: 'bold' },
73+ { token: 'type', foreground: '267F99' },
74+ { token: 'operator', foreground: '000000' },
75+ { token: 'identifier', foreground: '000000' },
76+ ],
77+ colors: {
78+ 'editor.foreground': '#000000',
79+ },
80+ });
81+
82+ // Apply the theme
83+ monaco.editor.setTheme('proofery-theme');
84+ };
85+
86+ return (
87+ <Box sx={{ height: '100%', display: 'flex', flexDirection: 'column' }}>
88+ <Editor
89+ height="100%"
90+ defaultLanguage="proofery"
91+ value={content}
92+ onChange={handleEditorChange}
93+ onMount={handleEditorDidMount}
94+ options={{
95+ minimap: { enabled: false },
96+ fontSize: 14,
97+ lineNumbers: 'on',
98+ scrollBeyondLastLine: false,
99+ wordWrap: 'on',
100+ automaticLayout: true,
101+ tabSize: 4,
102+ insertSpaces: true,
103+ }}
104+ />
105+ </Box>
106+ );
107+};
108+
109+export default ProofEditor;
src/components/ResultsPanel.tsxadded+95−0View file
@@ -0,0 +1,95 @@
1+import { Paper, Typography, Box } from '@mui/material';
2+import { CheckCircle, Error } from '@mui/icons-material';
3+import type { VerificationResult } from '../utils/verification';
4+
5+interface ResultsPanelProps {
6+ result: VerificationResult | null;
7+ isVerifying: boolean;
8+}
9+
10+const ResultsPanel: React.FC<ResultsPanelProps> = ({ result, isVerifying }) => {
11+ if (isVerifying) {
12+ return (
13+ <Box
14+ sx={{
15+ height: '100%',
16+ display: 'flex',
17+ alignItems: 'center',
18+ justifyContent: 'center',
19+ }}
20+ >
21+ <Typography color="text.secondary">Verifying...</Typography>
22+ </Box>
23+ );
24+ }
25+
26+ if (!result) {
27+ return (
28+ <Box
29+ sx={{
30+ height: '100%',
31+ display: 'flex',
32+ alignItems: 'center',
33+ justifyContent: 'center',
34+ }}
35+ >
36+ <Typography color="text.secondary">
37+ Enter proof content to see verification results
38+ </Typography>
39+ </Box>
40+ );
41+ }
42+
43+ return (
44+ <Box sx={{ height: '100%', overflow: 'auto', p: 2 }}>
45+ <Paper
46+ elevation={0}
47+ sx={{
48+ p: 3,
49+ backgroundColor: result.success ? '#e8f5e9' : '#ffebee',
50+ border: `2px solid ${result.success ? '#4caf50' : '#f44336'}`,
51+ }}
52+ >
53+ <Box sx={{ display: 'flex', alignItems: 'center', mb: 2 }}>
54+ {result.success ? (
55+ <CheckCircle sx={{ color: '#4caf50', mr: 1, fontSize: 32 }} />
56+ ) : (
57+ <Error sx={{ color: '#f44336', mr: 1, fontSize: 32 }} />
58+ )}
59+ <Typography
60+ variant="h6"
61+ sx={{ color: result.success ? '#2e7d32' : '#c62828' }}
62+ >
63+ {result.message}
64+ </Typography>
65+ </Box>
66+ {result.error && (
67+ <Box
68+ sx={{
69+ mt: 2,
70+ p: 2,
71+ backgroundColor: 'rgba(0, 0, 0, 0.05)',
72+ borderRadius: 1,
73+ }}
74+ >
75+ <Typography
76+ component="pre"
77+ sx={{
78+ fontFamily: 'monospace',
79+ fontSize: '13px',
80+ whiteSpace: 'pre-wrap',
81+ wordBreak: 'break-word',
82+ margin: 0,
83+ color: '#c62828',
84+ }}
85+ >
86+ {result.error}
87+ </Typography>
88+ </Box>
89+ )}
90+ </Paper>
91+ </Box>
92+ );
93+};
94+
95+export default ResultsPanel;
src/index.cssadded+68−0View file
@@ -0,0 +1,68 @@
1+:root {
2+ font-family: system-ui, Avenir, Helvetica, Arial, sans-serif;
3+ line-height: 1.5;
4+ font-weight: 400;
5+
6+ color-scheme: light dark;
7+ color: rgba(255, 255, 255, 0.87);
8+ background-color: #242424;
9+
10+ font-synthesis: none;
11+ text-rendering: optimizeLegibility;
12+ -webkit-font-smoothing: antialiased;
13+ -moz-osx-font-smoothing: grayscale;
14+}
15+
16+a {
17+ font-weight: 500;
18+ color: #646cff;
19+ text-decoration: inherit;
20+}
21+a:hover {
22+ color: #535bf2;
23+}
24+
25+body {
26+ margin: 0;
27+ display: flex;
28+ place-items: center;
29+ min-width: 320px;
30+ min-height: 100vh;
31+}
32+
33+h1 {
34+ font-size: 3.2em;
35+ line-height: 1.1;
36+}
37+
38+button {
39+ border-radius: 8px;
40+ border: 1px solid transparent;
41+ padding: 0.6em 1.2em;
42+ font-size: 1em;
43+ font-weight: 500;
44+ font-family: inherit;
45+ background-color: #1a1a1a;
46+ cursor: pointer;
47+ transition: border-color 0.25s;
48+}
49+button:hover {
50+ border-color: #646cff;
51+}
52+button:focus,
53+button:focus-visible {
54+ outline: 4px auto -webkit-focus-ring-color;
55+}
56+
57+@media (prefers-color-scheme: light) {
58+ :root {
59+ color: #213547;
60+ background-color: #ffffff;
61+ }
62+ a:hover {
63+ color: #747bff;
64+ }
65+ button {
66+ background-color: #f9f9f9;
67+ }
68+}
src/main.tsxadded+9−0View file
@@ -0,0 +1,9 @@
1+import { StrictMode } from 'react'
2+import { createRoot } from 'react-dom/client'
3+import App from './App.tsx'
4+
5+createRoot(document.getElementById('root')!).render(
6+ <StrictMode>
7+ <App />
8+ </StrictMode>,
9+)
src/utils/urlState.tsadded+38−0View file
@@ -0,0 +1,38 @@
1+// URL state management using base64 encoding
2+
3+export const encodeToUrl = (content: string): string => {
4+ try {
5+ const base64 = btoa(unescape(encodeURIComponent(content)));
6+ return base64;
7+ } catch (error) {
8+ console.error('Error encoding to base64:', error);
9+ return '';
10+ }
11+};
12+
13+export const decodeFromUrl = (base64: string): string => {
14+ try {
15+ const decoded = decodeURIComponent(escape(atob(base64)));
16+ return decoded;
17+ } catch (error) {
18+ console.error('Error decoding from base64:', error);
19+ return '';
20+ }
21+};
22+
23+export const getContentFromUrl = (): string => {
24+ const hash = window.location.hash.slice(1); // Remove the '#'
25+ if (hash) {
26+ return decodeFromUrl(hash);
27+ }
28+ return '';
29+};
30+
31+export const updateUrlWithContent = (content: string): void => {
32+ const encoded = encodeToUrl(content);
33+ if (encoded) {
34+ window.history.replaceState(null, '', `#${encoded}`);
35+ } else {
36+ window.history.replaceState(null, '', window.location.pathname);
37+ }
38+};
src/utils/verification.tsadded+33−0View file
@@ -0,0 +1,33 @@
1+// Verification logic using proofery library
2+
3+import { parseContent, verifyFile } from 'proofery';
4+
5+export interface VerificationResult {
6+ success: boolean;
7+ message: string;
8+ error?: string;
9+}
10+
11+export const verifyProofContent = (content: string): VerificationResult => {
12+ if (!content.trim()) {
13+ return {
14+ success: false,
15+ message: 'No content to verify',
16+ };
17+ }
18+
19+ try {
20+ const blocks = parseContent(content);
21+ verifyFile(blocks, false); // false for non-verbose mode
22+ return {
23+ success: true,
24+ message: '✓ Proof verified successfully!',
25+ };
26+ } catch (error) {
27+ return {
28+ success: false,
29+ message: 'Verification failed',
30+ error: error instanceof Error ? error.message : String(error),
31+ };
32+ }
33+};
tsconfig.app.jsonadded+28−0View file
@@ -0,0 +1,28 @@
1+{
2+ "compilerOptions": {
3+ "tsBuildInfoFile": "./node_modules/.tmp/tsconfig.app.tsbuildinfo",
4+ "target": "ES2022",
5+ "useDefineForClassFields": true,
6+ "lib": ["ES2022", "DOM", "DOM.Iterable"],
7+ "module": "ESNext",
8+ "types": ["vite/client"],
9+ "skipLibCheck": true,
10+
11+ /* Bundler mode */
12+ "moduleResolution": "bundler",
13+ "allowImportingTsExtensions": true,
14+ "verbatimModuleSyntax": true,
15+ "moduleDetection": "force",
16+ "noEmit": true,
17+ "jsx": "react-jsx",
18+
19+ /* Linting */
20+ "strict": true,
21+ "noUnusedLocals": true,
22+ "noUnusedParameters": true,
23+ "erasableSyntaxOnly": true,
24+ "noFallthroughCasesInSwitch": true,
25+ "noUncheckedSideEffectImports": true
26+ },
27+ "include": ["src"]
28+}
tsconfig.jsonadded+7−0View file
@@ -0,0 +1,7 @@
1+{
2+ "files": [],
3+ "references": [
4+ { "path": "./tsconfig.app.json" },
5+ { "path": "./tsconfig.node.json" }
6+ ]
7+}
tsconfig.node.jsonadded+26−0View file
@@ -0,0 +1,26 @@
1+{
2+ "compilerOptions": {
3+ "tsBuildInfoFile": "./node_modules/.tmp/tsconfig.node.tsbuildinfo",
4+ "target": "ES2023",
5+ "lib": ["ES2023"],
6+ "module": "ESNext",
7+ "types": ["node"],
8+ "skipLibCheck": true,
9+
10+ /* Bundler mode */
11+ "moduleResolution": "bundler",
12+ "allowImportingTsExtensions": true,
13+ "verbatimModuleSyntax": true,
14+ "moduleDetection": "force",
15+ "noEmit": true,
16+
17+ /* Linting */
18+ "strict": true,
19+ "noUnusedLocals": true,
20+ "noUnusedParameters": true,
21+ "erasableSyntaxOnly": true,
22+ "noFallthroughCasesInSwitch": true,
23+ "noUncheckedSideEffectImports": true
24+ },
25+ "include": ["vite.config.ts"]
26+}
vite.config.tsadded+7−0View file
@@ -0,0 +1,7 @@
1+import { defineConfig } from 'vite'
2+import react from '@vitejs/plugin-react'
3+
4+// https://vite.dev/config/
5+export default defineConfig({
6+ plugins: [react()],
7+})