Skip to content

PROOF-NEEDS.md

Latest commit

 

History

History
38 lines (26 loc) · 1.4 KB

PROOF-NEEDS.md

File metadata and controls

38 lines (26 loc) · 1.4 KB

PROOF-NEEDS.md

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.