Remove obsolete proof campaigns and isolate the direct guarantee core

.github/workflows/prove.yml

@@ -14,14 +14,7 @@ jobs:
         with:
           build: false
           use-mathlib-cache: true
-      # The P-SUBMIT-1 / P-DRAIN-1 / P-CONTROL-1 bytecode parents are discharged
-      # by native_decide, which runs the compiled EVMYulLean interpreter; it needs
-      # the keccak/sha2 FFI as shared objects before any Eip8282 module compiles.
-      - name: Build EVMYulLean FFI dynlibs
-        run: lake build EvmYul.FFI.ffi:dynlib
-      - name: Build
-        run: lake build
-      - name: Kill-lines
-        run: lake build Eip8282.Tests.Mutants Eip8282.Tests.PSubmit1Mutant Eip8282.Tests.PDrain1Mutant Eip8282.Tests.PControl1Mutant
-      - name: Audit metadata
-        run: python3 scripts/audit_metadata.py
+      # Full check keeps candidate proofs and every regression in CI while
+      # `make prove` is the smaller registered-correctness build for auditors.
+      - name: Core, candidates, kill-lines and metadata
+        run: make check

.gitignore

@@ -9,3 +9,4 @@ build/
 __pycache__/
 *.pyc
 .DS_Store
+.context/

AGENTS.md

@@ -1,33 +1,25 @@
 # Agent instructions
 
-This repository is Lean 4.31 evidence for three EIP-8282 predeploy guarantees
-(P-SUBMIT-1, P-DRAIN-1, P-CONTROL-1). Lean theorem statements are authoritative.
-`audit/guarantees.yaml` classifies them and must not overclaim.
+This repository contains Lean 4.31 evidence for three EIP-8282 predeploy
+guarantees: P-SUBMIT-1, P-DRAIN-1 and P-CONTROL-1. Lean statements are
+authoritative; `audit/guarantees.yaml` must describe their actual scope.
 
 ## Working in this repository
 
-- Read `audit/DIRECT-CLOSURE.md` before writing proofs. It is the current
-  clause-level evidence map. The superseded campaign documents live under
-  `audit/history/`.
-- Environment: `elan` + toolchain in `lean-toolchain` (4.31.0). Always
-  `lake build EvmYul.FFI.ffi:dynlib` before compiling Eip8282 modules.
-- Verify with `make prove` and the relevant kill-line module. Run
-  `python3 scripts/audit_metadata.py` before opening a PR.
-- Do not add more finite `native_decide` traces as a substitute for `∀`.
-  Wave 5 (P-CONTROL-1 nonempty) and Wave 6 (P-SUBMIT-1 underpay + second
-  image; P-DRAIN-1 more stale slots) already landed on `main` at `85dab78`.
-- Keep existing kill-lines. A new parent that a one-byte mutant cannot
-  refute is not load-bearing.
-- No `sorry`. No project `axiom`. `native_decide` only for finite jumpdest
-  tables in `Eip8282/Audit/Jumpdests.lean` if still forced by `D_J_aux`.
-- Do not edit sibling guarantee files from a claim worker. Integrators only
-  edit parent theorems, `Eip8282.lean`, `Trust.lean`, YAML, README.
-- Do not merge the three campaign PRs to `main`. Humans review them in order
-  P-SUBMIT-1 → P-CONTROL-1 → P-DRAIN-1.
-
-## Local prove
-
-```bash
-lake build EvmYul.FFI.ffi:dynlib
-make prove
-```
+- Read `audit/DIRECT-CLOSURE.md` for the current clause-level evidence map.
+- Use the toolchain in `lean-toolchain` and preserve the normative and interpreter
+  pins unless the task explicitly changes them.
+- Build `EvmYul.FFI.ffi:dynlib` before compiling project modules. `make prove`
+  builds registered correctness; `make check` validates the complete delivery.
+- Run metadata and library-partition checks before opening or updating a PR.
+- No `sorry` or project `axiom`. Do not add finite `native_decide` traces as a
+  replacement for universal proofs. Existing native receipts are confined to
+  the disclosed mutation evidence; correctness must use standard Lean axioms.
+- Keep the six registered same-predicate mutation refutations load-bearing.
+  Preserve the resource-assumption derivation and explicit protocol limits.
+- Use an isolated worktree and private mutable build cache for concurrent work.
+  Keep one heavy build on this Mac. Do not touch unrelated work or live caches.
+- Keep only material needed for current proofs, regressions, source provenance,
+  or reproduction. Git preserves superseded campaign history. Document the
+  reason for retaining historical material and verify references before deletion.
+- Do not merge a PR unless the user authorizes that merge.

Eip8282.lean

@@ -1,35 +1,5 @@
-import Eip8282.Audit.Bytecode
-import Eip8282.Audit.EvmRunner
-import Eip8282.Audit.Guarantees.Registry
-import Eip8282.Audit.Guarantees.PSubmit1
-import Eip8282.Audit.Guarantees.PSubmit1.Revert
-import Eip8282.Audit.Guarantees.PSubmit1.Append
-import Eip8282.Audit.Guarantees.PSubmit1.Fee
-import Eip8282.Audit.Guarantees.PSubmit1.FakeExpo
-import Eip8282.Audit.Guarantees.PDrain1
-import Eip8282.Audit.Guarantees.PDrain1.Footprint
-import Eip8282.Audit.Guarantees.PDrain1.Fifo
-import Eip8282.Audit.Guarantees.PDrain1.Encode
-import Eip8282.Audit.Guarantees.PControl1
-import Eip8282.Audit.Guarantees.PControl1.Gate
-import Eip8282.Audit.Guarantees.PControl1.Excess
-import Eip8282.Audit.Guarantees.PControl1.Count
-import Eip8282.Audit.Guarantees.PControl1.Ctor
-import Eip8282.Audit.Guarantees.PControl1.CtorXi
-import Eip8282.Audit.Reachable
-import Eip8282.Audit.Represents
-import Eip8282.Audit.UserXiCorrespondence
-import Eip8282.Audit.SystemXiCorrespondence
-import Eip8282.Audit.AllGuarantees
-import Eip8282.Audit.XiTransport
-import Eip8282.Audit.UniversalBoundary
-import Eip8282.Audit.EntryReach
-import Eip8282.Audit.EntryReach.Operands
-import Eip8282.Audit.EntryReach.Endpoint
-import Eip8282.Audit.Integrator
-import Eip8282.Audit.Trust
-import Eip8282.Tests.Mutants
-import Eip8282.Tests.PSubmit1Mutant
-import Eip8282.Tests.PControl1Mutant
-import Eip8282.Tests.PDrain1Mutant
-import Eip8282.Tests.DirectMutations
+import Eip8282.Audit.Integrator.DirectGuarantees
+
+/-! The three registered direct guarantees. Candidate protocol/history adapters
+and historical correspondence proofs are built separately by `make candidates`.
+Mutation refutations and the focused trust report are built by `make test`. -/