governance: enforce coordination-repo boundary so bots stop dumping project code#63
Merged
Merged
Conversation
…roject code nextgen-typing is the coordination monorepo (no compiler/application code), but its bot-facing steering still carried RSR-template instructions to put ABI/FFI code in src/interface/ and to "add proofs here". The repo's identity files said one thing while the files agents actually read said another, so agents kept landing typing-project content here instead of in the constituent repos. Prevention (correct boundary at every surface agents actually read): - add root AGENTS.md + CLAUDE.md and root .clinerules/.cursorrules/.windsurfrules carrying the placement boundary + a routing table (none existed before) - add .machine_readable/bot_directives/placement.a2ml as the authoritative, machine-readable routing table; reference it from 0-AI-MANIFEST.a2ml, AI-CONVENTIONS.adoc, AGENTIC.a2ml and bot_directives/README.adoc - strip the src/interface ABI/FFI instructions from copilot-instructions.md, the .machine_readable/ai/ rule files and AI-CONVENTIONS.adoc - rewrite the template-residue AI.a2ml (it still called the repo rsr-template-repo) Enforcement: - add scripts/check-coordination-boundary.sh + the coordination-boundary.yml workflow + a pre-commit hook: fail when project code or a non-allowlisted proof appears in the coordination repo Resite / cleanup: - remove the RSR ABI/TP proof scaffold from verification/proofs/ (those obligations belong in typed-wasm/typell); keep the genuinely cross-project echo-types proof (EchoTyping + Verification aggregator) - reconcile PROOF-NEEDS.md, PROOF-STATUS.md and verification/proofs/README.adoc to coordination reality; record the change in STATE.a2ml Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X2UKV63H4584CQ66qdgxZy
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
nextgen-typingis the coordination monorepo — itsREADME.adoc/0-AI-MANIFEST.a2mlsay it "does NOT contain compiler code … claims are made in constituent repos, never in this coordination layer." But it was scaffolded fromrsr-template-repo(a code-project template), and the bot-facing steering was never updated to match the identity. The files agents actually read still told them to write code here:.github/copilot-instructions.md, the.machine_readable/ai/rule files, and the "authoritative"docs/practice/AI-CONVENTIONS.adocall instructed: "ABI definitions insrc/interface/abi/, FFI insrc/interface/ffi/" — pointing at directories deleted in OQ-001..machine_readable/ai/AI.a2mlwas pure template residue (still called the reporsr-template-repo).verification/proofs/README.adocinvited "Adding New Proofs" with no cross-project gate;AGENTIC.a2mlgrantedcan-edit-source/can-create-fileswith no routing constraint.CLAUDE.md,AGENTS.md, or root.clinerules/.cursorrules/.windsurfrules— so the correct "no code here" rule (buried in0-AI-MANIFEST.a2ml/.machine_readable/) was invisible to most tools, while the visible surfaces misdirected.Net effect: agents kept landing typing-project content here (e.g. #33 integrated a 164-line echo-types Agda proof) instead of in the dedicated repos (
kategoria,typell,typed-wasm,echo-types,choreographic-types,typefix-zero, …).What this PR does
Prevention — correct boundary at every surface agents read
AGENTS.md+CLAUDE.md, root.clinerules/.cursorrules/.windsurfrules— each carries a STOP gate + routing table..machine_readable/bot_directives/placement.a2ml— the authoritative, machine-readable routing table (what this repo accepts vs. what to route where). Referenced from0-AI-MANIFEST.a2ml,AI-CONVENTIONS.adoc,AGENTIC.a2ml,bot_directives/README.adoc.src/interfaceABI/FFI instructions fromcopilot-instructions.md, the.machine_readable/ai/rule files, andAI-CONVENTIONS.adoc; rewrote the residueAI.a2ml.Enforcement (the hard stop)
scripts/check-coordination-boundary.sh+.github/workflows/coordination-boundary.yml+ apre-commithook. Fails when a code scaffold (src/,Cargo.toml, …), implementation source, or a non-allowlisted proof appears. Verified locally: flags the residue pre-cleanup, passes after.Resite / cleanup
verification/proofs/(idris2/ABI/*,Types.idr, genericProperties.agda/ApiTypes.lean/TypeSafety.v/StateMachine.tla) — those obligations belong intyped-wasm/typell.agda/EchoTyping.agda(+Verification.agdaaggregator), which importsecho-typesand relates it to the AffineScript/typed-wasm pipeline — the one documented "allowed here" example.PROOF-NEEDS.md,PROOF-STATUS.md,verification/proofs/README.adoc; recorded inSTATE.a2ml.How the routing works
The boundary is defined once in
placement.a2mland mirrored inAGENTS.md/CLAUDE.md. Rule of thumb baked into every file: if it implements or proves something about one project, it does not go here — open an issue instead of committing on spec.Notes / follow-ups (out of scope here)
typed-wasm) and any echo-types library work (echo-types) live in repos outside this session's write scope — those are not modified by this PR.rsr-template-reporesidue (e.g.Justfileproject := "rsr-template-repo",docs/developer/ABI-FFI-README.adoc, severalsrc/interfacementions in governance docs) tracked under OQ-002. Left untouched to keep this PR focused on the bot-dumping problem; the same template should ideally be fixed upstream so coordination repos don't re-inherit code-repo steering.🤖 Generated with Claude Code
https://claude.ai/code/session_01X2UKV63H4584CQ66qdgxZy
Generated by Claude Code