Skip to content

Commit a10bed3

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 af1a53e commit a10bed3

File tree

90 files changed

+92
-18085
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

90 files changed

+92
-18085
lines changed

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: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
# Test & Benchmark Requirements
2+
3+
## Current State
4+
- Unit tests: ~5 Rust test files + ~4 TS test files + ~54 Zig test files — partial coverage
5+
- Integration tests: partial (some Zig integration tests across ecosystem packages)
6+
- E2E tests: NONE
7+
- Benchmarks: ~738 benchmark files (mostly V-lang ecosystem benchmarks)
8+
- panic-attack scan: NEVER RUN
9+
10+
## What's Missing
11+
### Point-to-Point (P2P)
12+
This is a massive monorepo (29+ sub-ecosystems) with extreme variation in test coverage:
13+
14+
**Source file counts:**
15+
- ReScript: 3,446 files — likely bulk of code, ZERO test files identified
16+
- Julia: 635 files — ZERO test files identified
17+
- Idris2: 323 files — ZERO test files identified
18+
- V: 201 files — ZERO dedicated test files (benchmarks exist)
19+
- Zig: 180 files — 54 test files (BEST coverage ratio)
20+
- Rust: 90 files — 5 test files
21+
- Haskell: 77 files — ZERO test files
22+
- Elixir: 54 files — ZERO test files
23+
- JavaScript: 557 files — ZERO test files
24+
- TypeScript: 25 files — 4 test files
25+
- Shell: 300 files — ZERO test files
26+
27+
#### Sub-ecosystems with tests:
28+
- zig-ecosystem/ — 54 Zig test files (reasonable for 180 source files)
29+
- deno-ecosystem/ — 4 TS test files (inadequate for ecosystem size)
30+
- Some Rust components — 5 test files
31+
32+
#### Sub-ecosystems with ZERO tests:
33+
- **rescript-ecosystem/** (3,446 files) — completely untested
34+
- **julia-ecosystem/** (635 files) — completely untested
35+
- **idris2-ecosystem/** (323 files) — completely untested
36+
- **v-ecosystem/** (201 files) — benchmarks only, no correctness tests
37+
- **haskell ecosystem** (77 files) — completely untested
38+
- **ada-ecosystem/** — completely untested
39+
- **coq-ecosystem/** — no test files found
40+
- **well-known-ecosystem/** — no test files found
41+
- **package-publishers/** — no test files found
42+
- **techstack-enforcer/** — no test files found
43+
44+
### End-to-End (E2E)
45+
- Ecosystem package build and test cycle per language
46+
- Cross-ecosystem dependency resolution
47+
- Package publishing workflow per ecosystem
48+
- Satellite submodule synchronization
49+
- Tool version enforcement
50+
51+
### Aspect Tests
52+
- [ ] Security (package supply chain, dependency confusion, malicious packages)
53+
- [ ] Performance (build time per ecosystem, package resolution speed)
54+
- [ ] Concurrency (parallel builds across ecosystems)
55+
- [ ] Error handling (missing tools, version conflicts, broken satellites)
56+
- [ ] Accessibility (N/A)
57+
58+
### Build & Execution
59+
- [ ] Per-ecosystem builds — not systematically verified
60+
- [ ] Satellite submodule integrity — not verified
61+
- [ ] Package publishing dry-run — not verified
62+
- [ ] Self-diagnostic — none
63+
64+
### Benchmarks Needed
65+
- Per-ecosystem build times
66+
- Package resolution performance
67+
- Cross-ecosystem integration latency
68+
- Verify 738 existing benchmark files actually run (likely V-lang benchmarks)
69+
70+
### Self-Tests
71+
- [ ] panic-attack assail on own repo
72+
- [ ] Per-ecosystem health check
73+
74+
## Priority
75+
- **HIGH** — Staggeringly large monorepo (3,446 ReScript + 635 Julia + 557 JS + 323 Idris2 + 300 Shell + 201 V + 180 Zig + 90 Rust + 77 Haskell + 54 Elixir files). The ReScript ecosystem alone has 3,446 source files with ZERO tests. Only the Zig ecosystem has reasonable test coverage. The 738 "benchmark" files are likely V-lang ecosystem benchmarks, not project-level performance tests.
76+
77+
## FAKE-FUZZ ALERT
78+
79+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
80+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
81+
- Priority: P2 — creates false impression of fuzz coverage

ada-ecosystem/ada-loom-registry/src/abi/Foreign.idr

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

0 commit comments

Comments
 (0)