mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
docs(agents): post-interaction workflow + Compiler surface update
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>
This commit is contained in:
Brandon Schneider
parent
81a61b6944
commit
36b92418a0
2 changed files with 120 additions and 13 deletions
|
|
@ -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, <passed>, 278 - <passed>)`.
|
||||
|
||||
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)
|
||||
|
||||
|
|
|
|||
78
AGENTS.md
78
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:
|
||||
|
||||
```
|
||||
<type>(<scope>): <summary>
|
||||
|
||||
<body — what changed and why>
|
||||
|
||||
Build: <N> 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`.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue