Skip to content

Commit fe49bfa

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 0835a11 commit fe49bfa

5 files changed

Lines changed: 36 additions & 629 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`.

TEST-NEEDS.md

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# TEST-NEEDS: Cladistics.jl
2+
3+
## Current State
4+
5+
| Category | Count | Details |
6+
|----------|-------|---------|
7+
| **Source modules** | 2 | 1,197 lines |
8+
| **Test files** | 1 | 606 lines, 161 @test/@testset |
9+
| **Benchmarks** | 0 | None |
10+
11+
## What's Missing
12+
13+
- [ ] **Performance**: No benchmarks for phylogenetic tree computation
14+
- [ ] **Error handling**: No tests for malformed taxa, cyclic trees
15+
16+
## FLAGGED ISSUES
17+
- **161 tests for 2 modules = 80.5 tests/module** -- excellent
18+
- **0 benchmarks** -- tree algorithms should have scaling benchmarks
19+
20+
## Priority: P3 (LOW)
21+
22+
## FAKE-FUZZ ALERT
23+
24+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
25+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
26+
- Priority: P2 — creates false impression of fuzz coverage

src/abi/Foreign.idr

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

0 commit comments

Comments
 (0)