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>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -0,0 +1,38 @@
+# PROOF-NEEDS.md
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+
+## Current State
+
+- **LOC**: ~3,610
+- **Languages**: Rust, Julia, Idris2, Zig
+- **Existing ABI proofs**: `src/abi/*.idr` (template-level)
+- **Dangerous patterns**: None detected
+
+## What Needs Proving
+
+### VAE Dataset Normalization (Julia core)
+- `contrastive_model.jl`, `julia_utils.jl` — data processing pipeline
+- Prove: normalization is invertible (or document when it is lossy)
+- Prove: contrastive model training preserves dataset statistical properties
+
+### Metadata Handling (src/metadata.rs)
+- Dataset metadata management
+- Prove: metadata correctly describes the normalized dataset
+
+### Fuzz Target (fuzz/fuzz_targets/fuzz_input.rs)
+- Fuzzing exists — formal proofs of normalization properties would be stronger
+
+## Recommended Prover
+
+- **Lean4** with Mathlib for numerical/statistical properties
+- **Idris2** for ABI layer and metadata invariants
+
+## Priority
+
+**LOW** — Dataset preprocessing tool. Normalization correctness matters for ML pipeline reproducibility but is not safety-critical. The small codebase limits the scope of potential errors.
+
+## Template ABI Cleanup (2026-03-29)
+
+Template ABI removed -- was creating false impression of formal verification.
+The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
+scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.

TEST-NEEDS.md

@@ -0,0 +1,49 @@
+# TEST-NEEDS: zerostep
+
+## Current State
+
+| Category | Count | Details |
+|----------|-------|---------|
+| **Source modules** | 7 | Rust (main, metadata), Julia (contrastive_model, julia_utils), 3 Idris2 ABI |
+| **Unit tests** | 5 | test/runtests.jl (5 @test) |
+| **Integration tests** | 0 | None |
+| **E2E tests** | 0 | None |
+| **Benchmarks** | 0 | None |
+| **Fuzz tests** | 1 | fuzz/fuzz_targets/fuzz_input.rs |
+
+## What's Missing
+
+### P2P Tests
+- [ ] No tests for Rust <-> Julia interop
+- [ ] No tests for contrastive model feeding into metadata processing
+
+### E2E Tests
+- [ ] No test running zerostep binary end-to-end
+- [ ] No test for the contrastive learning pipeline
+
+### Aspect Tests
+- [ ] **Security**: No input validation tests
+- [ ] **Performance**: ML contrastive model with 0 benchmarks
+- [ ] **Concurrency**: No tests for parallel model execution
+- [ ] **Error handling**: No tests for malformed input data, model failures
+
+### Build & Execution
+- [ ] No Rust compilation test
+- [ ] No Idris2 ABI compilation test
+- [ ] Nickel config (config.ncl) untested
+
+### Benchmarks Needed
+- [ ] Contrastive model training time
+- [ ] Inference latency
+- [ ] Metadata processing throughput
+
+### Self-Tests
+- [ ] No self-diagnostic mode
+
+## FLAGGED ISSUES
+- **5 @test for 7 source modules** = barely tested
+- **ML project with 0 benchmarks** -- performance is the entire point
+- **Fuzz target exists** (fuzz_input.rs) -- rare positive
+- **Julia model code with no Julia-specific tests** for the model itself
+
+## Priority: P1 (HIGH)