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,47 @@
+# PROOF-NEEDS.md
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+
+## Current State
+
+- **LOC**: ~25,000
+- **Languages**: ReScript, Idris2, Zig
+- **Existing ABI proofs**: Extensive — 11 Idris2 files in `src/abi/TypedWasm/ABI/` covering Effects, Epistemic, Levels, Lifetime, Linear, MultiModule, Pointer, Proofs, Region, Tropical, TypedAccess
+- **Dangerous patterns**: None found (comment in Epistemic.idr confirms "no believe_me")
+
+## What Needs Proving
+
+### ReScript Parser Correctness
+- `lib/ocaml/Parser.res`, `Lexer.res`, `Ast.res` — WASM text format parser
+- Prove: parser produces well-formed ASTs that correspond to valid WASM modules
+- Prove: round-trip property (parse . print = id) for the AST
+
+### Multi-Module Safety (src/abi/TypedWasm/ABI/MultiModule.idr)
+- Cross-module memory access is the key innovation
+- Ensure the existing proofs cover all inter-module pointer dereference cases
+- Prove: no module can access memory outside its declared region
+
+### Lifetime / Region Interaction
+- `Lifetime.idr` + `Region.idr` — prove that lifetime-scoped regions never outlive their allocator
+- This is the highest-value proof target for WASM memory safety
+
+### Tropical Type Semantics (Tropical.idr)
+- Tropical semiring operations on types — ensure semiring laws hold
+- This may already be partially proven; audit for completeness
+
+### Linear Type Consumption (Linear.idr)
+- Prove: every linearly-typed value is consumed exactly once
+- This is foundational for the memory safety guarantees
+
+## Recommended Prover
+
+- **Idris2** (already in use with strong proof coverage — deepen and complete)
+
+## Priority
+
+**MEDIUM** — Proof suite is already the most mature in the ecosystem. Focus on completing coverage gaps rather than starting from scratch. The multi-module and lifetime proofs are the highest-value targets.
+
+## 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.

TEST-NEEDS.md

@@ -0,0 +1,57 @@
+# TEST-NEEDS: typed-wasm
+
+## Current State
+
+| Category | Count | Details |
+|----------|-------|---------|
+| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 3 ReScript parser (Ast, Parser, Lexer), 3 Idris2 interface ABI, 2 Zig FFI + cache |
+| **Unit tests** | 1 file | ParserTests.res (~82 assertions) |
+| **Integration tests** | 0 | None |
+| **E2E tests** | 1 | e2e-smoke.mjs (~43 assertions) |
+| **Benchmarks** | 0 | None |
+| **ECHIDNA harness** | 1 | echidna-harness.mjs (7 assertions) |
+
+## What's Missing
+
+### P2P Tests
+- [ ] No tests for Idris2 ABI type checking with Zig FFI
+- [ ] No tests for ReScript parser feeding into Idris2 type checker
+
+### E2E Tests
+- [ ] e2e-smoke exists but only 43 assertions for a type system with 10 safety levels
+- [ ] No WASM module compilation and execution test
+- [ ] No multi-module linking test (MultiModule.idr untested)
+
+### Aspect Tests
+- [ ] **Security**: No memory safety violation detection tests (this IS the product's purpose)
+- [ ] **Performance**: No benchmarks for type checking overhead vs raw WASM
+- [ ] **Concurrency**: No concurrent WASM module compilation tests
+- [ ] **Error handling**: No tests for invalid type annotations, malformed WASM
+
+### Build & Execution
+- [ ] 11 Idris2 modules with 0 Idris2-level tests -- are proofs checked?
+- [ ] Zig FFI integration_test.zig likely a template placeholder
+
+### Benchmarks Needed (CRITICAL)
+- [ ] Type checking overhead per WASM instruction
+- [ ] Memory region tracking performance
+- [ ] Lifetime analysis scaling with module size
+- [ ] Comparison: typed-wasm overhead vs raw WASM execution
+
+### Self-Tests
+- [ ] No type system self-consistency check
+
+## FLAGGED ISSUES
+- **Type safety system with no safety-level-specific tests** -- 10 levels claimed, 0 level-specific test suites
+- **11 Idris2 proof modules with 0 proof verification tests** -- "proven" is unproven
+- **Tropical.idr and Epistemic.idr (novel type features) have 0 tests** -- research features untested
+- **ECHIDNA harness is 7 assertions** -- token gesture, not real verification
+- **arXiv potential claimed** -- paper-worthy claims need paper-worthy evidence
+
+## Priority: P0 (CRITICAL)
+
+## FAKE-FUZZ ALERT
+
+- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
+- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
+- Priority: P2 — creates false impression of fuzz coverage