Skip to content

Commit 9a1c8fe

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 cd8b894 commit 9a1c8fe

5 files changed

Lines changed: 111 additions & 626 deletions

File tree

PROOF-NEEDS.md

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# Proof Requirements
2+
3+
## Current state
4+
- `src/abi/Types.idr` (232 lines) — Configuration flow types
5+
- `src/abi/Layout.idr` (177 lines) — Memory layout
6+
- `src/abi/Foreign.idr` (217 lines) — FFI declarations
7+
- No dangerous patterns in ABI layer
8+
- Claims: "type-safe", "memory-safe" (Rust)
9+
10+
## What needs proving
11+
- **Configuration DAG acyclicity**: Prove the configuration dependency graph is always a DAG (no circular dependencies that cause infinite loops)
12+
- **Merge conflict resolution determinism**: Prove that configuration merges produce deterministic results regardless of evaluation order
13+
- **Rollback safety**: Prove that configuration rollback restores the exact previous state (no partial rollback)
14+
- **Schema validation completeness**: Prove that all configuration values passing validation conform to their declared schema (no type confusion)
15+
16+
## Recommended prover
17+
- **Idris2** — Dependent types naturally express DAG properties and schema conformance; already used for ABI
18+
19+
## Priority
20+
- **MEDIUM** — Configuration errors can cascade to downstream services. The type-safety claim should be backed by proofs, especially for merge determinism and rollback correctness.
21+
22+
## Template ABI Cleanup (2026-03-29)
23+
24+
Template ABI removed -- was creating false impression of formal verification.
25+
The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
26+
scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.

TEST-NEEDS.md

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
# Test & Benchmark Requirements
2+
3+
## Current State
4+
- Unit tests: BUILD FAILS — cargo test cannot complete (1 compilation error + 22 warnings)
5+
- Integration tests: 1 Zig integration test (template)
6+
- E2E tests: NONE
7+
- Benchmarks: NONE
8+
- panic-attack scan: NEVER RUN
9+
10+
## What's Missing
11+
### Point-to-Point (P2P)
12+
45 Rust source files with 22 files containing #[cfg(test)] / #[test] — but none can run because the build is broken.
13+
14+
#### Modules (organized by subsystem):
15+
**Analyzer (5 files):**
16+
- complexity.rs — has inline tests (BLOCKED)
17+
- config_detector.rs — has inline tests (BLOCKED)
18+
- patterns.rs — has inline tests (BLOCKED)
19+
- recommender.rs — likely has tests (BLOCKED)
20+
- mod.rs
21+
22+
**Cache (3 files):**
23+
- filesystem.rs — needs tests
24+
- hash.rs — needs tests
25+
- mod.rs
26+
27+
**CLI (8 files):**
28+
- analyze.rs, cache.rs, graph.rs, init.rs, run.rs, validate.rs, watch.rs, rsr.rs
29+
- CLI commands need integration tests
30+
31+
**Errors (3 files):**
32+
- educational.rs — error message quality tests
33+
- recovery.rs — recovery path tests
34+
- mod.rs
35+
36+
**Executors (4 files):**
37+
- cue.rs, nickel.rs, shell.rs — executor correctness tests
38+
- mod.rs
39+
40+
**Pipeline (5 files):**
41+
- dag.rs — DAG construction and cycle detection tests
42+
- definition.rs — pipeline definition parsing tests
43+
- executor.rs — pipeline execution tests
44+
- validation.rs — **THIS IS WHERE THE BUILD ERROR IS** (unused field `flags`, `shell`)
45+
- mod.rs
46+
47+
**RSR (multiple files):**
48+
- badges.rs + others — RSR generation tests
49+
50+
### End-to-End (E2E)
51+
- Full pipeline: define -> validate -> execute -> cache results
52+
- CLI: init project -> define pipeline -> run -> watch for changes
53+
- Analyzer: scan project -> detect configs -> recommend pipeline
54+
- Cache: execute -> cache -> re-execute (cache hit)
55+
- Graph generation and visualization
56+
- Error recovery: introduce error -> recover -> resume
57+
58+
### Aspect Tests
59+
- [ ] Security (shell executor command injection, path traversal in cache, untrusted pipeline definitions)
60+
- [ ] Performance (DAG resolution on large pipelines, cache lookup speed)
61+
- [ ] Concurrency (parallel pipeline stages, file watching races)
62+
- [ ] Error handling (executor failures, missing tools, invalid configs)
63+
- [ ] Accessibility (N/A — CLI tool)
64+
65+
### Build & Execution
66+
- [ ] cargo build — **FAILS** (compilation error in pipeline/validation.rs)
67+
- [ ] cargo test — **FAILS** (blocked by build error)
68+
- [ ] Binary runs — **BLOCKED**
69+
- [ ] CLI --help — **BLOCKED**
70+
- [ ] Self-diagnostic — none
71+
72+
### Benchmarks Needed
73+
- Pipeline execution throughput
74+
- DAG resolution for complex dependency graphs
75+
- Cache hit/miss ratio under typical workloads
76+
- File watching latency
77+
- Analyzer scan speed on large projects
78+
79+
### Self-Tests
80+
- [ ] panic-attack assail on own repo
81+
- [ ] Fix compilation error first (pipeline/validation.rs)
82+
- [ ] Built-in doctor/check command (if applicable)
83+
84+
## Priority
85+
- **HIGH** — 45 Rust source files that CANNOT EVEN COMPILE. The build is broken. ~20 files have inline test modules but none can run. Fix the compilation error in pipeline/validation.rs first, then verify test coverage. A configuration flow tool with shell execution needs security testing as a top priority.

src/abi/Foreign.idr

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

0 commit comments

Comments
 (0)