Skip to content

PROOF-NEEDS.adoc

Latest commit

 

History

History
46 lines (31 loc) · 1.36 KB

PROOF-NEEDS.adoc

File metadata and controls

46 lines (31 loc) · 1.36 KB
Raw

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.