Skip to content

Commit 322dba8

Browse files
hyperpolymathclaude
andcommitted
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>
1 parent 74ac06c commit 322dba8

4 files changed

Lines changed: 10 additions & 622 deletions

File tree

PROOF-NEEDS.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# PROOF-NEEDS.md
2+
3+
## Template ABI Cleanup (2026-03-29)
4+
5+
Template ABI removed -- was creating false impression of formal verification.
6+
The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
7+
scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
8+
9+
When this project needs formal ABI verification, create domain-specific Idris2 proofs
10+
following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.

src/interface/abi/Foreign.idr

Lines changed: 0 additions & 210 deletions
This file was deleted.

0 commit comments

Comments
 (0)