Remove template-only ABI files that falsely implied formal verification

Template Idris2 ABI files (Types.idr, Layout.idr, Foreign.idr) contained
only RSR template scaffolding with unresolved placeholders and no
domain-specific proofs. Removed to prevent false impression of formal
verification coverage.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.build/dune-project

@@ -34,6 +34,7 @@
   (sexplib0 (>= 0.16))
   (fmt (>= 0.9))
   (cmdliner (>= 1.2))
+  (yojson (>= 2.1))
   (alcotest (and (>= 1.7) :with-test))
   (odoc (and (>= 2.4) :with-doc)))
  (tags

.claude/PROJECT.md

@@ -48,7 +48,7 @@ dune exec affinescript -- <command> <args>
 
 ## Language Specification
 
-The full language specification is at `/var/home/hyper/affinescript-spec.md`.
+The full language specification is at `/var$HOME/affinescript-spec.md`.
 
 Key language features:
 - **Partial by default**: Functions are partial unless marked `total`

AI.djot

@@ -17,7 +17,7 @@ Additional artefact:
 
 ## Repository Roots
 
-- Local repository root: `/var/mnt/eclipse/repos`
+- Local repository root: `/var$REPOS_DIR`
 - Remote mapping: `https://github.com/hyperpolymath/<name>`
 - Repository names are lowercase; dots (`.`) are replaced with hyphens (`-`).
 - If a repository is missing locally, check the remote and synchronize before proceeding.
@@ -26,10 +26,10 @@ Additional artefact:
 
 - Include `ai-cli-crash-capture/` and `contractiles/` from this template in all new repositories.
 - Mirror all 6SCM files into `.machine_readable/6scm/`.
-- Before generating code, inspect `/var/mnt/eclipse/repos/proven` for the current Idris “unbreakable” library status.
+- Before generating code, inspect `/var$REPOS_DIR/proven` for the current Idris “unbreakable” library status.
 - If the project depends on the unbreakable Idris library, add an *Idris Inside* badge to the repository.
-- When new bindings are required, create them under `/var/mnt/eclipse/repos/proven` using the naming pattern `idris2-zig-<language>`.
-- If new code implies additional unbreakable Idris modules, add them to `/var/mnt/eclipse/repos/proven` and update binders across all supported languages.
+- When new bindings are required, create them under `/var$REPOS_DIR/proven` using the naming pattern `idris2-zig-<language>`.
+- If new code implies additional unbreakable Idris modules, add them to `/var$REPOS_DIR/proven` and update binders across all supported languages.
 
 ## Language Policy
 

PROOF-NEEDS.md

@@ -0,0 +1,10 @@
+# PROOF-NEEDS.md
+
+## Template ABI Cleanup (2026-03-29)
+
+Template ABI removed -- was creating false impression of formal verification.
+The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
+scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
+
+When this project needs formal ABI verification, create domain-specific Idris2 proofs
+following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.