From ed9ec629d9ef4e5e9d8e29b665b3202cffd9c827 Mon Sep 17 00:00:00 2001
From: William Wolff
Date: Wed, 14 May 2025 18:49:40 +0200
Subject: [PATCH 01/10] site: agda web
---
site/docusaurus.config.ts | 17 +
site/scripts/build-agda-docs.sh | 23 ++
site/scripts/dev-with-formal-spec.sh | 31 ++
site/scripts/process-agda-html.js | 334 +++++++++++++++++++
site/scripts/test-formal-spec-integration.sh | 56 ++++
site/src/pages/formal-spec/index.tsx | 84 +++++
site/src/pages/formal-spec/styles.module.css | 53 +++
7 files changed, 598 insertions(+)
create mode 100755 site/scripts/build-agda-docs.sh
create mode 100755 site/scripts/dev-with-formal-spec.sh
create mode 100755 site/scripts/process-agda-html.js
create mode 100755 site/scripts/test-formal-spec-integration.sh
create mode 100644 site/src/pages/formal-spec/index.tsx
create mode 100644 site/src/pages/formal-spec/styles.module.css
diff --git a/site/docusaurus.config.ts b/site/docusaurus.config.ts
index a69bd2929..384befa6d 100644
--- a/site/docusaurus.config.ts
+++ b/site/docusaurus.config.ts
@@ -1,6 +1,7 @@
import type * as Preset from "@docusaurus/preset-classic";
import type { Config } from "@docusaurus/types";
import { themes as prismThemes } from "prism-react-renderer";
+import path from 'path';
const config: Config = {
title: "Ouroboros Leios",
@@ -37,6 +38,13 @@ const config: Config = {
},
],
+ // Configure static file serving
+ staticDirectories: ['static', 'public'],
+
+ // Configure plugins
+ plugins: [
+ ],
+
presets: [
[
"classic",
@@ -87,6 +95,11 @@ const config: Config = {
position: "left",
label: "Development",
},
+ {
+ to: "/formal-spec/",
+ label: "Formal Specification",
+ position: "left",
+ },
{ to: "/news", label: "Weekly updates", position: "right" },
{
type: "dropdown",
@@ -142,6 +155,10 @@ const config: Config = {
label: "How it works",
to: "/docs/how-it-works",
},
+ {
+ label: "Formal Specification",
+ to: "/formal-spec/",
+ },
{
label: "FAQs",
to: "/docs/faq",
diff --git a/site/scripts/build-agda-docs.sh b/site/scripts/build-agda-docs.sh
new file mode 100755
index 000000000..ffea0690c
--- /dev/null
+++ b/site/scripts/build-agda-docs.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+# Exit on error
+set -e
+
+# Get the directory of this script
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+SITE_DIR="$(dirname "$SCRIPT_DIR")"
+FORMAL_SPEC_DIR="$(cd "$SITE_DIR/../../../ouroboros-leios-formal-spec" && pwd)"
+
+echo "Building Agda documentation..."
+cd "$FORMAL_SPEC_DIR"
+nix build .#leiosDocs
+
+echo "Copying Agda HTML files..."
+mkdir -p "$SITE_DIR/static/agda_html"
+cp -r result/share/doc/agda/html/* "$SITE_DIR/static/agda_html/"
+
+echo "Processing Agda HTML files..."
+cd "$SITE_DIR"
+node scripts/process-agda-html.js
+
+echo "Done! The Agda specification is now available at /agda_html/"
\ No newline at end of file
diff --git a/site/scripts/dev-with-formal-spec.sh b/site/scripts/dev-with-formal-spec.sh
new file mode 100755
index 000000000..26b7892fc
--- /dev/null
+++ b/site/scripts/dev-with-formal-spec.sh
@@ -0,0 +1,31 @@
+#!/bin/bash
+
+# Exit on error
+set -e
+
+# Get the directory of this script
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+SITE_DIR="$(dirname "$SCRIPT_DIR")"
+FORMAL_SPEC_DIR="$(cd "$SITE_DIR/../../ouroboros-leios-formal-spec" && pwd)"
+
+echo "Building Agda documentation..."
+cd "$FORMAL_SPEC_DIR"
+
+# Add Nix configuration for trusted users
+export NIX_CONFIG="trusted-users = root $USER
+substituters = https://cache.nixos.org/
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY="
+
+# Build the docs with --impure to handle dirty git tree
+nix build .#leiosDocs --impure
+
+echo "Copying Agda HTML files..."
+mkdir -p "$SITE_DIR/static/agda_html"
+cp -r result/html/* "$SITE_DIR/static/agda_html/"
+
+echo "Processing Agda HTML files..."
+cd "$SITE_DIR"
+node scripts/process-agda-html.js
+
+echo "Starting development server..."
+yarn start
diff --git a/site/scripts/process-agda-html.js b/site/scripts/process-agda-html.js
new file mode 100755
index 000000000..3b0cd8917
--- /dev/null
+++ b/site/scripts/process-agda-html.js
@@ -0,0 +1,334 @@
+const fs = require('fs');
+const path = require('path');
+
+const AGDA_HTML_DIR = path.join(__dirname, '../static/agda_html');
+
+// First, collect all module information and create search index
+const modules = new Map();
+const moduleGroups = new Map();
+const searchIndex = [];
+
+fs.readdirSync(AGDA_HTML_DIR).forEach(file => {
+ if (file.endsWith('.html')) {
+ const filePath = path.join(AGDA_HTML_DIR, file);
+ const content = fs.readFileSync(filePath, 'utf8');
+ // Look for both h1 and title tags to find module names
+ const h1Match = content.match(/]*>([^<]+)<\/h1>/);
+ const titleMatch = content.match(/]*>([^<]+)<\/title>/);
+ const moduleName = h1Match ? h1Match[1].trim() : (titleMatch ? titleMatch[1].trim() : file);
+
+ // Only include Leios package modules
+ if (moduleName.startsWith('Leios.') ||
+ moduleName.startsWith('Ouroboros.') ||
+ moduleName.startsWith('Cardano.')) {
+
+ // Get the top-level module name for grouping
+ const topLevel = moduleName.split('.')[0];
+ if (!moduleGroups.has(topLevel)) {
+ moduleGroups.set(topLevel, []);
+ }
+
+ const moduleInfo = {
+ name: moduleName,
+ path: file,
+ group: topLevel
+ };
+
+ modules.set(file, moduleInfo);
+ moduleGroups.get(topLevel).push(moduleInfo);
+
+ // Add to search index
+ const lines = content.split('\n');
+ lines.forEach((line, index) => {
+ if (line.trim()) { // Only index non-empty lines
+ // Try to extract the type/expression from the line
+ const typeMatch = line.match(/^([^:]+):/);
+ const expressionMatch = line.match(/^([^=]+)=/);
+ const title = typeMatch ? typeMatch[1].trim() :
+ expressionMatch ? expressionMatch[1].trim() :
+ line.trim();
+
+ searchIndex.push({
+ moduleName: moduleName,
+ path: file,
+ group: topLevel,
+ lineNumber: index + 1,
+ title: title,
+ content: line.trim(),
+ searchableContent: line.toLowerCase()
+ });
+ }
+ });
+ }
+ }
+});
+
+// Create the script file
+const scriptContent = `
+// Search functionality
+const searchIndex = ${JSON.stringify(searchIndex)};
+const searchInput = document.querySelector('.search-input');
+const searchResults = document.querySelector('.search-results');
+const searchOverlay = document.querySelector('.search-overlay');
+
+function toggleSearch() {
+ searchOverlay.classList.toggle('active');
+ if (searchOverlay.classList.contains('active')) {
+ searchInput.focus();
+ }
+}
+
+if (searchInput && searchResults) {
+ // Update the search results HTML generation
+ function generateSearchResults(results) {
+ return results.map(result => {
+ const highlightedTitle = result.title.replace(
+ new RegExp(result.term, 'gi'),
+ match => \`\${match}\`
+ );
+
+ return \`
+
+
+ \${result.content}
+
+ \`;
+ }).join('');
+ }
+
+ searchInput.addEventListener('input', (e) => {
+ const query = e.target.value.toLowerCase();
+ if (query.length < 2) {
+ searchResults.innerHTML = '';
+ return;
+ }
+
+ const results = searchIndex
+ .filter(item => item.searchableContent.includes(query))
+ .map(item => ({
+ ...item,
+ term: query
+ }))
+ .slice(0, 10);
+
+ if (results.length > 0) {
+ searchResults.innerHTML = generateSearchResults(results);
+ } else {
+ searchResults.innerHTML = 'No results found
';
+ }
+ });
+
+ // Add scroll-to-line functionality
+ document.addEventListener('click', (e) => {
+ const result = e.target.closest('.search-result');
+ if (result) {
+ const lineNumber = result.dataset.line;
+ const targetElement = document.querySelector(\`#L\${lineNumber}\`);
+ if (targetElement) {
+ targetElement.scrollIntoView({ behavior: 'smooth', block: 'center' });
+ targetElement.classList.add('highlight-line');
+ setTimeout(() => targetElement.classList.remove('highlight-line'), 2000);
+ }
+ searchOverlay.classList.remove('active');
+ }
+ });
+
+ // Close search when clicking outside or pressing Escape
+ document.addEventListener('click', (e) => {
+ if (e.target === searchOverlay) {
+ searchOverlay.classList.remove('active');
+ }
+ });
+
+ document.addEventListener('keydown', (e) => {
+ if (e.key === 'Escape' && searchOverlay.classList.contains('active')) {
+ searchOverlay.classList.remove('active');
+ }
+ });
+}
+
+// Theme toggle functionality
+function toggleTheme() {
+ const html = document.documentElement;
+ const currentTheme = html.getAttribute('data-theme');
+ const newTheme = currentTheme === 'dark' ? 'light' : 'dark';
+ html.setAttribute('data-theme', newTheme);
+ localStorage.setItem('theme', newTheme);
+}
+
+// Initialize theme from localStorage or system preference
+const savedTheme = localStorage.getItem('theme');
+if (savedTheme) {
+ document.documentElement.setAttribute('data-theme', savedTheme);
+} else if (window.matchMedia('(prefers-color-scheme: dark)').matches) {
+ document.documentElement.setAttribute('data-theme', 'dark');
+}
+`;
+
+fs.writeFileSync(path.join(AGDA_HTML_DIR, 'agda.js'), scriptContent);
+
+// Process all HTML files in the agda_html directory
+fs.readdirSync(AGDA_HTML_DIR).forEach(file => {
+ if (file.endsWith('.html')) {
+ const filePath = path.join(AGDA_HTML_DIR, file);
+ let content = fs.readFileSync(filePath, 'utf8');
+
+ // Add our custom CSS and theme toggle
+ content = content.replace(
+ //,
+ `
+
+ `
+ );
+
+ // Add header, sidebar, and theme toggle
+ content = content.replace(
+ /]*>/,
+ `
+
+
+
+
+
+ `
+ );
+
+ // Close the main content div
+ content = content.replace(
+ /<\/body>/,
+ `
`
+ );
+
+ // Fix internal links
+ content = content.replace(
+ /href="([^"]*\.html)(#[^"]*)?"/g,
+ (match, file, anchor) => {
+ if (file.startsWith('http')) {
+ return match; // Keep external links as is
+ }
+ // Remove any existing /agda_html/ prefix to prevent duplication
+ const cleanFile = file.replace(/^\/?agda_html\//, '');
+ return `href="/agda_html/${cleanFile}${anchor || ''}"`;
+ }
+ );
+
+ // Update the theme toggle button HTML
+ content = content.replace(
+ /
- Available Modules
+ Modules
{AGDA_MODULES.map(module => (
))}
-
- Getting Started
-
- The formal specification is organized into modules, each focusing on different
- aspects of the protocol. Start with these key modules:
-
-
- {AGDA_MODULES.slice(0, 3).map(module => (
- -
-
- {module.name}
-
- {' - '}{module.description}
-
- ))}
-
diff --git a/site/static/agda_html/Agda.css b/site/static/agda_html/Agda.css
new file mode 100644
index 000000000..fc8cb347d
--- /dev/null
+++ b/site/static/agda_html/Agda.css
@@ -0,0 +1,546 @@
+:root {
+ --bg-color: #ffffff;
+ --text-color: #24292e;
+ --border-color: #e1e4e8;
+ --code-bg: #f6f8fa;
+ --link-color: #0366d6;
+ --header-bg: transparent;
+ --sidebar-width: 280px;
+ --content-width: 800px;
+ --search-width: 300px;
+ --hover-color: #f6f8fa;
+ --highlight-color: #ffeb3b;
+ --muted-color: #6a737d;
+ --header-height: 60px;
+ --font-sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, Arial, sans-serif;
+ --font-mono: "Fira Code", "SF Mono", "Roboto Mono", Menlo, Consolas, monospace;
+}
+
+[data-theme="dark"] {
+ --bg-color: #0d1117;
+ --text-color: #c9d1d9;
+ --border-color: #30363d;
+ --code-bg: #161b22;
+ --link-color: #58a6ff;
+ --header-bg: transparent;
+ --hover-color: #161b22;
+ --highlight-color: #ffeb3b;
+ --muted-color: #8b949e;
+}
+
+/* Layout */
+body {
+ margin: 0;
+ padding: 0;
+ min-height: 100vh;
+ display: flex;
+ flex-direction: column;
+ background-color: var(--bg-color);
+ color: var(--text-color);
+ font-family: var(--font-sans);
+ line-height: 1.6;
+}
+
+.agda-header {
+ position: fixed;
+ top: 0;
+ left: 0;
+ right: 0;
+ height: var(--header-height);
+ background-color: var(--bg-color);
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ padding: 0 1.5rem;
+ z-index: 100;
+ border-bottom: none;
+}
+
+.agda-header-left {
+ display: flex;
+ align-items: center;
+ gap: 1.5rem;
+}
+
+.agda-container {
+ display: flex;
+ margin-top: var(--header-height);
+ min-height: calc(100vh - var(--header-height));
+}
+
+.agda-sidebar {
+ position: fixed;
+ top: var(--header-height);
+ left: 0;
+ bottom: 0;
+ width: var(--sidebar-width);
+ background-color: var(--bg-color);
+ overflow-y: auto;
+ padding: 1.5rem;
+ border-right: none;
+}
+
+.agda-sidebar h3 {
+ margin: 0 0 1.5rem 0;
+ font-size: 1.1rem;
+ font-weight: 600;
+ color: var(--text-color);
+ letter-spacing: -0.01em;
+}
+
+.agda-sidebar h4 {
+ margin: 1.5rem 0 0.75rem 0;
+ font-size: 0.9rem;
+ font-weight: 600;
+ color: var(--muted-color);
+ text-transform: uppercase;
+ letter-spacing: 0.05em;
+}
+
+.agda-sidebar ul {
+ list-style: none;
+ padding: 0;
+ margin: 0;
+}
+
+.agda-sidebar li {
+ margin: 0.25rem 0;
+}
+
+.agda-sidebar a {
+ color: var(--text-color);
+ text-decoration: none;
+ font-size: 0.9rem;
+ display: block;
+ padding: 0.35rem 0.5rem;
+ border-radius: 4px;
+ transition: all 0.2s;
+}
+
+.agda-sidebar a:hover {
+ background-color: var(--hover-color);
+ color: var(--link-color);
+}
+
+.agda-sidebar a.active {
+ background-color: var(--hover-color);
+ color: var(--link-color);
+ font-weight: 500;
+}
+
+.agda-content {
+ flex: 1;
+ margin-left: var(--sidebar-width);
+ padding: 2rem;
+ max-width: var(--content-width);
+}
+
+/* Agda Syntax Highlighting */
+.Agda {
+ font-family: var(--font-mono);
+ font-size: 0.95rem;
+ line-height: 1.6;
+ background-color: var(--bg-color);
+ color: var(--text-color);
+}
+
+.Agda code {
+ font-family: var(--font-mono);
+ font-size: 0.95rem;
+ background-color: var(--code-bg);
+ padding: 0.2em 0.4em;
+ border-radius: 3px;
+}
+
+.Agda a {
+ color: var(--link-color);
+ text-decoration: none;
+}
+
+.Agda a:hover {
+ text-decoration: underline;
+}
+
+/* Aspects. */
+.Agda .Comment { color: #B22222 }
+.Agda .Background {}
+.Agda .Markup { color: #000000 }
+.Agda .Keyword { color: #CD6600 }
+.Agda .String { color: #B22222 }
+.Agda .Number { color: #A020F0 }
+.Agda .Symbol { color: #404040 }
+.Agda .PrimitiveType { color: #0000CD }
+.Agda .Pragma { color: black }
+.Agda .Operator {}
+.Agda .Hole { background: #B4EEB4 }
+
+/* NameKinds. */
+.Agda .Bound { color: black }
+.Agda .Generalizable { color: black }
+.Agda .InductiveConstructor { color: #008B00 }
+.Agda .CoinductiveConstructor { color: #8B7500 }
+.Agda .Datatype { color: #0000CD }
+.Agda .Field { color: #EE1289 }
+.Agda .Function { color: #0000CD }
+.Agda .Macro { color: #0000CD }
+.Agda .Module { color: #A020F0 }
+.Agda .Postulate { color: #0000CD }
+.Agda .Primitive { color: #0000CD }
+.Agda .Record { color: #0000CD }
+
+/* OtherAspects. */
+.Agda .DottedPattern {}
+.Agda .UnsolvedMeta { color: black; background: yellow }
+.Agda .UnsolvedConstraint { color: black; background: yellow }
+.Agda .TerminationProblem { color: black; background: #FFA07A }
+.Agda .IncompletePattern { color: black; background: #F5DEB3 }
+.Agda .Error { color: red; text-decoration: underline }
+.Agda .TypeChecks { color: black; background: #ADD8E6 }
+.Agda .Deadcode { color: black; background: #808080 }
+.Agda .ShadowingInTelescope { color: black; background: #808080 }
+
+/* Standard attributes. */
+.Agda a { text-decoration: none }
+.Agda a[href]:hover { background-color: #B4EEB4 }
+.Agda [href].hover-highlight { background-color: #B4EEB4; }
+
+/* Back link styling */
+.agda-header-left a {
+ color: var(--muted-color);
+ text-decoration: none;
+ font-size: 0.9rem;
+ display: flex;
+ align-items: center;
+ gap: 0.5rem;
+ transition: all 0.2s;
+}
+
+.agda-header-left a:hover {
+ color: var(--link-color);
+}
+
+.agda-header-left a::before {
+ content: "←";
+ font-size: 1.1em;
+}
+
+/* Dark mode syntax highlighting improvements */
+[data-theme="dark"] .Agda .Comment {
+ color: #8b949e;
+}
+
+[data-theme="dark"] .Agda .Keyword {
+ color: #ff7b72;
+}
+
+[data-theme="dark"] .Agda .Number {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .String {
+ color: #a5d6ff;
+}
+
+[data-theme="dark"] .Agda .Symbol {
+ color: #c9d1d9;
+}
+
+[data-theme="dark"] .Agda .Function {
+ color: #d2a8ff;
+}
+
+[data-theme="dark"] .Agda .Module {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .Postulate {
+ color: #ffa657;
+}
+
+[data-theme="dark"] .Agda .Type {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .Record {
+ color: #d2a8ff;
+}
+
+[data-theme="dark"] .Agda .Constructor {
+ color: #7ee787;
+}
+
+[data-theme="dark"] .Agda .Field {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .Bound {
+ color: #c9d1d9;
+}
+
+[data-theme="dark"] .Agda .Generalizable {
+ color: #c9d1d9;
+}
+
+[data-theme="dark"] .Agda .InductiveConstructor {
+ color: #7ee787;
+}
+
+[data-theme="dark"] .Agda .CoinductiveConstructor {
+ color: #ffa657;
+}
+
+[data-theme="dark"] .Agda .Datatype {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .Macro {
+ color: #d2a8ff;
+}
+
+[data-theme="dark"] .Agda .Primitive {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .PrimitiveType {
+ color: #79c0ff;
+}
+
+[data-theme="dark"] .Agda .Operator {
+ color: #c9d1d9;
+}
+
+[data-theme="dark"] .Agda .Hole {
+ background: #1b4b1b;
+}
+
+[data-theme="dark"] .Agda .UnsolvedMeta {
+ color: #c9d1d9;
+ background: #5a1a1a;
+}
+
+[data-theme="dark"] .Agda .UnsolvedConstraint {
+ color: #c9d1d9;
+ background: #5a1a1a;
+}
+
+[data-theme="dark"] .Agda .TerminationProblem {
+ color: #c9d1d9;
+ background: #5a1a1a;
+}
+
+[data-theme="dark"] .Agda .IncompletePattern {
+ color: #c9d1d9;
+ background: #5a1a1a;
+}
+
+[data-theme="dark"] .Agda .Error {
+ color: #ff7b72;
+ text-decoration: underline;
+}
+
+[data-theme="dark"] .Agda .TypeChecks {
+ color: #c9d1d9;
+ background: #1b4b1b;
+}
+
+[data-theme="dark"] .Agda .Deadcode {
+ color: #8b949e;
+ background: #30363d;
+}
+
+[data-theme="dark"] .Agda .ShadowingInTelescope {
+ color: #8b949e;
+ background: #30363d;
+}
+
+/* Search and Theme Toggle */
+.search-button {
+ display: flex;
+ align-items: center;
+ gap: 0.5rem;
+ padding: 0.5rem 1rem;
+ border: none;
+ background: none;
+ color: var(--text-color);
+ cursor: pointer;
+ font-size: 0.9rem;
+ transition: all 0.2s;
+ opacity: 0.8;
+ font-family: var(--font-sans);
+}
+
+.search-button:hover {
+ opacity: 1;
+ color: var(--link-color);
+}
+
+.theme-toggle {
+ background: none;
+ border: none;
+ cursor: pointer;
+ padding: 0.5rem;
+ width: 24px;
+ height: 24px;
+ opacity: 0.8;
+ transition: opacity 0.2s;
+ color: var(--text-color);
+ display: flex;
+ align-items: center;
+ justify-content: center;
+}
+
+.theme-toggle:hover {
+ opacity: 1;
+ color: var(--link-color);
+}
+
+.search-button svg {
+ width: 16px;
+ height: 16px;
+}
+
+.search-overlay {
+ position: fixed;
+ top: 0;
+ left: 0;
+ right: 0;
+ bottom: 0;
+ background-color: rgba(0, 0, 0, 0.5);
+ display: none;
+ z-index: 1000;
+}
+
+.search-overlay.active {
+ display: flex;
+ align-items: flex-start;
+ justify-content: center;
+ padding-top: 10vh;
+}
+
+.search-modal {
+ background-color: var(--bg-color);
+ border-radius: 8px;
+ box-shadow: 0 4px 12px rgba(0, 0, 0, 0.15);
+ width: 90%;
+ max-width: 800px;
+ max-height: 80vh;
+ overflow: hidden;
+}
+
+.search-container {
+ padding: 1rem;
+}
+
+.search-input {
+ width: 100%;
+ padding: 0.75rem 1rem;
+ border: 1px solid var(--border-color);
+ border-radius: 4px;
+ background-color: var(--bg-color);
+ color: var(--text-color);
+ font-size: 1rem;
+ transition: border-color 0.2s;
+ margin-bottom: 1rem;
+}
+
+.search-input:focus {
+ outline: none;
+ border-color: var(--link-color);
+}
+
+.search-results {
+ max-height: calc(80vh - 5rem);
+ overflow-y: auto;
+}
+
+.search-result {
+ display: block;
+ padding: 1rem;
+ border-bottom: 1px solid var(--border-color);
+ text-decoration: none;
+ color: var(--text-color);
+ transition: background-color 0.2s;
+}
+
+.search-result:hover {
+ background-color: var(--hover-color);
+}
+
+.search-header {
+ margin: 0 0 0.5rem 0;
+ font-size: 1.1em;
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+}
+
+.search-identifier {
+ font-weight: 500;
+}
+
+.search-module {
+ font-size: 0.9em;
+ color: var(--muted-color);
+ margin-left: 1rem;
+}
+
+.search-type {
+ font-family: var(--font-mono);
+ font-size: 0.9em;
+ color: var(--muted-color);
+ display: block;
+ white-space: nowrap;
+ overflow: hidden;
+ text-overflow: ellipsis;
+}
+
+.search-match {
+ background-color: var(--highlight-color);
+ color: var(--text-color);
+ padding: 0 2px;
+ border-radius: 2px;
+}
+
+.search-no-results {
+ padding: 1rem;
+ color: var(--muted-color);
+ text-align: center;
+}
+
+.theme-toggle svg {
+ width: 24px;
+ height: 24px;
+ fill: currentColor;
+}
+
+[data-theme="dark"] .light-icon,
+[data-theme="light"] .dark-icon {
+ display: none;
+}
+
+.agda-header-right {
+ display: flex;
+ align-items: center;
+ gap: 1rem;
+}
+
+.github-link {
+ display: flex;
+ align-items: center;
+ justify-content: center;
+ width: 24px;
+ height: 24px;
+ color: var(--text-color);
+ opacity: 0.8;
+ transition: opacity 0.2s;
+}
+
+.github-link:hover {
+ opacity: 1;
+}
+
+.github-link svg {
+ width: 24px;
+ height: 24px;
+ fill: currentColor;
+}
diff --git a/site/static/agda_html/agda.js b/site/static/agda_html/agda.js
new file mode 100644
index 000000000..111ae3fe4
--- /dev/null
+++ b/site/static/agda_html/agda.js
@@ -0,0 +1,102 @@
+
+// Search functionality
+const searchIndex = [{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":1,"title":"","content":"","searchableContent":""},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":2,"title":"Leios.Abstract{-# OPTIONS --safe #-}","searchableContent":"leios.abstract{-# options --safe #-}"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":4,"title":"module Leios.Abstract where","searchableContent":"module leios.abstract where"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":6,"title":"open import Leios.Prelude","searchableContent":"open import leios.prelude"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":8,"title":"record LeiosAbstract ","content":"record LeiosAbstract : Type₁ where","searchableContent":"record leiosabstract : type₁ where"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":9,"title":"field Tx ","content":"field Tx : Type","searchableContent":" field tx : type"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":10,"title":"⦃ DecEq-Tx ⦄ ","content":"⦃ DecEq-Tx ⦄ : DecEq Tx","searchableContent":" ⦃ deceq-tx ⦄ : deceq tx"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":11,"title":"PoolID ","content":"PoolID : Type","searchableContent":" poolid : type"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":12,"title":"⦃ DecEq-PoolID ⦄ ","content":"⦃ DecEq-PoolID ⦄ : DecEq PoolID","searchableContent":" ⦃ deceq-poolid ⦄ : deceq poolid"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":13,"title":"BodyHash VrfPf PrivKey Sig Hash ","content":"BodyHash VrfPf PrivKey Sig Hash : Type ","searchableContent":" bodyhash vrfpf privkey sig hash : type "},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":14,"title":"⦃ DecEq-Hash ⦄ ","content":"⦃ DecEq-Hash ⦄ : DecEq Hash","searchableContent":" ⦃ deceq-hash ⦄ : deceq hash"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":15,"title":"⦃ DecEq-VrfPf ⦄ ","content":"⦃ DecEq-VrfPf ⦄ : DecEq VrfPf","searchableContent":" ⦃ deceq-vrfpf ⦄ : deceq vrfpf"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":16,"title":"⦃ DecEq-Sig ⦄ ","content":"⦃ DecEq-Sig ⦄ : DecEq Sig","searchableContent":" ⦃ deceq-sig ⦄ : deceq sig"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":17,"title":"Vote ","content":"Vote : Type","searchableContent":" vote : type"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":18,"title":"⦃ DecEq-Vote ⦄ ","content":"⦃ DecEq-Vote ⦄ : DecEq Vote","searchableContent":" ⦃ deceq-vote ⦄ : deceq vote"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":19,"title":"vote ","content":"vote : PrivKey → Hash → Vote","searchableContent":" vote : privkey → hash → vote"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":20,"title":"sign ","content":"sign : PrivKey → Hash → Sig","searchableContent":" sign : privkey → hash → sig"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":21,"title":"⦃ Hashable-Txs ⦄ ","content":"⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash","searchableContent":" ⦃ hashable-txs ⦄ : hashable (list tx) hash"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":22,"title":"L ","content":"L : ℕ","searchableContent":" l : ℕ"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":23,"title":"⦃ NonZero-L ⦄ ","content":"⦃ NonZero-L ⦄ : NonZero L","searchableContent":" ⦃ nonzero-l ⦄ : nonzero l"},{"moduleName":"Leios.Abstract","path":"Leios.Abstract.html","group":"Leios","lineNumber":24,"title":"","content":"","searchableContent":""},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":1,"title":"","content":"","searchableContent":""},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":2,"title":"Leios.Base{-# OPTIONS --safe #-}","searchableContent":"leios.base{-# options --safe #-}"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":4,"title":"open import Leios.Prelude","searchableContent":"open import leios.prelude"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":5,"title":"open import Leios.Abstract","searchableContent":"open import leios.abstract"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":6,"title":"open import Leios.VRF","searchableContent":"open import leios.vrf"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":8,"title":"module Leios.Base (a ","content":"module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) (vrf' : LeiosVRF a)","searchableContent":"module leios.base (a : leiosabstract) (open leiosabstract a) (vrf' : leiosvrf a)"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":9,"title":"(let open LeiosVRF vrf') where","searchableContent":" (let open leiosvrf vrf') where"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":11,"title":"open import Leios.Blocks a using (EndorserBlock)","searchableContent":"open import leios.blocks a using (endorserblock)"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":13,"title":"StakeDistr ","content":"StakeDistr : Type","searchableContent":"stakedistr : type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":14,"title":"StakeDistr = TotalMap PoolID ℕ","searchableContent":"stakedistr = totalmap poolid ℕ"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":16,"title":"RankingBlock ","content":"RankingBlock : Type","searchableContent":"rankingblock : type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":17,"title":"RankingBlock = These EndorserBlock (List Tx)","searchableContent":"rankingblock = these endorserblock (list tx)"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":19,"title":"record BaseAbstract ","content":"record BaseAbstract : Type₁ where","searchableContent":"record baseabstract : type₁ where"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":20,"title":"field Cert ","content":"field Cert : Type","searchableContent":" field cert : type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":21,"title":"VTy ","content":"VTy : Type","searchableContent":" vty : type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":22,"title":"initSlot ","content":"initSlot : VTy → ℕ","searchableContent":" initslot : vty → ℕ"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":23,"title":"V-chkCerts ","content":"V-chkCerts : List PubKey → EndorserBlock × Cert → Bool","searchableContent":" v-chkcerts : list pubkey → endorserblock × cert → bool"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":25,"title":"data Input ","content":"data Input : Type where","searchableContent":" data input : type where"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":26,"title":"INIT ","content":"INIT : (EndorserBlock × Cert → Bool) → Input","searchableContent":" init : (endorserblock × cert → bool) → input"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":27,"title":"SUBMIT ","content":"SUBMIT : RankingBlock → Input","searchableContent":" submit : rankingblock → input"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":28,"title":"FTCH-LDG ","content":"FTCH-LDG : Input","searchableContent":" ftch-ldg : input"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":30,"title":"data Output ","content":"data Output : Type where","searchableContent":" data output : type where"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":31,"title":"STAKE ","content":"STAKE : StakeDistr → Output","searchableContent":" stake : stakedistr → output"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":32,"title":"EMPTY ","content":"EMPTY : Output","searchableContent":" empty : output"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":33,"title":"BASE-LDG ","content":"BASE-LDG : List RankingBlock → Output","searchableContent":" base-ldg : list rankingblock → output"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":35,"title":"record Functionality ","content":"record Functionality : Type₁ where","searchableContent":" record functionality : type₁ where"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":36,"title":"field State ","content":"field State : Type","searchableContent":" field state : type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":37,"title":"_-⟦_/_⟧⇀_ ","content":"_-⟦_/_⟧⇀_ : State → Input → Output → State → Type","searchableContent":" _-⟦_/_⟧⇀_ : state → input → output → state → type"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":38,"title":"⦃ Dec-_-⟦_/_⟧⇀_ ⦄ ","content":"⦃ Dec-_-⟦_/_⟧⇀_ ⦄ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇","searchableContent":" ⦃ dec-_-⟦_/_⟧⇀_ ⦄ : {s : state} → {i : input} → {o : output} → {s' : state} → (s -⟦ i / o ⟧⇀ s') ⁇"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":39,"title":"SUBMIT-total ","content":"SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s'","searchableContent":" submit-total : ∀ {s b} → ∃[ s' ] s -⟦ submit b / empty ⟧⇀ s'"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":41,"title":"open Input public","searchableContent":" open input public"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":42,"title":"open Output public","searchableContent":" open output public"},{"moduleName":"Leios.Base","path":"Leios.Base.html","group":"Leios","lineNumber":43,"title":"","content":"","searchableContent":"