Skip to content

PROOF-NEEDS.md

Latest commit

 

History

History
53 lines (39 loc) · 2.53 KB

PROOF-NEEDS.md

File metadata and controls

53 lines (39 loc) · 2.53 KB

PROOF-NEEDS.md

Current State

  • LOC: ~139,200 (monorepo with many sub-standards)
  • Languages: ReScript, Idris2, Agda, Rust, Haskell, Zig, Nickel
  • Existing ABI proofs: Multiple src/abi/*.idr across sub-projects (a2ml, axel-protocol, avow-protocol, lol, etc.)
  • Existing verification: lol/proofs/theories/information_theory.agda with A2ML Idris2 proofs in a2ml/src/A2ML/Proofs.idr
  • Dangerous patterns:
    • lol/proofs/theories/information_theory.agda: 6 postulate (information theory axioms)
    • axel-protocol/src/Tea.res and AxelApp.res: Obj.magic for DOM operations
    • lol/src/abi/Locale.idr: mentions avoiding believe_me (good practice)

What Needs Proving

LOL Information Theory Postulates (6)

  • information_theory.agda has 6 postulated axioms about entropy, mutual information, etc.
  • Audit: which are genuine mathematical axioms vs. provable lemmas?
  • Entropy non-negativity and chain rule should be constructively provable

A2ML Parser Proofs (a2ml/src/A2ML/)

  • Proofs.idr exists — audit completeness
  • Parser.idr, TypedCore.idr, Surface.idr — prove parser/type-system correspondence
  • A2ML is a markup format standard — parser correctness ensures documents are faithfully processed

Avow Protocol Consent Proofs

  • avow-protocol/avow-lib/src/abi/Consent.idr, Unsubscribe.idr
  • Consent management is GDPR-relevant — prove consent state transitions are correct
  • Prove: unsubscribe always terminates in a non-consented state

Axel Protocol Obj.magic

  • axel-protocol/src/Tea.res — 8+ Obj.magic calls for DOM rendering
  • Lower priority than the protocol specification proofs

Groove Protocol Reference

  • groove-protocol/reference/groove-proxy/GrooveProxy.idr — Idris2 reference implementation
  • Prove: proxy faithfully implements the Groove protocol specification

Recommended Prover

  • Agda for information theory (extend existing proofs, eliminate postulates)
  • Idris2 for A2ML, Avow, Groove protocol correctness (already in use)

Priority

MEDIUM — Standards monorepo. The LOL information theory postulates and Avow consent proofs are the highest-value targets. A2ML proofs already exist and need completion audit.

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.