From 36b92418a003c5ba1a47102079503fb3fc047470 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 22:25:26 -0500 Subject: [PATCH] docs(agents): post-interaction workflow + Compiler surface update MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Root AGENTS.md: - Add §Post-Interaction Workflow: mandatory steps after every agent session that changes code — update AGENTS.md, verify build, commit, check tree cleanliness. Explicit trigger conditions (file edits, lake build, arch decisions, new TODO/quarantine). Does NOT trigger for read-only sessions. - Update AVM glossary entry: ISA is live; AVM is sole output boundary for RRC receipts; describe AVMIsa.Emit / RRC.Emit / RRC.Corpus278 roles. Semantics/AGENTS.md: - Replace stale Blessed Compiler Surface section with current state (commit 81a61b69, 3567 jobs, 3 roots: RRC.Emit, AVMIsa.Emit, RRC.Corpus278) - Document AVM-sole-output-boundary architecture with ASCII data-flow diagram - Document 278-corpus current state: (278, 0, 278) — correct and honest - Document 5 generator fields for EN9wiki page generation - Document build_corpus278.py regeneration command and Python/Lean role split Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- 0-Core-Formalism/lean/Semantics/AGENTS.md | 55 ++++++++++++---- AGENTS.md | 78 ++++++++++++++++++++++- 2 files changed, 120 insertions(+), 13 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index 3598039f..7d698975 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -83,18 +83,16 @@ lake build - Generated `*_tb.v` and `*_test_vectors.json` files are build artifacts unless a task explicitly promotes one as a hardware receipt. -## Blessed Compiler Surface (as of 2026-05-26) +## Blessed Compiler Surface (as of 2026-05-26, commit `9928dd74`) The `Compiler` lean_lib in `lakefile.toml` gates the promoted API surface. Only the following roots are blessed for downstream import and receipt emission: | Root | Purpose | |------|---------| -| `Semantics.RRC.Emit` | RRC record construction and JSON emission | -| `Semantics.AVMIsa.Emit` | AVM ISA canary runner + receipt emitter (Goal A) | -| `Semantics.AVMIsa.Run` | AVM ISA interpreter (used by Emit) | -| `Semantics.ReceiptCore` | Shared receipt schema types | -| `Semantics.RRCLogogramProjection` | Logogram projection predicate | +| `Semantics.RRC.Emit` | Alignment classifier; `emitCorpus` generic entry point | +| `Semantics.AVMIsa.Emit` | **Sole output boundary** — AVM canaries + stamps all receipts | +| `Semantics.RRC.Corpus278` | 278-equation raw feature list (Python-supplied, Lean-gated) | Build the narrow surface with: @@ -108,12 +106,26 @@ Build the full workspace with: lake build ``` -Full workspace build baseline: **3566 jobs, 0 errors** (commit `c20aa4be` + consolidation). +Full workspace build baseline: **3567 jobs, 0 errors** (commit `9928dd74`). -### Goal A canary receipt (AVMIsa.Emit) +### Architecture: AVM is the sole output boundary -`Semantics/AVMIsa/Emit.lean` runs three AVM ISA canaries and emits a JSON -receipt on every `#eval`. Expected output shape: +``` +RRC.Corpus278 — 278 FixtureRows, raw features only (no decisions) + ↓ emitCorpus +RRC.Emit — alignment gate (missingPrediction / alignedExact / etc.) + ↓ emitRrcCorpus278 +AVMIsa.Emit — AVM canaries must pass; stamps avm.rrc_corpus278.bundle + emits final JSON; SOLE output boundary +``` + +**Rule:** Nothing outside `AVMIsa.Emit` may emit a top-level receipt JSON. +`RRC.Emit` is a classifier that feeds it. `RRC.Corpus278` supplies raw features. + +### Goal A canary receipt (AVMIsa.Emit §1–6) + +Three passing canaries: `avm.canary.not`, `avm.canary.and`, `avm.canary.or`. +Expected `#eval emit.json` shape: ```json { @@ -125,7 +137,28 @@ receipt on every `#eval`. Expected output shape: } ``` -Three passing canaries: `avm.canary.not`, `avm.canary.and`, `avm.canary.or`. +### 278-equation corpus (AVMIsa.Emit §7 / RRC.Corpus278) + +`emitRrcCorpus278` classifies all 278 rows and stamps the bundle. +Expected `#eval` corpus summary: `(278, , 278 - )`. + +Current state: `(278, 0, 278)` — all held, no PIST labels present yet. +This is **correct and honest** — the gate reports exactly what it sees. + +Each row carries 5 generator fields for EN9wiki page generation: +- `operatorTokens` — domain/operator token list (from route_hint + rrc_kind) +- `invariantsDeclared` — declared invariant family (from domain_type) +- `boundaryConds` — binding class (from bind_class) +- `templateKey` — page-generator template (`definition`/`master_equation`/`gate`/`receipt`/`hold`) +- `templateParams` — compact rendering parameter string + +To regenerate `Corpus278.lean` from source: + +```bash +python3 4-Infrastructure/shim/build_corpus278.py +``` + +Python's role: raw feature extraction only. Lean's role: all gating decisions. ## Quarantined Modules (not in build surface) diff --git a/AGENTS.md b/AGENTS.md index 8bd1776d..0270a439 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -58,6 +58,78 @@ This file is the first stop for coding agents working in this repository. and `.vscode/tasks.json`, then use the pinned Python/CAD commands documented in `5-Applications/text-to-cad/AGENTS.md`. +## Post-Interaction Workflow (mandatory after every agent session) + +After every interaction with the user that changes code, Lean modules, +shim scripts, receipts, or architecture decisions, the agent MUST run the +following steps **before claiming the session is complete**: + +### 1. Update AGENTS.md files + +Update the nearest scoped AGENTS.md for every subtree touched: + +| Subtree touched | AGENTS.md to update | +|----------------|-------------------| +| `0-Core-Formalism/lean/Semantics/` | `0-Core-Formalism/lean/Semantics/AGENTS.md` | +| `4-Infrastructure/` | `4-Infrastructure/AGENTS.md` | +| Root or multi-subtree | `AGENTS.md` (this file) | + +Minimum required updates per touched subtree: +- **Blessed surface table** — add/remove/update module rows if Compiler roots changed +- **Build baseline** — update job count and commit hash if `lake build` was run +- **Architecture section** — update if data-flow or boundary rules changed +- **Pending proof work** — add new `TODO(lean-port)` stubs; remove resolved ones +- **Quarantine table** — add quarantined files; remove revived ones + +### 2. Verify the build + +```bash +cd 0-Core-Formalism/lean/Semantics && lake build Compiler +``` + +If Lean files were touched, also run the full build: + +```bash +cd 0-Core-Formalism/lean/Semantics && lake build +``` + +### 3. Commit + +Stage only explicitly touched files (never `git add .`). +Commit message format: + +``` +(): + + + +Build: jobs, 0 errors (lake build) +``` + +Types: `feat`, `fix`, `chore`, `docs`, `refactor`. +Scope examples: `lean`, `rrc`, `avm-isa`, `infra`, `corpus278`. + +### 4. Check tree cleanliness + +```bash +git status --branch --short --untracked-files=all +``` + +Untracked files that are not generated artifacts should either be staged or +noted as intentionally dirty. Do not claim the tree is stable if there are +unexpected modifications. + +### What "every interaction" means + +This workflow triggers whenever the user message results in: +- Any file edit (Lean, Python, TOML, JSON, shell, Rust, etc.) +- Any `lake build` run +- Any architectural decision that changes the data-flow or boundary rules +- Any new `TODO(lean-port)` or quarantine boundary + +It does NOT trigger for pure read-only exploration, explanation, or +questions that result in no file changes. + ## Do Not Sweep Avoid broad cleanup or staging commands such as: @@ -120,8 +192,10 @@ These terms appear throughout all AGENTS.md files and the codebase: Builder/Warden/Judge clock domains. - **GCL** — Genetic Code Language. Self-improving evolutionary program representation. - **AVM** — Adaptive Virtual Machine. Universal bridge between math languages and - Python bytecode (status: core ISA rebuild pending — see §7.4 in - `6-Documentation/docs/AGENTS.md`). + Python bytecode. Core ISA is live in `Semantics.AVMIsa.*` (Types, Value, Instr, + State, Step, Run). AVM is the **sole output boundary** for RRC receipts: + `AVMIsa.Emit` stamps all top-level receipt JSON; `RRC.Emit` and `RRC.Corpus278` + feed it as classifier and raw-feature supplier respectively. - **enwik9** — the Hutter Prize 1GB Wikipedia XML corpus, used as the canonical end-to-end test vector for the hierarchical compressor. - **receipt** — a machine-readable attestation record stored in `ene.receipts`.