Add agent documentation discovery endpoints

PrintAxioms.lean

@@ -3943,6 +3943,11 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.Backends.compileStmtList_internalCall_bridged
   Compiler.Proofs.YulGeneration.Backends.compileStmt_externalCallBind_bridged
   Compiler.Proofs.YulGeneration.Backends.compileStmtList_externalCallBind_bridged
+  -- Compiler.Proofs.YulGeneration.Backends.compileStmtList_noFuncDefs_of_perStmtBridge  -- private
+  Compiler.Proofs.YulGeneration.Backends.compileStmt_internalCall_noFuncDefs
+  Compiler.Proofs.YulGeneration.Backends.compileStmtList_internalCall_noFuncDefs
+  Compiler.Proofs.YulGeneration.Backends.compileStmt_externalCallBind_noFuncDefs
+  Compiler.Proofs.YulGeneration.Backends.compileStmtList_externalCallBind_noFuncDefs
   Compiler.Proofs.YulGeneration.Backends.compileStmt_ecm_bridged
   Compiler.Proofs.YulGeneration.Backends.compileStmtList_ecm_bridged
   Compiler.Proofs.YulGeneration.Backends.compileStmtList_append_ok_inv
@@ -5457,4 +5462,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 5162 theorems/lemmas (3583 public, 1579 private, 0 sorry'd)
+-- Total: 5167 theorems/lemmas (3587 public, 1580 private, 0 sorry'd)

docs-site/README.md

@@ -38,12 +38,15 @@ npm start
 ```
 docs-site/
 ├── app/api/docs/[...slug]/route.ts  # API for serving markdown
+├── app/llms-full.txt/route.ts       # Full-docs markdown endpoint
+├── agent-discovery.mjs              # Shared agent discovery headers/routes
 ├── content/                         # Documentation pages (MDX)
 │   ├── index.mdx                    # Homepage
 │   ├── examples.mdx                 # Example contracts
 │   ├── core.mdx                     # Core architecture
 │   └── _meta.js                     # Navigation config
 ├── public/llms.txt                  # AI agent index
+├── public/skill.md                  # Operational workflow for agents
 ├── proxy.ts                         # Middleware for AI agent detection
 └── next.config.mjs                  # Next.js config with Nextra
 ```
@@ -61,7 +64,14 @@ The site automatically serves markdown to AI agents through:
 1. **Auto-detection**: Known AI user agents get markdown automatically
 2. **Explicit format**: Any page with `.md` extension or `?format=md` query
 3. **Accept header**: Requests with `Accept: text/markdown`
-4. **API routes**:
+4. **Plain text fallback**: Requests with `Accept: text/plain`
+5. **Discovery endpoints**:
+   - `/llms.txt` and `/.well-known/llms.txt` - Compact agent index
+   - `/llms-full.txt` and `/.well-known/llms-full.txt` - All docs concatenated (Markdown)
+   - `/skill.md` and `/.well-known/skill.md` - Operational workflow for agents working in Verity
+   - `/.well-known/agent-skills` - JSON skill discovery index
+6. **Discovery headers**: Every response advertises `Link`, `X-Llms-Txt`, `X-Llms-Full-Txt`, and `X-Agent-Skill`
+7. **API routes**:
    - `/api/docs/_index` - List all documents (JSON)
    - `/api/docs/_all` - All docs concatenated (Markdown)
    - `/api/docs/[page]` - Single document (Markdown)

docs-site/agent-discovery.mjs

@@ -0,0 +1,19 @@
+export const AGENT_DISCOVERY_LINKS = [
+  '</llms.txt>; rel="llms-txt"',
+  '</llms-full.txt>; rel="llms-full-txt"',
+  '</skill.md>; rel="agent-skill"',
+].join(", ");
+
+export const AGENT_DISCOVERY_HEADERS = [
+  { key: "Link", value: AGENT_DISCOVERY_LINKS },
+  { key: "X-Llms-Txt", value: "/llms.txt" },
+  { key: "X-Llms-Full-Txt", value: "/llms-full.txt" },
+  { key: "X-Agent-Skill", value: "/skill.md" },
+];
+
+export const AGENT_DISCOVERY_REWRITES = [
+  { source: "/.well-known/llms.txt", destination: "/llms.txt" },
+  { source: "/.well-known/llms-full.txt", destination: "/llms-full.txt" },
+  { source: "/.well-known/skill.md", destination: "/skill.md" },
+  { source: "/.well-known/agent-skills", destination: "/api/agent-skills" },
+];

docs-site/app/api/agent-skills/route.ts

@@ -0,0 +1,21 @@
+import { NextResponse } from "next/server";
+import { agentDiscoveryHeaderRecord } from "@/server/agent-discovery";
+
+export function GET() {
+  return NextResponse.json(
+    {
+      description: "Verity agent skill index",
+      skills: [
+        {
+          name: "verity",
+          url: "/skill.md",
+          description:
+            "Operational guidance for agents adding, porting, proving, and auditing Verity contracts.",
+        },
+      ],
+    },
+    {
+      headers: agentDiscoveryHeaderRecord(),
+    }
+  );
+}

docs-site/app/api/docs/[...slug]/route.ts

@@ -1,62 +1,6 @@
 import { NextRequest, NextResponse } from "next/server";
-import { readFile, readdir, stat } from "fs/promises";
-import { join } from "path";
-
-// Content directory relative to project root
-const CONTENT_DIR = join(process.cwd(), "content");
-
-/**
- * Strip frontmatter from MDX/markdown content
- * Frontmatter is the YAML block between --- markers at the start
- */
-function stripFrontmatter(content: string): string {
-  const frontmatterRegex = /^---\s*\n[\s\S]*?\n---\s*\n/;
-  return content.replace(frontmatterRegex, "").trim();
-}
-
-/**
- * Extract frontmatter metadata from MDX content
- */
-function extractFrontmatter(content: string): Record<string, string> {
-  const match = content.match(/^---\s*\n([\s\S]*?)\n---/);
-  if (!match) return {};
-
-  const frontmatter: Record<string, string> = {};
-  const lines = match[1].split("\n");
-  for (const line of lines) {
-    const [key, ...valueParts] = line.split(":");
-    if (key && valueParts.length) {
-      frontmatter[key.trim()] = valueParts.join(":").trim();
-    }
-  }
-  return frontmatter;
-}
-
-/**
- * List all available documentation files
- */
-async function listDocs(dir: string = CONTENT_DIR, prefix: string = ""): Promise<string[]> {
-  const entries = await readdir(dir, { withFileTypes: true });
-  const docs: string[] = [];
-
-  for (const entry of entries) {
-    // Skip meta files and hidden files
-    if (entry.name.startsWith("_") || entry.name.startsWith(".")) continue;
-
-    const fullPath = join(dir, entry.name);
-    const relativePath = prefix ? `${prefix}/${entry.name}` : entry.name;
-
-    if (entry.isDirectory()) {
-      docs.push(...(await listDocs(fullPath, relativePath)));
-    } else if (entry.name.endsWith(".mdx") || entry.name.endsWith(".md")) {
-      // Convert filename to URL path (remove extension)
-      const urlPath = relativePath.replace(/\.(mdx?|md)$/, "");
-      docs.push(urlPath);
-    }
-  }
-
-  return docs;
-}
+import { agentDiscoveryHeaderRecord } from "@/server/agent-discovery";
+import { buildAllDocsMarkdown, docIndex, readDoc } from "@/server/docs";
 
 /**
  * GET /api/docs/[...slug]
@@ -81,15 +25,15 @@ export async function GET(
   // Special route: list all docs
   if (path === "_index") {
     try {
-      const docs = await listDocs();
-      return NextResponse.json({
-        description: "Verity Documentation Index",
-        docs: docs.map((doc) => ({
-          path: doc,
-          url: `/api/docs/${doc}`,
-          html_url: `/${doc === "index" ? "" : doc}`,
-        })),
-      });
+      return NextResponse.json(
+        {
+          description: "Verity Documentation Index",
+          docs: await docIndex(),
+        },
+        {
+          headers: agentDiscoveryHeaderRecord(),
+        }
+      );
     } catch {
       return NextResponse.json({ error: "Failed to list docs" }, { status: 500 });
     }
@@ -98,50 +42,9 @@ export async function GET(
   // Special route: all docs concatenated
   if (path === "_all") {
     try {
-      const docs = await listDocs();
-      const contents: string[] = [
-        "# Verity - Complete Documentation",
-        "",
-        "> Minimal Lean EDSL for Smart Contracts - All documentation concatenated for AI agent consumption.",
-        "",
-        "---",
-        "",
-      ];
-
-      for (const docPath of docs) {
-        const filePath = join(CONTENT_DIR, `${docPath}.mdx`);
-        try {
-          const content = await readFile(filePath, "utf-8");
-          const frontmatter = extractFrontmatter(content);
-          const markdown = stripFrontmatter(content);
-
-          contents.push(`# ${frontmatter.title || docPath}`);
-          contents.push("");
-          if (frontmatter.description) {
-            contents.push(`> ${frontmatter.description}`);
-            contents.push("");
-          }
-          contents.push(markdown);
-          contents.push("");
-          contents.push("---");
-          contents.push("");
-        } catch {
-          // Try .md extension as fallback
-          try {
-            const mdPath = join(CONTENT_DIR, `${docPath}.md`);
-            const content = await readFile(mdPath, "utf-8");
-            contents.push(stripFrontmatter(content));
-            contents.push("");
-            contents.push("---");
-            contents.push("");
-          } catch {
-            // Skip if file not found
-          }
-        }
-      }
-
-      return new NextResponse(contents.join("\n"), {
+      return new NextResponse(await buildAllDocsMarkdown(), {
         headers: {
+          ...agentDiscoveryHeaderRecord(),
           "Content-Type": "text/markdown; charset=utf-8",
           "Cache-Control": "public, max-age=3600",
           "X-Content-Type-Options": "nosniff",
@@ -155,31 +58,9 @@ export async function GET(
   // Regular doc request - normalize path
   let normalizedPath = path.replace(/\.md$/, ""); // Strip .md extension if present
 
-  // Try to find the file
-  const possiblePaths = [
-    join(CONTENT_DIR, `${normalizedPath}.mdx`),
-    join(CONTENT_DIR, `${normalizedPath}.md`),
-    join(CONTENT_DIR, normalizedPath, "index.mdx"),
-    join(CONTENT_DIR, normalizedPath, "index.md"),
-  ];
-
-  let content: string | null = null;
-  let foundPath: string | null = null;
+  const doc = await readDoc(normalizedPath);
 
-  for (const filePath of possiblePaths) {
-    try {
-      const stats = await stat(filePath);
-      if (stats.isFile()) {
-        content = await readFile(filePath, "utf-8");
-        foundPath = filePath;
-        break;
-      }
-    } catch {
-      // File doesn't exist, try next
-    }
-  }
-
-  if (!content || !foundPath) {
+  if (!doc) {
     return NextResponse.json(
       {
         error: "Document not found",
@@ -190,29 +71,26 @@ export async function GET(
     );
   }
 
-  // Extract metadata and strip frontmatter
-  const frontmatter = extractFrontmatter(content);
-  const markdown = stripFrontmatter(content);
-
   // Build response with optional metadata header
   const includeMetadata = request.nextUrl.searchParams.get("metadata") === "true";
-  let responseContent = markdown;
+  let responseContent = doc.markdown;
 
-  if (includeMetadata && (frontmatter.title || frontmatter.description)) {
+  if (includeMetadata && (doc.metadata.title || doc.metadata.description)) {
     const metaLines = [];
-    if (frontmatter.title) metaLines.push(`# ${frontmatter.title}`);
-    if (frontmatter.description) metaLines.push(`> ${frontmatter.description}`);
+    if (doc.metadata.title) metaLines.push(`# ${doc.metadata.title}`);
+    if (doc.metadata.description) metaLines.push(`> ${doc.metadata.description}`);
     if (metaLines.length) {
-      responseContent = metaLines.join("\n") + "\n\n" + markdown;
+      responseContent = metaLines.join("\n") + "\n\n" + doc.markdown;
     }
   }
 
   return new NextResponse(responseContent, {
     headers: {
+      ...agentDiscoveryHeaderRecord(),
       "Content-Type": "text/markdown; charset=utf-8",
       "Cache-Control": "public, max-age=3600",
       "X-Content-Type-Options": "nosniff",
-      "X-Doc-Title": frontmatter.title || normalizedPath,
+      "X-Doc-Title": doc.metadata.title || normalizedPath,
       "X-Doc-Path": normalizedPath,
     },
   });

docs-site/app/llms-full.txt/route.ts

@@ -0,0 +1,18 @@
+import { NextResponse } from "next/server";
+import { agentDiscoveryHeaderRecord } from "@/server/agent-discovery";
+import { buildAllDocsMarkdown } from "@/server/docs";
+
+export async function GET() {
+  try {
+    return new NextResponse(await buildAllDocsMarkdown(), {
+      headers: {
+        ...agentDiscoveryHeaderRecord(),
+        "Content-Type": "text/markdown; charset=utf-8",
+        "Cache-Control": "public, max-age=3600",
+        "X-Content-Type-Options": "nosniff",
+      },
+    });
+  } catch {
+    return NextResponse.json({ error: "Failed to compile docs" }, { status: 500 });
+  }
+}

docs-site/next.config.mjs

@@ -3,6 +3,7 @@ import { readFileSync } from "fs";
 import { fileURLToPath } from "url";
 import nextra from "nextra";
 import { bundledLanguages, createHighlighter } from "shiki";
+import { AGENT_DISCOVERY_HEADERS, AGENT_DISCOVERY_REWRITES } from "./agent-discovery.mjs";
 
 const configDir = dirname(fileURLToPath(import.meta.url));
 const isDev = process.env.NODE_ENV !== "production";
@@ -54,6 +55,17 @@ export default withNextra({
   images: {
     formats: ["image/avif", "image/webp"],
   },
+  async headers() {
+    return [
+      {
+        source: "/:path*",
+        headers: AGENT_DISCOVERY_HEADERS,
+      },
+    ];
+  },
+  async rewrites() {
+    return AGENT_DISCOVERY_REWRITES;
+  },
   // Redirect legacy URLs to the new IA so old bookmarks / external
   // links don't 404 after the restructure.
   async redirects() {

docs-site/proxy.ts

@@ -1,4 +1,5 @@
 import { NextRequest, NextResponse } from "next/server";
+import { applyAgentDiscoveryHeaders } from "@/server/agent-discovery";
 
 /**
  * Known LLM/AI user agent patterns
@@ -33,8 +34,9 @@ function isLLMUserAgent(userAgent: string | null): boolean {
  * Routes to raw markdown API when:
  * 1. URL ends with .md extension (e.g., /setup.md)
  * 2. Accept header includes text/markdown
- * 3. Query param ?format=md is present
- * 4. User-Agent is a known LLM (ChatGPT, GPTBot, PerplexityBot, etc.)
+ * 3. Accept header includes text/plain
+ * 4. Query param ?format=md is present
+ * 5. User-Agent is a known LLM (ChatGPT, GPTBot, PerplexityBot, etc.)
  *
  * This allows AI agents to fetch documentation as raw markdown
  * while browsers get the rendered HTML version.
@@ -45,6 +47,7 @@ export function proxy(request: NextRequest) {
   // Skip API routes, static files, and Next.js internals
   if (
     pathname.startsWith("/api/") ||
+    pathname.startsWith("/.well-known/") ||
     pathname.startsWith("/_next/") ||
     pathname.startsWith("/static/") ||
     pathname.startsWith("/_pagefind/") ||
@@ -59,6 +62,7 @@ export function proxy(request: NextRequest) {
   const wantsMarkdown =
     pathname.endsWith(".md") ||
     request.headers.get("Accept")?.includes("text/markdown") ||
+    request.headers.get("Accept")?.includes("text/plain") ||
     request.nextUrl.searchParams.get("format") === "md" ||
     isLLMUserAgent(userAgent);
 
@@ -77,10 +81,10 @@ export function proxy(request: NextRequest) {
     url.searchParams.delete("format");
 
     // Rewrite to the API route (internal redirect, URL doesn't change for client)
-    return NextResponse.rewrite(url);
+    return applyAgentDiscoveryHeaders(NextResponse.rewrite(url));
   }
 
-  return NextResponse.next();
+  return applyAgentDiscoveryHeaders(NextResponse.next());
 }
 
 // Only run proxy on relevant paths