Skip to content

Commit f54a765

Browse files
hyperpolymathclaude
andcommitted
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 2c3b2fa commit f54a765

2 files changed

Lines changed: 92 additions & 0 deletions

File tree

PROOF-NEEDS.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# Proof Requirements
2+
3+
## Current state
4+
- ABI exists in `src/interface/abi/Layout.idr`
5+
- **Known gap**: `postulate alignUpProducesAligned` at line 341 — alignment proof is postulated, not proven
6+
- 10K lines of source; 7 Gossamer panels, VeriSimDB backing
7+
8+
## What needs proving
9+
- **Close the postulate**: Replace `postulate alignUpProducesAligned` with an actual proof via `Data.Nat.Factor` or equivalent
10+
- **Server probe safety**: Prove that server health probes do not cause side effects on the target game servers
11+
- **Configuration drift detection**: Prove the drift dashboard correctly identifies all deviations from declared state
12+
- **Access control for admin panels**: Prove panel-level access control prevents unauthorized server operations
13+
14+
## Recommended prover
15+
- **Idris2** — The postulate is already in Idris2; closing it requires a proof about natural number alignment (straightforward with `Data.Nat`)
16+
17+
## Priority
18+
- **MEDIUM** — The postulate is a concrete proof gap that should be easy to close. Server probe safety matters for production game servers but is not as critical as the other HIGH-priority repos.

TEST-NEEDS.md

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
# Test & Benchmark Requirements
2+
3+
## Current State
4+
- Unit tests: NONE
5+
- Integration tests: 2 Zig integration tests (template-level)
6+
- E2E tests: NONE
7+
- Benchmarks: NONE
8+
- panic-attack scan: NEVER RUN (feature dir exists but no report)
9+
10+
## What's Missing
11+
### Point-to-Point (P2P)
12+
13 Zig + 13 Ephapax + 3 Idris2 + 5 JS + 1 ReScript source files with ZERO functional tests:
13+
14+
#### Core (Ephapax — 6 files):
15+
- Types.eph — no tests
16+
- Capabilities.eph — no tests
17+
- Shell.eph — no tests
18+
- Bridge.eph — no tests
19+
- GrooveClient.eph — no tests
20+
21+
#### GUI (Ephapax — 1 file):
22+
- main.eph — no tests
23+
24+
#### Zig (13 files):
25+
- Only 2 template integration tests
26+
27+
#### JavaScript (5 files):
28+
- No tests
29+
30+
#### Idris2 ABI (3 files):
31+
- No verification tests
32+
33+
### End-to-End (E2E)
34+
- Game server lifecycle: discover -> connect -> configure -> monitor -> restart
35+
- Panel system: load panels -> display server status -> interact
36+
- Groove integration: discover services -> negotiate capabilities
37+
- Shell execution: send command -> execute on server -> return output
38+
- Per-game profile: load profile -> apply settings -> verify
39+
- VeriSimDB integration: store server metrics -> query -> dashboard
40+
- Clade system integration: classify servers -> manage taxonomy
41+
42+
### Aspect Tests
43+
- [ ] Security (shell command injection — CRITICAL, server credential handling, Groove auth, capability escalation)
44+
- [ ] Performance (server monitoring poll latency, multi-server dashboard rendering)
45+
- [ ] Concurrency (multiple server management, concurrent shell sessions)
46+
- [ ] Error handling (server unreachable, auth failure, malformed server response)
47+
- [ ] Accessibility (admin panel keyboard navigation, screen reader, color contrast)
48+
49+
### Build & Execution
50+
- [ ] zig build — not verified
51+
- [ ] Ephapax compile — not verified
52+
- [ ] GUI launches — not verified
53+
- [ ] Shell command execution — not verified
54+
- [ ] Self-diagnostic — none
55+
56+
### Benchmarks Needed
57+
- Server status poll frequency vs latency
58+
- Multi-server dashboard rendering time (10, 50, 100 servers)
59+
- Shell command execution roundtrip time
60+
- Groove service discovery latency
61+
62+
### Self-Tests
63+
- [ ] panic-attack assail on own repo
64+
- [ ] Server connectivity self-test
65+
- [ ] Groove handshake self-test
66+
67+
## Priority
68+
- **HIGH** — Game server administration tool (13 Zig + 13 Ephapax + 5 JS files) with ZERO functional tests. The Shell.eph module that executes commands on remote servers is a massive security surface that is completely untested. Command injection testing is non-negotiable for any tool that runs shell commands on game servers.
69+
70+
## FAKE-FUZZ ALERT
71+
72+
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
73+
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
74+
- Priority: P2 — creates false impression of fuzz coverage

0 commit comments

Comments
 (0)