# PROOF-NEEDS.md
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

## 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.
