Skip to content

Commit b445d9f

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 6f53425 commit b445d9f

5 files changed

Lines changed: 46 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`.

TEST-NEEDS.md

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# TEST-NEEDS: InvestigativeJournalist.jl
2+
3+
## Current State
4+
5+
| Category | Count | Details |
6+
|----------|-------|---------|
7+
| **Source modules** | 19 | 1,525 lines |
8+
| **Test files** | 1 | 488 lines, 222 @test/@testset |
9+
| **Benchmarks** | 0 | None |
10+
| **E2E tests** | 0 | None |
11+
12+
## What's Missing
13+
14+
### E2E Tests
15+
- [ ] No end-to-end investigation pipeline test
16+
17+
### Aspect Tests
18+
- [ ] **Security**: Investigation tool -- needs data handling security tests
19+
- [ ] **Performance**: No benchmarks for data analysis throughput
20+
- [ ] **Error handling**: No tests for corrupt data sources, API failures
21+
22+
### Benchmarks Needed
23+
- [ ] Data source ingestion throughput
24+
- [ ] Analysis pipeline latency
25+
26+
## FLAGGED ISSUES
27+
- **222 tests for 19 modules = 11.7 tests/module** -- adequate
28+
- **Single test file for 19 modules** -- should be split
29+
30+
## Priority: P2 (MEDIUM)
31+
32+
## FAKE-FUZZ ALERT
33+
34+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
35+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
36+
- Priority: P2 — creates false impression of fuzz coverage

src/abi/Foreign.idr

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

0 commit comments

Comments
 (0)