Skip to content

Commit f8bedb8

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 6812fbc commit f8bedb8

2 files changed

Lines changed: 101 additions & 0 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
# PROOF-NEEDS.md
2+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
3+
4+
## Current State
5+
6+
- **LOC**: ~57,650
7+
- **Languages**: Rust, ReScript, Agda, Idris2, Zig
8+
- **Existing ABI proofs**: `src/abi/*.idr` plus extensive Agda proof suite (9 files in `proofs/agda/`)
9+
- **Dangerous patterns**:
10+
- `proofs/agda/FileContentOperations.agda`: 5 `postulate`
11+
- `proofs/agda/FilesystemModel.agda`: 1 `postulate`
12+
- `proofs/agda/RMOOperations.agda`: 1 `postulate`
13+
- `impl/mcp/src/Server.res`: 20+ `Obj.magic` in MCP tool handlers
14+
15+
## What Needs Proving
16+
17+
### FileContentOperations Postulates (5)
18+
- These are in the core filesystem proof — content operations are critical for shell correctness
19+
- Audit each postulate: are they about byte-level I/O (acceptable axiom) or about logical properties (should be proven)?
20+
21+
### FilesystemModel Postulate (1)
22+
- Foundation postulate — if this is wrong, all downstream proofs are unsound
23+
- Should be the highest priority to eliminate or justify
24+
25+
### RMOOperations Postulate (1)
26+
- Reversible Mutable Operations — the core innovation of valence-shell
27+
- Any unproven claim about reversibility undermines the entire system guarantee
28+
29+
### MCP Server Obj.magic (impl/mcp/src/Server.res)
30+
- Every filesystem operation handler uses `Obj.magic` for JSON result construction
31+
- `makeToolResult` and `makeJsonResult` return type-erased values
32+
- Prove: MCP tool responses conform to MCP protocol schema
33+
34+
### Rust FFI Verification (ffi/rust/)
35+
- `ffi/rust/src/preconditions.rs`, `verification.rs`, `rmo.rs` — safety-critical FFI
36+
- Precondition checking and operation verification should have formal backing
37+
38+
## Recommended Prover
39+
40+
- **Agda** (already in use — eliminate remaining 7 postulates)
41+
- **Idris2** for ABI layer and Rust FFI interface contracts
42+
43+
## Priority
44+
45+
**HIGH** — Filesystem shell with formal reversibility guarantees. The 7 postulates in the Agda proofs are close to full verification. Eliminating them would make this a genuinely formally verified filesystem tool.

‎TEST-NEEDS.md‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# TEST-NEEDS: valence-shell
2+
3+
## Current State
4+
5+
| Category | Count | Details |
6+
|----------|-------|---------|
7+
| **Source modules** | 77 | Rust CLI (~32: parser, commands, arith, glob, job, pager, etc.), Zig impl (~12: root, audit, daemon, demo, path, preconditions, prover, etc.), Elixir (2: application, NIF), 3 Idris2 ABI |
8+
| **Unit tests (Rust inline)** | ~250+ | parser=112, commands=27, state=34, posix_builtins=18, quotes=17, arith=13, external=13, functions=13, glob=8, job=8, highlighter=6, etc. |
9+
| **Integration tests (Rust)** | 11 files | parameter_expansion=67, extended_test=55, integration=35, correspondence=35, function_and_script=24, property_correspondence=19, property=28, lean4_proptest=16, security=15, stress=11, integration_tests=10 |
10+
| **Elixir tests** | 1 file | vsh_test.exs (13 assertions) |
11+
| **Zig tests** | ~21 | Inline test functions across src files |
12+
| **Shell integration test** | 1 | integration_test.sh (70 assertions) |
13+
| **E2E tests** | 0 | None |
14+
| **Benchmarks** | 0 | None |
15+
16+
## What's Missing
17+
18+
### P2P Tests
19+
- [ ] No tests for Rust CLI <-> Zig backend <-> Elixir NIF pipeline
20+
- [ ] No tests for Lean4 prover integration in practice (only proptest correspondence)
21+
22+
### E2E Tests
23+
- [ ] No test running valence-shell as an actual shell (interactive session)
24+
- [ ] No POSIX compliance test suite
25+
- [ ] No test for script execution end-to-end
26+
27+
### Aspect Tests
28+
- [ ] **Security**: security_tests.rs exists (15 tests) -- good start but insufficient for a shell (needs injection, escape, privilege escalation tests)
29+
- [ ] **Performance**: No benchmarks for shell startup time, command dispatch latency
30+
- [ ] **Concurrency**: No tests for job control with concurrent processes
31+
- [ ] **Error handling**: stress_tests.rs exists (11 tests) -- needs expansion
32+
33+
### Benchmarks Needed
34+
- [ ] Shell startup time
35+
- [ ] Command parsing throughput
36+
- [ ] Pipeline execution overhead vs bash/zsh
37+
- [ ] Glob expansion performance (1000/10000 files)
38+
39+
### Self-Tests
40+
- [ ] No `valence-shell --self-test` mode
41+
- [ ] No POSIX conformance self-check
42+
43+
## FLAGGED ISSUES
44+
- **Best tested repo in the scan** -- 250+ inline + 315+ integration tests across 3 languages
45+
- **Property-based testing exists** (proptest, lean4 correspondence) -- rare and excellent
46+
- **No benchmarks at all for a SHELL** -- startup time and command latency are critical
47+
- **Elixir layer has only 13 tests** compared to 300+ Rust tests
48+
- **Zig layer has only ~21 inline tests for 12 modules** -- undertested
49+
50+
## Priority: P2 (MEDIUM) -- strong test foundation, needs benchmarks and E2E
51+
52+
## FAKE-FUZZ ALERT
53+
54+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
55+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
56+
- Priority: P2 — creates false impression of fuzz coverage

0 commit comments

Comments
 (0)