From d3e18e88f01951303bcc6d75a3823a33725abbbc Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 22:26:16 -0500 Subject: [PATCH] docs(agents): add programming choice flow to post-interaction workflow MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds §5 Programming choice flow — a decision tree that runs before writing any new code. Covers: - Admissibility / gating / routing logic → Lean only - Receipt minting / top-level JSON emission → AVMIsa.Emit only (sole boundary) - Alignment classification → Lean (RRC.Emit or new Semantics.RRC.*) - Raw input features → Python shim acceptable with strict constraints (no admissibility logic, regenerable, TODO(lean-port) if portable) - Float in compute paths → STOP, use Q16_16 - Promotion advancement in shim space → STOP, always not_promoted until a Lean gate passes - Pure I/O → Python shim fine, must route receipt output through AVMIsa.Emit Summary rule: Lean owns all decisions. Python owns all I/O. Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- AGENTS.md | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/AGENTS.md b/AGENTS.md index 0270a439..fa1db2d7 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -119,6 +119,54 @@ 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. +### 5. Programming choice flow (check before writing any new code) + +Before writing or placing any new logic, run through this decision tree in +order. Stop at the first rule that applies. + +``` +New logic needed? +│ +├── Does it make an admissibility, routing, alignment, or gating decision? +│ └── YES → Write it in Lean. No Python equivalent allowed. +│ File: Semantics/RRC/Emit.lean or a new Semantics.* module. +│ +├── Does it mint, stamp, or emit a top-level receipt or JSON bundle? +│ └── YES → It belongs in Semantics.AVMIsa.Emit ONLY. +│ AVMIsa.Emit is the sole output boundary. No other module +│ may call leanBuildReceipt and produce a top-level JSON. +│ +├── Does it classify rows, run an alignment gate, or compute scores? +│ └── YES → Lean (Semantics.RRC.Emit or a new Semantics.RRC.* module). +│ Python may call it via #eval / lake exe but may not replicate it. +│ +├── Does it supply raw input features (equation text, route_hint, domain_type, +│ equation_id hashing, weak_axes count)? +│ └── YES → Python shim is acceptable. The shim must: +│ (a) produce only a List FixtureRow (or equivalent data structure) +│ (b) carry no admissibility logic — every field it sets is "raw" +│ (c) be regenerable from source (document the regeneration command) +│ (d) live in 4-Infrastructure/shim/ with a clear TODO(lean-port) if +│ any logic in it could eventually move to Lean +│ +├── Does it use floating-point arithmetic in a compute path? +│ └── YES → STOP. Use Q16_16.ofNat / Q16_16.ofRatio / Q16_16.ofInt instead. +│ ofFloat is only permitted at the external boundary (JSON parsing, +│ sensor input) and must be immediately bracketed. +│ +├── Does it advance promotion status (e.g. set promotion = "promoted")? +│ └── YES → STOP. Promotion is always not_promoted until a Lean gate +│ explicitly passes. Never advance it in shim space or by hand. +│ +└── Is it pure I/O (read JSON, write JSONL, call subprocess, format output)? + └── YES → Python shim is fine. Keep it in 4-Infrastructure/shim/. + Receipt-writing Python must still route output through + AVMIsa.Emit (Lean stamps; Python only formats/stores). +``` + +**Summary rule:** Lean owns all decisions. Python owns all I/O. +If you find yourself writing decision logic in Python, stop and port it to Lean. + ### What "every interaction" means This workflow triggers whenever the user message results in: