# Proof Specifications — LLM Handoff Directory
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
<!-- Generated: 2026-04-04 -->

## Purpose

This directory contains **executable proof specifications** for all 292 repos in the hyperpolymath estate. Each spec is designed so that any coding LLM with proof-checker tooling (Gemini + MCPs to `coqc`/`lean`/`agda`/`idris2`, or similar) can pick up one file and produce verified proofs independently.

## Directory Structure

```
proof-specs/
├── README.md                       (this file)
├── SPEC-TEMPLATE.md                (template for new specs)
├── T1-critical/                    (~25 repos — safety-critical)
│   ├── echidna.md
│   ├── verisimdb.md
│   ├── hypatia.md
│   └── ...
├── T2-high/                        (~20 repos — core infra)
│   └── ...
├── T3-standard/                    (~210 repos — ABI + bespoke)
│   └── ...
└── T4-light/                       (~20 repos — template only)
    └── ...
```

T5 (exempt) repos are not listed here — no proofs needed.

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

## How to Execute a Spec (for LLMs)

You have been given ONE `.md` spec file from this directory. Follow it exactly:

1. **Read the entire spec file** before starting. Note the target repo, prover(s), and total theorem count.
2. **Navigate to the target repo** at the path given in the spec.
3. **Create the proof files** at the exact paths specified in the spec.
4. **Write each theorem** matching the signature/statement given.
5. **NEVER use banned patterns**: `believe_me`, `assert_total`, `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, `Obj.magic`. Each spec repeats this reminder.
6. **Run the verification command** given at the end of the spec. All proofs MUST check successfully.
7. **Update the repo's `PROOF-STATUS.md`** with completed rows.
8. **Commit** with message: `proof: complete <spec-name> proofs (N/M theorems)`

## Spec Format

Every spec contains:

- **Header**: repo name, tier, proof count, prover(s)
- **Context**: what the repo does, source file tree
- **Existing proofs**: what is already verified (do not redo)
- **Theorems**: numbered list with:
  - Theorem ID (e.g., `E1`, `V3`)
  - Target file (where proof lives)
  - Source file + line range (what code is being verified)
  - Prover and file extension
  - Statement (formal or semi-formal)
  - Expected signature (typed skeleton)
  - Hints and obligations
- **Verification commands**: shell commands to check all proofs
- **Banned patterns**: reminder
- **Handoff checklist**: final verification steps

## Final Coverage

| Tier | Per-repo specs | Archetype docs | Total files |
|------|----------------|----------------|-------------|
| T1 Critical | 23 | — | 23 |
| T2 High | 17 | — | 17 |
| T3 Standard | 228 | 9 archetypes | 237 |
| T4 Light | — | 1 README (template applies) | 1 |
| **Total** | **268** | **10** | **278** |

**T1/T2 specs** (40 repos): Deep — specific theorems with signatures, hints, obligations, source file references.
**T3 specs** (228 repos): Stub — references archetype + lists repo-specific items. Archetype provides the common proof pattern.
**T4 specs** (~17 repos): Template-only — copy ABI proofs from rsr-template-repo.

## Parallelism Strategy

Multiple LLMs can work on different spec files simultaneously without conflict, because:
- Each spec targets one repo
- Each spec lists files that do not overlap with other specs
- All specs follow the same protocol (banned patterns, verification commands)

Suggested allocation:
- Assign T1 specs to the strongest LLMs (critical safety proofs)
- Assign T2 specs to mid-tier LLMs
- Assign T3 specs to any LLM with proof-checker MCP access
- T4 specs can be auto-generated from the template

## Tracking Progress

Each spec file has a checkbox table at the top. Update as you go:

```
| # | Theorem | Status | Verified |
|---|---------|--------|----------|
| 1 | E1 Confidence lattice | [x] Done | 2026-04-05 |
| 2 | E2 Axiom completeness | [ ] Pending | — |
```

## Dependencies Between Specs

Some proofs depend on others. Each spec lists upstream dependencies. Execute in this order:

1. **`proven` repo** first (foundational Idris2 library)
2. **`rsr-template-repo` ABI proofs** second (baseline for all repos)
3. **T1 repos** third (each self-contained)
4. **T2/T3 repos** any time after their ABI dependencies

## Questions / Clarifications

If a spec is unclear or a theorem cannot be proven as stated:
1. Document the blocker in the spec file (add a `Blockers` section)
2. Do NOT invent or weaken the theorem
3. Mark the status as `Blocked — needs human review`
4. Move on to the next theorem

## References

- Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.md`
- Template repo: `/var/mnt/eclipse/repos/rsr-template-repo/`
- Proven library: `/var/mnt/eclipse/repos/proven/`
- Hyperpolymath standards: `~/.claude/CLAUDE.md`
