From 747045ff0fa29ae035918062bc7356dc64e53906 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 22:34:46 -0500 Subject: [PATCH] =?UTF-8?q?docs(agents):=20project-wide=20AGENTS.md=20audi?= =?UTF-8?q?t=20=E2=80=94=20cross-refs,=20baseline,=20contracts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Actions taken from 5-agent audit sweep (audit date 2026-05-26): AGENTS.md / docs sync: - root AGENTS.md: add scripts/qc-flag and lean_expert_agent to Nested Contracts - All 6 nested AGENTS.md files: append Cross-References section pointing to root for Post-Interaction Workflow, Programming Choice Flow, Do Not Sweep, Git Remote Hygiene (Lean, Infra, text-to-cad, docs, qc-flag, lean_expert_agent) - 6-Documentation/docs/AGENTS.md: cross-ref also lists AVMIsa.Emit sole output boundary and Compiler surface blessing Lean build baseline: - 0-Core-Formalism/lean/Semantics/AGENTS.md: update blessed Compiler Surface header to commit ff8e71fa; correct job count to 3311 (lake build Compiler) ARCHITECTURE.md: - §7 repo table: add RRC.Emit, AVMIsa.Emit, RRC.Corpus278 to Lean/Semantics entry - New §7.1 Compiler Surface: documents 3-root pipeline and sole output boundary - §4 Data Flow: annotate output with AVMIsa.Emit sole-boundary note TODO_MAP.md: - Phase A6: add 3 new Lean deliverables (Corpus278, RRC.Emit, AVMIsa.Emit); update status/result with Compiler build baseline; refine next action Build: Compiler 3311 jobs, 0 errors (no Lean changes). 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 | 12 ++++++++-- 4-Infrastructure/AGENTS.md | 8 +++++++ 5-Applications/text-to-cad/AGENTS.md | 8 +++++++ 6-Documentation/docs/AGENTS.md | 11 +++++++++ AGENTS.md | 2 ++ ARCHITECTURE.md | 23 ++++++++++++++++++- TODO_MAP.md | 8 ++++++- scripts/qc-flag/AGENTS.md | 8 +++++++ .../artifacts/lean_expert_agent/AGENTS.md | 8 +++++++ 9 files changed, 84 insertions(+), 4 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index 7d698975..58afe65a 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -83,7 +83,7 @@ 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, commit `9928dd74`) +## Blessed Compiler Surface (as of 2026-05-26, commit `8d158bf9`) The `Compiler` lean_lib in `lakefile.toml` gates the promoted API surface. Only the following roots are blessed for downstream import and receipt emission: @@ -106,7 +106,7 @@ Build the full workspace with: lake build ``` -Full workspace build baseline: **3567 jobs, 0 errors** (commit `9928dd74`). +Compiler surface baseline: **3311 jobs, 0 errors** (`lake build Compiler`, commit `8d158bf9`). ### Architecture: AVM is the sole output boundary @@ -187,3 +187,11 @@ after narrowly compiling the file under a scratch target. - `liftMetaM` is the correct combinator for `MetaM → TacticM` in `mapM`. - `MVarId.toNat` does not exist — use `g.name.toString`. - `List.size` → `.length`; `Json.num Nat` → `Json.num { mantissa := (n : Int), exponent := 0 }`. + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O) +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene** diff --git a/4-Infrastructure/AGENTS.md b/4-Infrastructure/AGENTS.md index 329b8c78..4bb91f07 100644 --- a/4-Infrastructure/AGENTS.md +++ b/4-Infrastructure/AGENTS.md @@ -345,3 +345,11 @@ These tables extend `ene_substrate_schema.sql` (not yet created): phase_hash, residual_total, is_stable - `ene.receipts ADD theorem_id` — FK to prover_state - `ene.receipts ADD dispatch_path` — CHECK(vulkan_gpu, cpu_blitter) + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O — shims must not contain decision/gating/scoring logic) +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene** diff --git a/5-Applications/text-to-cad/AGENTS.md b/5-Applications/text-to-cad/AGENTS.md index 4a28b7f0..733bb663 100644 --- a/5-Applications/text-to-cad/AGENTS.md +++ b/5-Applications/text-to-cad/AGENTS.md @@ -147,3 +147,11 @@ Run from the repository root unless you intentionally want paths to resolve from - If the first pass makes scope clear, edit the source first and validate after. - Do not run generation tools, `cadref`, and `snapshot` in parallel against geometry that is still changing in the same edit loop. Rebuild first, then inspect, then render. - In cloud or constrained environments, avoid full-repo hydration when affected entries are known. Fetch only the needed inputs, generated outputs, and LFS objects for the entries being edited and explicitly regenerated. + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O) +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene** diff --git a/6-Documentation/docs/AGENTS.md b/6-Documentation/docs/AGENTS.md index 099839e5..b76bad84 100644 --- a/6-Documentation/docs/AGENTS.md +++ b/6-Documentation/docs/AGENTS.md @@ -1024,3 +1024,14 @@ must hold byte-for-byte. **Document ID:** AGENTS_LEAN_PORT_STRICT **Version:** 2.2 **Date:** 2026-05-19 + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O) +- **Compiler Surface Blessing** (RRC.Emit, AVMIsa.Emit, RRC.Corpus278 are the 3 blessed roots) +- **AVMIsa.Emit sole output boundary** — nothing outside AVMIsa.Emit may emit a top-level receipt JSON +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene** +- **Nested Contracts** listing all subtree AGENTS.md files diff --git a/AGENTS.md b/AGENTS.md index fa1db2d7..d430896b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -312,6 +312,8 @@ backup/distilled-with-vcd-history-2026-05-11 - Lean module-local contract: `0-Core-Formalism/lean/Semantics/AGENTS.md` - Infrastructure contract: `4-Infrastructure/AGENTS.md` - CAD harness contract: `5-Applications/text-to-cad/AGENTS.md` +- QC flagger contract: `scripts/qc-flag/AGENTS.md` +- Lean expert agent contract: `shared-data/artifacts/lean_expert_agent/AGENTS.md` ## 🚨 CRITICAL RULE #1 - ENE CONTEXT FIRST 🚨 diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 7b32d68d..2775a4a0 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -99,6 +99,7 @@ Raw Data └────────┬─────────┘ ▼ Compressed Output + Receipt + (all receipt JSON stamped exclusively by AVMIsa.Emit) ``` --- @@ -138,7 +139,7 @@ GCCL = Law Stack (what must be preserved) | Path | Purpose | |------|---------| -| `0-Core-Formalism/lean/Semantics/` | Lean 4 source (truth), FixedPoint, PIST, GWL, AVMR, FAMM, etc. | +| `0-Core-Formalism/lean/Semantics/` | Lean 4 source (truth), FixedPoint, PIST, GWL, AVMR, FAMM, RRC.Emit, AVMIsa.Emit, RRC.Corpus278 | | `0-Core-Formalism/otom/` | One-Truth-Only-Model consolidated spec | | `0-Core-Formalism/core/` | Rust/Python extraction targets | | `1-Distributed-Systems/` | ENE mesh nodes, gossip, waveprobe | @@ -155,6 +156,26 @@ GCCL = Law Stack (what must be preserved) | `workspace-config/` | IDE and environment settings | | `scratch/` | Experimental code | +### 7.1 Compiler Surface (Blessed Output Boundary) + +The `Compiler` lean_lib (`lakefile.toml`) is the sole gate for downstream +import and receipt emission. Only three roots are blessed: + +| Root | Role | +|------|------| +| `Semantics.RRC.Corpus278` | 278 raw FixtureRows — Python-supplied, Lean-gated; no decisions | +| `Semantics.RRC.Emit` | Alignment classifier (`missingPrediction` / `alignedExact` / etc.) | +| `Semantics.AVMIsa.Emit` | **Sole output boundary** — AVM canaries must pass; stamps and emits all receipt JSON | + +**Invariant:** nothing outside `AVMIsa.Emit` may emit a top-level receipt JSON. +The pipeline is: + +``` +RRC.Corpus278 →(emitCorpus)→ RRC.Emit →(emitRrcCorpus278)→ AVMIsa.Emit → JSON receipt +``` + +Build the narrow surface: `lake build Compiler` (3311 jobs, 0 errors, commit `8d158bf9`). + --- ## 8. Settlements & Promotion Ladder diff --git a/TODO_MAP.md b/TODO_MAP.md index 90c409af..287ffff6 100644 --- a/TODO_MAP.md +++ b/TODO_MAP.md @@ -131,10 +131,16 @@ PCIe FPGA = future math-hell router (VU9P-class) - `4-Infrastructure/shim/rrc_equation_classifier_curriculum.jsonl` - `4-Infrastructure/shim/rrc_equation_classifier_table.csv` - `docs/rrc_equation_classification.md` + - `Semantics/RRC/Corpus278.lean` — 278 FixtureRows, Python-supplied, Lean-gated ✅ + - `Semantics/RRC/Emit.lean` — alignment classifier (missingPrediction / alignedExact / etc.) ✅ + - `Semantics/AVMIsa/Emit.lean` — sole output boundary; stamps avm.rrc_corpus278.bundle ✅ - **Owner:** Python shim / Lean bridge - **Status:** 🔄 IN_PROGRESS - **Result:** 278 equation surfaces projected; 29 CANDIDATE, 249 HOLD. Labels demoted to non-authoritative route hints. -- **Next action:** Add `scale_band_declared` witnesses and negative-control strength fields, then rerun the receipt and measure HOLD deltas. + Lean Compiler surface (RRC.Corpus278 → RRC.Emit → AVMIsa.Emit) implemented and building: + `lake build Compiler` → 3311 jobs, 0 errors (commit `8d158bf9`). +- **Next action:** Add `scale_band_declared` witnesses and negative-control strength fields, + then rerun the receipt and measure HOLD deltas. --- diff --git a/scripts/qc-flag/AGENTS.md b/scripts/qc-flag/AGENTS.md index 8ae23c2b..4cf9f262 100644 --- a/scripts/qc-flag/AGENTS.md +++ b/scripts/qc-flag/AGENTS.md @@ -37,3 +37,11 @@ bash scripts/qc-flag/run_qc_flag.sh path/to/dir/ --verbose - **JSON**: structured per-file results with issue details - **Markdown**: human-readable report with summary table and issue tables - **Exit code**: 0 if all files pass, 1 if any file has ERROR-severity issues + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O) +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene** diff --git a/shared-data/artifacts/lean_expert_agent/AGENTS.md b/shared-data/artifacts/lean_expert_agent/AGENTS.md index adfe9380..dc157c14 100644 --- a/shared-data/artifacts/lean_expert_agent/AGENTS.md +++ b/shared-data/artifacts/lean_expert_agent/AGENTS.md @@ -66,3 +66,11 @@ Each issue MUST include `file:line` reference, severity (⚠️ ERROR, 🔶 WARN - `6-Documentation/docs/AGENTS.md` for strict operating rules - `0-Core-Formalism/lean/Semantics/Semantics/Physics/` for target inspection - `lake build` at `0-Core-Formalism/lean/Semantics/` for compilation verification + +## Cross-References + +See root `AGENTS.md` for: +- **Post-Interaction Workflow** (mandatory 5-step session-end procedure) +- **Programming Choice Flow** (Lean owns decisions; Python owns I/O) +- **Do Not Sweep** rules (no broad `git add .`) +- **Git Remote Hygiene**