From 58db0fbada2d93528bed7a25be6baf57535d6d2d Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Fri, 29 May 2026 00:06:12 -0500 Subject: [PATCH] docs: enforce lean-proof skill + no-float rule in AGENTS.md Ground Rules - Added lean-proof skill auto-load requirement to Ground Rules - Added no-Float rule to Ground Rules (front and center) - lean-proof skill has trigger_patterns for auto-activation - lean-autoformalization and vcn-compute-substrate also have triggers - 6 hub skills installed (fpga, systemverilog, verilog-design, math-help, physics-intuition, hardware-counters) - MCP4EDA registered as MCP server --- AGENTS.md | 99 ++++++++----------------------------------------------- 1 file changed, 13 insertions(+), 86 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 88fad4f8..fe0bdde5 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -20,6 +20,15 @@ This file is the first stop for coding agents working in this repository. - Preserve user work. The working tree is often intentionally dirty; do not revert, delete, or stage unrelated files. - Prefer repo-native tools and receipt generators over ad hoc summaries. - Treat Lean as the source of truth for formal or hardware-adjacent claims. +- **Load the `lean-proof` skill before any Lean work.** It enforces the proof + quality contract: no bare sorries, no tautologies, Q16_16 compliance, and + `#eval` witness requirements. Trigger patterns auto-load it on `.lean`, + `lake build`, `sorry`, `Q16_16`, `theorem`, `lemma`, etc. +- **No `Float` in compute paths.** `ofFloat` is only permitted at the external + boundary (JSON parsing, sensor data). All core/main computation uses + `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt`. This applies to + Lean, Python, and Verilog. The HiGHS boundary is the only exception (it + requires float inputs, but the result is immediately converted to Q16_16). - Keep claims bounded: a receipt proves only the gate it actually checks. - Secrets are runtime-only. Use environment variables such as `OLLAMA_API_KEY` or `DEEPSEEK_API_KEY`; never paste, print, or commit literal provider keys. @@ -389,92 +398,10 @@ correct: one prediction per invariant equation id, with provenance for all sourc records. -## 🚨 CRITICAL RULE #1 - ENE CONTEXT FIRST 🚨 - -**ENE is the local memory/context source of truth. BEFORE using ContextStream, -Glob, Grep, Search, Read (for discovery), Explore, Task(Explore), -EnterPlanMode, or ANY local file scanning:** - -``` -STOP → Call ene-contextstream first: - 1. ene_context(user_message="...", save_exchange=true) on session/message start - 2. ene_status if only health is needed - 3. ene_search(query="...", sources=["ene_api", "local_memory"]) - 4. ene_recall(query="...") when looking for prior decisions/preferences -``` - -**MCP tool names by client usually look like:** - -- `mcp__ene-contextstream__ene_status` -- `mcp__ene-contextstream__ene_context` -- `mcp__ene-contextstream__ene_search` -- `mcp__ene-contextstream__ene_recall` -- `mcp__ene-contextstream__ene_remember` - -If the client cannot call the ENE MCP server, use the local fallback: - -```bash -python3 4-Infrastructure/infra/ene_contextstream_mcp.py --status -``` - -## Remote Proof Agent - -Hermes, OpenCode, Codex, Cursor, Roo, and VS Code should use the -`remote-lean-proof` MCP server for AWS-backed Lean checks when local Lean is -slow or unavailable. The MCP server fronts the dedicated proof service at -`http://54.236.176.28:8787`, requires the runtime token stored outside Git at -`~/.config/ene/language-proof-server.token`, and returns receipt-bearing -responses. - -Active proof-worker pool: - -```text -http://54.236.176.28:8787 AWS EC2 dedicated proof server -http://100.110.163.82:8787 361395-1 Netcup proof worker -http://100.102.173.61:8787 nixos-laptop proof worker -http://100.85.244.73:8787 nixos-steamdeck-1 proof worker -``` - -Primary tools: - -- `proof_status` for health and token wiring. -- `lean_check` for inline Lean snippets. -- `lake_build` for allowlisted repo targets. - -Do not call the raw HTTP proof endpoint directly from agents. Route through the -MCP shim so auth, receipts, and ENE memory can be centralized. - -ContextStream remains a fallback only: - -1. Try ENE first. -2. Use ContextStream second if ENE returns no useful result, `ene-api` is down, - or the task specifically needs ContextStream-hosted transcript history. -3. Use local tools only after ENE and ContextStream fail or after they return - exact file paths that need direct editing. - -## ContextStream Fallback Search - -**BEFORE using Glob, Grep, Search, Read (for discovery), Explore, Task(Explore), EnterPlanMode, or ANY local file scanning:** -``` -STOP → Call search(mode="auto", query="...") FIRST -``` - -**Note:** PreToolUse hooks block these tools when ContextStream is available. -**Claude Code users:** Your tool names are `mcp__contextstream__search`, `mcp__contextstream__init`, etc. - -❌ **NEVER DO THIS:** -- `Glob("**/*.ts")` → Use `search(mode="pattern", query="*.ts")` instead -- `Grep("functionName")` → Use `search(mode="keyword", query="functionName")` instead -- `Read(file)` for discovery → Use `search(mode="auto", query="...")` instead -- `Explore` or `Task(subagent_type="Explore")` → Use `search(mode="auto")` instead -- `EnterPlanMode` for discovery → Use `search(mode="auto", output_format="paths")` instead - -✅ **ALWAYS DO THIS:** -1. `search(mode="auto", query="what you're looking for")` -2. Only use local tools (Glob/Grep/Read) after stale/not-indexed refresh grace window elapses (~20s) or ContextStream still returns **0 results** after retry -3. Use Read ONLY for exact file edits after you know the file path - -This applies to **EVERY search** throughout the **ENTIRE conversation**, not just the first message. +### When to Use ContextStream Search: +✅ Project is indexed and fresh +✅ Looking for code by meaning/concept +✅ Need semantic understanding ---