Skip to content

Commit 137a49d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add TEST-NEEDS.md and/or PROOF-NEEDS.md from audit
Documents testing and proof gaps identified during batch audit. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 2d59a0d commit 137a49d

2 files changed

Lines changed: 97 additions & 0 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# PROOF-NEEDS.md
2+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
3+
4+
## Current State
5+
6+
- **LOC**: ~17,000
7+
- **Languages**: Rust, Idris2, Zig
8+
- **Existing ABI proofs**: `src/abi/*.idr` (template-level)
9+
- **Dangerous patterns**: None detected in source files
10+
11+
## What Needs Proving
12+
13+
### Core Type System (crates/typell-core/)
14+
- `check.rs` — type checking for the 10-level type system
15+
- `infer.rs` — type inference
16+
- `unify.rs` — unification algorithm
17+
- `proof.rs` (495 lines) — proof generation/checking in Rust
18+
- `linear.rs` — linear type tracking
19+
- `qtt.rs` — quantitative type theory
20+
- `session.rs` — session types
21+
- `effects.rs` — effect system
22+
- Prove: type checking is sound (well-typed programs do not get stuck)
23+
- Prove: type inference is complete (finds principal types when they exist)
24+
- Prove: unification terminates and is most general
25+
26+
### Language Bridges (14 crates)
27+
- Each `typell-*` crate bridges TypeLL to a nextgen language
28+
- Prove: bridge translations preserve typing judgments
29+
- Prove: subtyping relationships are transitive across bridges
30+
31+
### Dimensional Types (crates/typell-core/src/dimensional.rs)
32+
- Physical dimension tracking in types
33+
- Prove: dimensional analysis is consistent (no unit mismatch can pass type checking)
34+
35+
## Recommended Prover
36+
37+
- **Idris2** for the type system metatheory (soundness, completeness)
38+
- **Agda** alternative for the unification/inference proofs (strong equational reasoning)
39+
40+
## Priority
41+
42+
**HIGH** — TypeLL is PanLL's verification kernel. If the type system is unsound, every downstream language that relies on TypeLL levels has unsound guarantees. The 10-level type hierarchy is the central claim of the project and must be formally verified.

‎TEST-NEEDS.md‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# TEST-NEEDS: typell
2+
3+
## Current State
4+
5+
| Category | Count | Details |
6+
|----------|-------|---------|
7+
| **Source modules** | 53 | Rust: typell-core (12: types, error, unify, infer, check, linear, effects, qtt, dimensional, session, proof, lib), typell-eclexia (3), typell-affinescript (3), typell-ephapax (3), typell-wokelang (3), typell-tangle (3), typell-betlang (3), typell-mylang (3), typell-oblibeny (3), typell-jtv (3), typell-phronesis (3), typell-errorlang (3), typell-vql (4) + 3 Idris2 ABI |
8+
| **Unit tests (inline)** | 398 | Distributed across all crates -- types=21, unify=31, proof=14, session=7, dimensional=10, etc. |
9+
| **Integration tests** | 2 files | core_comprehensive_tests.rs (95), vql_bridge_tests.rs (58) |
10+
| **E2E tests** | 0 | None |
11+
| **Benchmarks** | 0 | benches/.gitkeep ONLY |
12+
13+
## What's Missing
14+
15+
### P2P Tests
16+
- [ ] No tests for cross-language bridge correctness (e.g., typell-wokelang checks match wokelang semantics)
17+
- [ ] No tests for bridge interoperability (two language backends against same type)
18+
19+
### E2E Tests (CRITICAL)
20+
- [ ] No test that type-checks a real program through the full pipeline
21+
- [ ] No test for all 10 type system levels (dependent, linear, session, QTT, effects, modal, dimensional, proof, epistemic, tropical)
22+
- [ ] No test for language backend integration with actual language compilers
23+
24+
### Aspect Tests
25+
- [ ] **Security**: Type system = trust boundary; no soundness fuzzing
26+
- [ ] **Performance**: No benchmarks despite being performance-critical type checker
27+
- [ ] **Concurrency**: No parallel type checking tests
28+
- [ ] **Error handling**: No tests for unsatisfiable constraints, infinite unification, cyclic types
29+
30+
### Benchmarks Needed (CRITICAL)
31+
- [ ] **benches/.gitkeep is EMPTY** -- phantom benchmarks
32+
- [ ] Type checking throughput (expressions/second)
33+
- [ ] Unification performance scaling with constraint count
34+
- [ ] QTT resource tracking overhead
35+
- [ ] Session type verification latency
36+
- [ ] Proof checking throughput
37+
38+
### Self-Tests
39+
- [ ] No soundness self-check
40+
- [ ] No regression suite for type system properties
41+
42+
## FLAGGED ISSUES
43+
- **398 inline tests across 13 crates is respectable** -- best inline coverage among non-Julia repos
44+
- **benches/.gitkeep = phantom benchmarks** -- a type checker with no performance measurements
45+
- **13 language backends (eclexia through vql) each have only ~10 inline tests** -- thin coverage per backend
46+
- **0 E2E for a 10-level type system** -- can't verify the type system actually works on real programs
47+
- **core_comprehensive_tests.rs (95 tests) is solid** for the kernel
48+
49+
## Priority: P1 (HIGH) -- inline tests are decent but need E2E, benchmarks, and soundness proofs
50+
51+
## FAKE-FUZZ ALERT
52+
53+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
54+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
55+
- Priority: P2 — creates false impression of fuzz coverage

0 commit comments

Comments
 (0)