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

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`.

editors/vscode/lib/bs/.bsdeps

@@ -1,8 +1,8 @@
 11.1.4
-/var/mnt/eclipse/repos/betlang/editors/vscode
+/var$REPOS_DIR/betlang/editors/vscode
 0
 0
 rescript.json	0x1.a5fb25b059f1fp+30
 src	0x1.a5fb263114802p+30
 ===
-/var/mnt/eclipse/repos/betlang/editors/vscode/node_modules/rescript/linux/rescript.exe	0x1.a5fb24e7d80eep+30
+/var$REPOS_DIR/betlang/editors/vscode/node_modules/rescript/linux/rescript.exe	0x1.a5fb24e7d80eep+30

editors/vscode/lib/bs/build.ninja

@@ -1,13 +1,13 @@
 rescript = 1
 rule astj
-  command = /var/mnt/eclipse/repos/betlang/editors/vscode/node_modules/rescript/linux/bsc.exe  -warn-error +101 -bs-v 11.1.4 -uncurried  -absname -bs-ast -o $out $i
+  command = /var$REPOS_DIR/betlang/editors/vscode/node_modules/rescript/linux/bsc.exe  -warn-error +101 -bs-v 11.1.4 -uncurried  -absname -bs-ast -o $out $i
 o src/VSCode.ast : astj ../../src/VSCode.res
 rule deps
-  command = /var/mnt/eclipse/repos/betlang/editors/vscode/node_modules/rescript/linux/bsb_helper.exe -hash 01f137aa28e8f6a8e6efabc3fd6f6c1c $in
+  command = /var$REPOS_DIR/betlang/editors/vscode/node_modules/rescript/linux/bsb_helper.exe -hash 01f137aa28e8f6a8e6efabc3fd6f6c1c $in
   restat = 1
 o src/VSCode.d : deps src/VSCode.ast
 rule mij
-  command = /var/mnt/eclipse/repos/betlang/editors/vscode/node_modules/rescript/linux/bsc.exe -I src   -warn-error +101 -uncurried -bs-package-name betlang-vscode -bs-package-output esmodule:$in_d:.res.js $i
+  command = /var$REPOS_DIR/betlang/editors/vscode/node_modules/rescript/linux/bsc.exe -I src   -warn-error +101 -uncurried -bs-package-name betlang-vscode -bs-package-output esmodule:$in_d:.res.js $i
   dyndep = 1
   restat = 1
 o src/VSCode.cmj src/VSCode.cmi ../../src/VSCode.res.js : mij src/VSCode.ast