PROOF-NEEDS.adoc

Proof Requirements — PSEUDOSCRIPT

Proof Tier

Tier: T3 — Standard

Proof Categories

Code	Meaning	Applies?
TP	Typing Proofs (type soundness, type safety)	Yes
INV	Invariant Proofs (state machines, monotonicity, bounds)
SEC	Security Proofs (crypto, injection freedom, access control)
CONC	Concurrency Proofs (linearizability, deadlock freedom)
ALG	Algorithm Proofs (termination, correctness, bounds)
ABI	ABI/FFI Proofs (memory layout, pointer safety, platform compat)	Yes
DOM	Domain-Specific Proofs (bespoke to this project)

Mandatory Proofs (All RSR Repos)

These proofs come from the rsr-template-repo and MUST be present in every repo:

ABI/FFI Boundary Proofs (Idris2)

#	Proof	Status	File
ABI-1	Non-null pointer proofs (So (ptr /= 0))	Needed	verification/proofs/idris2/ABI/Pointers.idr
ABI-2	Memory layout correctness (HasSize, HasAlignment)	Needed	verification/proofs/idris2/ABI/Layout.idr
ABI-3	Platform type size proofs (per platform)	Needed	verification/proofs/idris2/ABI/Platform.idr
ABI-4	FFI function return type proofs	Needed	verification/proofs/idris2/ABI/Foreign.idr
ABI-5	C ABI compliance (CABICompliant, FieldsAligned)	Needed	verification/proofs/idris2/ABI/Compliance.idr

Typing Proofs (Prover Varies)

#	Proof	Status	File
TP-1	Core data type well-formedness	Needed	verification/proofs/idris2/Types.idr
TP-2	Public API type safety (exported functions)	Needed	verification/proofs/lean4/ApiTypes.lean

Project-Specific Proofs

#	Proof Needed	Category	Prover	Priority	File(s)

Dangerous Patterns (BANNED)

The following MUST NOT appear anywhere in proof files:

Pattern	Language	Meaning
believe_me	Idris2	Unsafe cast / trust-me
assert_total	Idris2	Skip totality check
postulate	Idris2/Agda	Unproven axiom
sorry	Lean4	Incomplete proof
Admitted	Coq	Incomplete proof
unsafeCoerce	Haskell	Unsafe type cast
Obj.magic	OCaml/ReScript	Unsafe type cast
unsafe (unaudited)	Rust	Unsafe block without safety comment

CI will reject any PR introducing these patterns (enforced by panic-attack assail).

Prover Selection Guide

Use Case	Recommended Prover	Why
ABI/FFI boundaries	Idris2	Dependent types model layouts precisely
Type system proofs	Coq or Lean4	Mature proof assistants for metatheory
Algebraic properties	Lean4	Good mathlib support
Inductive/coinductive	Agda	Native support for (co)induction
Distributed systems	TLA+	Model checking for protocols
Numerical properties	Isabelle	Strong real analysis library

Proof File Locations

verification/proofs/
├── idris2/          # Idris2 proofs (ABI, dependent types)
│   ├── ABI/         # ABI-specific proofs
│   └── *.idr        # Project-specific Idris2 proofs
├── lean4/           # Lean4 proofs (algebra, lattices)
│   └── *.lean
├── agda/            # Agda proofs (induction, metatheory)
│   └── *.agda
├── coq/             # Coq proofs (type systems, compilation)
│   └── *.v
└── tlaplus/         # TLA+ specs (distributed protocols)
    └── *.tla

References

• Master list: ~/Desktop/PROOF-REQUIREMENTS-MASTER.md

• Proof status tracking: PROOF-STATUS.md (this repo)

• Proven library: proven repo (Idris2 verified foundations)

• Template: rsr-template-repo/PROOF-NEEDS.md