1 {2 "schema": "eip-8282-assurance-contract-v1",3 "authority": "Lean theorem statements and proofs are authoritative; metadata classifies but never closes evidence.",4 "objective": "Exactly three registered conditional direct guarantees for actual complete pinned calls. Their theorem statements are CHECKED under explicit domains; complete protocol applicability remains OPEN/PARTIAL. Historical CFG/model and finite evidence are retained separately.",5 "guarantees": [6 {7 "id": "P-SUBMIT-1",8 "parent": "Eip8282.Audit.Integrator.DirectGuarantees.psubmit1_direct",9 "parent_note": "Universal conditional direct proof for both contract kinds at pinned code; no finite trace or legacy correspondence conjunct. The overall protocol audit remains PARTIAL.",10 "assumptions": [11 "A-CLASSICAL-CHOICE",12 "A-DIRECT-DOMAIN",13 "A-PINNED-EVM-SEMANTICS",14 "A-PROTOCOL-CLOSURE",15 "A-PINNED-SOURCE"16 ],17 "summary": "Only a non-inhibited, well-formed, sufficiently paid nonempty user call can successfully append one authentic record and one anonymous LOG0. Deposits retain exactly 184 calldata bytes, require at least 10^9 gwei amount and fee+amount*1gwei payment, and do not validate signatures. Exits store/log caller20||pubkey48. Actual failure restores the pre-transfer journal. Successful getters preserve account lookups, created accounts and logs and have zero value. SYSTEM adds no logs and preserves all record slots.",18 "abstract": {19 "status": "CHECKED",20 "theorem": "Eip8282.Audit.Guarantees.PSubmit1.success_count_and_balance"21 },22 "evm": {23 "status": "CHECKED",24 "scope": "THETA_CONDITIONAL_FORALL",25 "theorem": "Eip8282.Audit.Integrator.DirectGuarantees.psubmit1_direct",26 "executes": "Actual pinned EvmYul.EVM.\u0398 and its \u039e/X bytecode execution; P-CONTROL-1 also quantifies actual \u039b initialization. EVMYulLean b62586650b4f96cc6da25f36574aaa8f329a6420. Small independent storage/encoding/FIFO/math specs; no global legacy Model equivalence.",27 "world": "Actual completed \u0398 calls at arbitrary gas, evaluator fuel, permission, surrounding AccountMap, original world and header. Independent input conditions: target exists; apparent value equals transferred value; calldata.size < 2^256; natural budget < 2^128; HEAD <= TAIL <= budget, count <= budget, and enabled excess+count <= budget; either inhibited or natural fee numerator excess+max(0,count-TARGET) <= 2892. No original-code pin, predicted post-state, fee completion or path premise occurs inside the domain. Interpreter OutOfFuel is an error, outside completed .ok results.",28 "kill_line": {29 "module": "Eip8282.Tests.DirectThetaKills",30 "theorem": "Eip8282.Tests.DirectThetaKills.submit_kill",31 "mutation": "Deposit runtime byte 274: LOG0 length PUSH1 operand 184 -> 0; the actual funded call returns one empty log.",32 "effect": "One actual \u0398 counterexample with a code-independent budget-0 domain, two ETH total pre-balances, real/apparent value 1ETH+1wei, and 184-byte input. Its 158 decode/Z/Step certificates and \u0398 settlement are kernel checked; no native execution axiom.",33 "independence": "No universal sibling survival claim. Guarantees intentionally overlap: stale record corruption also contradicts PSubmit SYSTEM framing. Historical sibling Boolean facts remain finite regression checks, separately archived."34 }35 },36 "fidelity": {37 "covered": [38 "Actual successful nonempty user \u0398 yields exactly one authentic record/log and empty return, plus the untruncated mathematical fee and payment inequality.",39 "Actual completed invalid/inhibited calls roll back; successful getters are read-only on accounts/logs/created set. Access bookkeeping is not claimed unchanged.",40 "Actual SYSTEM \u0398 cannot add a log or alter any storage word at slot >=4."41 ],42 "missing": [43 "Derive the independent local domains from initialized valid Ethereum execution, including nested calls and rollback.",44 "Canonical source-to-Lean full occurrence identity, real block/history extraction and protocol justification of the explicit credit bounds; pinned-semantic accounting is already composed.",45 "Pinned evaluator adequacy for the selected protocol fork; transaction admission, canonical predeploy installation and SYSTEM scheduling."46 ]47 },48 "classification": {49 "kind": "PARTIAL",50 "work": "The registered conditional complete-call theorem is proved. Application to all protocol-reachable calls remains OPEN; neither a green build nor a finite mutation witness closes it."51 },52 "protocol_closure": {53 "status": "OPEN",54 "assumption": "A-PROTOCOL-CLOSURE"55 },56 "reproduction": {57 "command": "make check",58 "expected": "Direct parents and all six same-predicate \u0398 refutations compile; Trust shows only propext/Classical.choice/Quot.sound for direct correctness parents and the funded LOG witness. Five other finite refutations disclose their respective old native receipt axioms separately.",59 "prerequisite": "Make builds EVMYul FFI dynlibs before Lean."60 },61 "supporting_historical_evidence": {62 "metadata": "audit/history/pre-direct-guarantees-20260909.json",63 "parent": "Eip8282.Audit.Guarantees.PSubmit1.psubmit1_forall_parent",64 "note": "Kept unchanged in Lean, with its CFG/model claims and finite native traces; not conjoined into the registered direct proof."65 },66 "next_gate": "Discharge A-PROTOCOL-CLOSURE and establish the deployment/fork binding; do not revive unrestricted legacy \u039e\u2194Model as a prerequisite.",67 "roadmap_priority": "NOW"68 },69 {70 "id": "P-DRAIN-1",71 "parent": "Eip8282.Audit.Integrator.DirectGuarantees.pdrain1_direct",72 "parent_note": "Universal conditional direct proof for both contract kinds at pinned code; no finite trace or legacy correspondence conjunct. The overall protocol audit remains PARTIAL.",73 "assumptions": [74 "A-CLASSICAL-CHOICE",75 "A-DIRECT-DOMAIN",76 "A-PINNED-EVM-SEMANTICS",77 "A-PROTOCOL-CLOSURE",78 "A-PINNED-SOURCE"79 ],80 "summary": "Only SYSTEM consumes the queue. Its actual success returns exactly the oldest min(length,cap) records, caps 64 deposits/16 exits, with deposit amount recoded BE to LE and exits as stored. Full drain resets both pointers, partial drain advances HEAD and leaves TAIL; every old record slot remains. User success keeps HEAD and the old queue prefix, extending it by exactly one record only on nonempty input; failure keeps the world/queue.",81 "abstract": {82 "status": "CHECKED",83 "theorem": "Eip8282.Audit.Guarantees.PDrain1.fifo_bounded"84 },85 "evm": {86 "status": "CHECKED",87 "scope": "THETA_CONDITIONAL_FORALL",88 "theorem": "Eip8282.Audit.Integrator.DirectGuarantees.pdrain1_direct",89 "executes": "Actual pinned EvmYul.EVM.\u0398 and its \u039e/X bytecode execution; P-CONTROL-1 also quantifies actual \u039b initialization. EVMYulLean b62586650b4f96cc6da25f36574aaa8f329a6420. Small independent storage/encoding/FIFO/math specs; no global legacy Model equivalence.",90 "world": "Actual completed \u0398 calls at arbitrary gas, evaluator fuel, permission, surrounding AccountMap, original world and header. Independent input conditions: target exists; apparent value equals transferred value; calldata.size < 2^256; natural budget < 2^128; HEAD <= TAIL <= budget, count <= budget, and enabled excess+count <= budget; either inhibited or natural fee numerator excess+max(0,count-TARGET) <= 2892. No original-code pin, predicted post-state, fee completion or path premise occurs inside the domain. Interpreter OutOfFuel is an error, outside completed .ok results. Additionally: the independent physical queue representation and exit source words <2^160, including retained entries.",91 "kill_line": {92 "module": "Eip8282.Tests.DirectThetaKills",93 "theorem": "Eip8282.Tests.DirectThetaKills.drain_kills",94 "mutation": "Deposit cap byte 304:64->32; exit cap byte 244:16->8; deposit partial-head SSTORE slot byte 483:2->9.",95 "effect": "Three actual \u0398 counterexamples instantiate independent physical queues and domains. Each reuses only its corresponding historical finite \u039e native receipt after exact entry/settlement transport. They refute the same new PDrain predicate.",96 "independence": "No universal sibling survival claim. Guarantees intentionally overlap: stale record corruption also contradicts PSubmit SYSTEM framing. Historical sibling Boolean facts remain finite regression checks, separately archived."97 }98 },99 "fidelity": {100 "covered": [101 "Actual \u0398 return bytes equal independent FIFO take/encoding; the actual post-world represents the corresponding drop.",102 "Natural full/partial pointers, caps, packed length and all stale record words are preserved as specified.",103 "Every successful user call, including the getter, preserves HEAD and the prior queue prefix."104 ],105 "missing": [106 "Derive the independent local domains from initialized valid Ethereum execution, including nested calls and rollback.",107 "Canonical source-to-Lean full occurrence identity, real block/history extraction and protocol justification of the explicit credit bounds; pinned-semantic accounting is already composed.",108 "Pinned evaluator adequacy for the selected protocol fork; transaction admission, canonical predeploy installation and SYSTEM scheduling."109 ]110 },111 "classification": {112 "kind": "PARTIAL",113 "work": "The registered conditional complete-call theorem is proved. Application to all protocol-reachable calls remains OPEN; neither a green build nor a finite mutation witness closes it."114 },115 "protocol_closure": {116 "status": "OPEN",117 "assumption": "A-PROTOCOL-CLOSURE"118 },119 "reproduction": {120 "command": "make check",121 "expected": "Direct parents and all six same-predicate \u0398 refutations compile; Trust shows only propext/Classical.choice/Quot.sound for direct correctness parents and the funded LOG witness. Five other finite refutations disclose their respective old native receipt axioms separately.",122 "prerequisite": "Make builds EVMYul FFI dynlibs before Lean."123 },124 "supporting_historical_evidence": {125 "metadata": "audit/history/pre-direct-guarantees-20260909.json",126 "parent": "Eip8282.Audit.Guarantees.PDrain1.pdrain1_forall_parent",127 "note": "Kept unchanged in Lean, with its CFG/model claims and finite native traces; not conjoined into the registered direct proof."128 },129 "next_gate": "Discharge A-PROTOCOL-CLOSURE and establish the deployment/fork binding; do not revive unrestricted legacy \u039e\u2194Model as a prerequisite.",130 "roadmap_priority": "NOW"131 },132 {133 "id": "P-CONTROL-1",134 "parent": "Eip8282.Audit.Integrator.DirectGuarantees.pcontrol1_direct",135 "parent_note": "Universal conditional direct proof for both contract kinds at pinned code; no finite trace or legacy correspondence conjunct. The overall protocol audit remains PARTIAL.",136 "assumptions": [137 "A-CLASSICAL-CHOICE",138 "A-DIRECT-DOMAIN",139 "A-PINNED-EVM-SEMANTICS",140 "A-PROTOCOL-CLOSURE",141 "A-PINNED-SOURCE"142 ],143 "summary": "Caller alone selects runtime user/SYSTEM behavior. Inhibition rejects every user but does not prevent a sufficiently resourced writable SYSTEM call. Successful getters return the untruncated mathematical quote without account/log writes; paid append increments count and preserves excess. SYSTEM resets count and latches, unlocks, or stores max(0,excess+count-TARGET), with targets8/2. Actual successful constructor installation gives deposit enabled/exit inhibited, empty queues and pinned runtime.",144 "abstract": {145 "status": "CHECKED",146 "theorem": "Eip8282.Audit.Guarantees.PControl1.empty_updates_excess"147 },148 "evm": {149 "status": "CHECKED",150 "scope": "THETA_CONDITIONAL_FORALL",151 "theorem": "Eip8282.Audit.Integrator.DirectGuarantees.pcontrol1_direct",152 "executes": "Actual pinned EvmYul.EVM.\u0398 and its \u039e/X bytecode execution; P-CONTROL-1 also quantifies actual \u039b initialization. EVMYulLean b62586650b4f96cc6da25f36574aaa8f329a6420. Small independent storage/encoding/FIFO/math specs; no global legacy Model equivalence.",153 "world": "Actual completed \u0398 calls at arbitrary gas, evaluator fuel, permission, surrounding AccountMap, original world and header. Independent input conditions: target exists; apparent value equals transferred value; calldata.size < 2^256; natural budget < 2^128; HEAD <= TAIL <= budget, count <= budget, and enabled excess+count <= budget; either inhibited or natural fee numerator excess+max(0,count-TARGET) <= 2892. No original-code pin, predicted post-state, fee completion or path premise occurs inside the domain. Interpreter OutOfFuel is an error, outside completed .ok results. Initializer domain separately assumes address-preimage encoding, no collision, absent target, Context.fuel=steps+1; deposit gas>=1000/steps>=8; exit permission, sender existence, gas>=25000/steps>=11. It assumes actual creation success and does not assert low-resource creation liveness. SYSTEM progress has the separate resources stated in covered.",154 "kill_line": {155 "module": "Eip8282.Tests.DirectThetaKills",156 "theorem": "Eip8282.Tests.DirectThetaKills.control_kills",157 "mutation": "Deposit caller gate byte 22:EQ->LT; deposit TARGET byte 571:8->9. Each falsifies RuntimeControl and therefore the full PControl conjunction for any initializer parameter.",158 "effect": "Two actual \u0398 counterexamples with parameter-code independent budget105 domains. Each retains only its corresponding historical finite \u039e native receipt. PControl includes RuntimeControl, Initializes and SystemProgress, not just the first conjunct.",159 "independence": "No universal sibling survival claim. Guarantees intentionally overlap: stale record corruption also contradicts PSubmit SYSTEM framing. Historical sibling Boolean facts remain finite regression checks, separately archived."160 }161 },162 "fidelity": {163 "covered": [164 "RuntimeControl observes the actual \u0398 tuple, including failure journal, getter, paid append controls, and SYSTEM latch/unlock/fold.",165 "Initializes observes actual successful \u039b installation under its separate constructor domain.",166 "SystemProgress proves actual successful SYSTEM \u0398 with owner, permission, gas>=2500000 and Context.fuel>=8503, without an enabled-state premise."167 ],168 "missing": [169 "Derive the independent local domains from initialized valid Ethereum execution, including nested calls and rollback.",170 "Canonical source-to-Lean full occurrence identity, real block/history extraction and protocol justification of the explicit credit bounds; pinned-semantic accounting is already composed.",171 "Pinned evaluator adequacy for the selected protocol fork; transaction admission, canonical predeploy installation and SYSTEM scheduling."172 ]173 },174 "classification": {175 "kind": "PARTIAL",176 "work": "The registered conditional complete-call theorem is proved. Application to all protocol-reachable calls remains OPEN; neither a green build nor a finite mutation witness closes it."177 },178 "protocol_closure": {179 "status": "OPEN",180 "assumption": "A-PROTOCOL-CLOSURE"181 },182 "reproduction": {183 "command": "make check",184 "expected": "Direct parents and all six same-predicate \u0398 refutations compile; Trust shows only propext/Classical.choice/Quot.sound for direct correctness parents and the funded LOG witness. Five other finite refutations disclose their respective old native receipt axioms separately.",185 "prerequisite": "Make builds EVMYul FFI dynlibs before Lean."186 },187 "supporting_historical_evidence": {188 "metadata": "audit/history/pre-direct-guarantees-20260909.json",189 "parent": "Eip8282.Audit.Guarantees.PControl1.pcontrol1_forall_parent",190 "note": "Kept unchanged in Lean, with its CFG/model claims and finite native traces; not conjoined into the registered direct proof."191 },192 "next_gate": "Discharge A-PROTOCOL-CLOSURE and establish the deployment/fork binding; do not revive unrestricted legacy \u039e\u2194Model as a prerequisite.",193 "roadmap_priority": "NOW"194 }195 ],196 "scoped_release": {197 "claims": "audit/release/CLAIMS.md",198 "original_clauses": "audit/release/ORIGINAL-GUARANTEES.md",199 "premises": "audit/release/PREMISES.json",200 "evidence_manifest": "audit/release/MANIFEST.json",201 "primary_composition": "Eip8282.Audit.Integrator.ReleaseCandidate.composed",202 "scope": "Actual pinned initialized-history conditional theorems; applicability to canonical Ethereum remains OPEN. Internal installed-code/queue/control/work/fee premises are derived from the explicit history. No EIP or policy adoption.",203 "verification": "Exact frozen candidate status is recorded in the manifest; parent registration unchanged."204 }205 }206