1 import Eip8282.Audit.Integrator.ReferenceAdmissionExtraction2 import Eip8282.Audit.Integrator.TransactionFunding3 import Eip8282.Audit.Integrator.FactoryHistoryGuarantees4 import Eip8282.Audit.Integrator.ActualJournalHistory5 import Eip8282.Audit.Integrator.ReferenceSourcePrepaidCheckpoint6 7 /-! Canonical-producer hook interfaces for the three named Ethereum-semantic8 raccordements listed in DIRECT-CLOSURE.md remaining obligation 4.9 10 This module names the *interface* a canonical producer of Ethereum semantics11 must supply so that the existing conditional theorems can be discharged. It12 adds no new premise, adopts no new protocol policy, and does not identify13 any new bytecode with a reference implementation. Each declaration below is14 a *type* — a `structure` bundling the exact hypotheses downstream theorems15 already consume — plus a small structural theorem projecting the bundle to16 the raw fields those theorems accept.17 18 The three named hooks:19 20 * `CompleteAdmission` — bundles the audited partial admission21 (`ReferenceAdmissionExtraction.SourceChecks`) with the funding22 admission (`TransactionFunding.Admission`), the sender read, and the23 represented-recipient recovery. It does not add signature recovery,24 full blob validation, capacity checks or type-4 authorization; those25 remain OPEN, and callers must widen this structure once a canonical26 Ethereum admission machinery becomes available.27 28 * `Deployment` — bundles the two factory-deployment `Inputs` records for29 the deposit and exit contracts, together with the linked-worlds30 condition. This is exactly the shape `FactoryHistoryGuarantees.two_seeds`31 consumes; canonical Ethereum production of these records remains32 external.33 34 * `SystemAuthorization` — bundles the empty-data zero-value SYSTEM35 invocation guards (`caller = sysAddr`, `value = 0`,36 `calldata.size < UInt256.size`) that37 `ActualJournalHistory.Trace.system` consumes. It does not adopt a38 schedule, does not identify the caller's authorization source and does39 not claim the pinned reference invokes any particular SYSTEM address40 automatically.41 42 For each hook the module exposes a `.project` theorem returning the raw43 fields the downstream conditional theorem accepts, so a canonical producer44 can hand off its bundle and let the existing composition run without45 pattern-matching on the internal structure.46 47 The three declarations remain `Prop`-valued obligations: they are neither48 axioms nor claimed satisfactions. Their purpose is to make the exact49 interface auditable at a single site. -/50 namespace Eip8282.Audit.Integrator.ReferenceCanonicalHooks51 52 open EvmYul EvmYul.EVM53 open ReachableCalls (Contract)54 open TransactionAppendBudget (Receipt)55 open ReferenceAdmissionExtraction (SourceChecks)56 set_option autoImplicit false57 58 /-! ## Hook 1 — Complete admission -/59 60 /-- Interface a canonical Ethereum admission producer must supply for a61 represented nonblob ordinary call. Combines the audited partial admission62 (`SourceChecks`) with the funding admission and the sender/recipient63 correspondence. Complete Ethereum admission (signature recovery, full blob64 validation, capacity, type-4 authorization) remains OPEN and must widen65 this structure. -/66 structure CompleteAdmission (tx : RefundAccounting.Context) (kind : Contract)67 (sender : Account .EVM) : Prop where68 /-- Audited partial admission over represented inputs. -/69 checks : SourceChecks tx sender70 /-- Prepayment/nonce/priority admission consumed by transaction funding. -/71 funding : TransactionFunding.Admission tx sender72 /-- Sender lookup in the pre-transaction world. -/73 senderRead : tx.world.get? tx.sender = some sender74 /-- Represented recipient equals the audited pinned target. -/75 recipient : tx.transaction.base.recipient = some (ReachableCalls.address kind)76 /-- Nonblob transaction (blob validation remains an OPEN separate hook). -/77 nonblob : ReferenceSourcePrepaidCheckpoint.Nonblob tx.transaction78 79 /-- Projection: a canonical producer hands off the five fields the80 downstream fee-block theorems already accept as separate arguments. -/81 theorem CompleteAdmission.project {tx : RefundAccounting.Context} {kind : Contract}82 {sender : Account .EVM}83 (h : CompleteAdmission tx kind sender) :84 SourceChecks tx sender ∧ TransactionFunding.Admission tx sender ∧85 tx.world.get? tx.sender = some sender ∧86 tx.transaction.base.recipient = some (ReachableCalls.address kind) ∧87 ReferenceSourcePrepaidCheckpoint.Nonblob tx.transaction :=88 ⟨h.checks, h.funding, h.senderRead, h.recipient, h.nonblob⟩89 90 /-! ## Hook 2 — Deployment -/91 92 /-- Interface a canonical Ethereum deployment producer must supply. Bundles93 the two `FactoryHistoryGuarantees.Inputs` records for the deposit and exit94 contracts with the linked-worlds condition. This is the exact input95 `FactoryHistoryGuarantees.two_seeds` consumes; canonical production of the96 records remains external. The structure is Type-valued (not Prop-valued)97 because `Inputs` carries data fields (steps, sender account, factory98 account) beyond pure propositions. -/99 structure Deployment (deposit exit : Receipt) where100 depositInputs : FactoryHistoryGuarantees.Inputs .deposit deposit.call101 exitInputs : FactoryHistoryGuarantees.Inputs .exit exit.call102 linked : exit.call.world = deposit.world103 104 /-- Convenience wrapper naming the linked-worlds hypothesis explicitly.105 The `Inputs` fields are Type-valued and are directly accessible as106 `.depositInputs` / `.exitInputs` on the structure itself; no separate107 projection theorem is required for them. -/108 theorem Deployment.linked_hypothesis {deposit exit : Receipt}109 (h : Deployment deposit exit) : exit.call.world = deposit.world := h.linked110 111 /-! ## Hook 3 — SYSTEM authorization -/112 113 /-- Interface a canonical SYSTEM caller/scheduler must supply for a single114 empty-data zero-value SYSTEM invocation. This is exactly the field set115 `ActualJournalHistory.Trace.system` accepts. It does not adopt a schedule,116 does not identify the caller's authorization source and does not claim any117 particular SYSTEM address is invoked by the pinned reference automatically. -/118 structure SystemAuthorization (c : MessageCall.Context) : Prop where119 caller : c.caller = Eip8282.Audit.EvmRunner.sysAddr120 zeroValue : c.value = ⟨0⟩121 dataFit : c.calldata.size < UInt256.size122 123 /-- Projection: hands off the three fields the SYSTEM Trace step accepts. -/124 theorem SystemAuthorization.project {c : MessageCall.Context}125 (h : SystemAuthorization c) :126 c.caller = Eip8282.Audit.EvmRunner.sysAddr ∧ c.value = ⟨0⟩ ∧127 c.calldata.size < UInt256.size :=128 ⟨h.caller, h.zeroValue, h.dataFit⟩129 130 /-! ## Combined interface -/131 132 /-- A single bundle containing all three canonical hooks. Consumers that133 require the whole set can accept `AllHooks` and dispatch to each hook via134 the `.admission`, `.deployment`, `.authorization` accessors below. This is135 still purely interface: no protocol policy is asserted, no schedule is136 adopted, and the bundle carries no output field. Type-valued because the137 inner `Deployment` carries data fields. -/138 structure AllHooks (tx : RefundAccounting.Context) (kind : Contract)139 (sender : Account .EVM) (deposit exit : Receipt)140 (systemCall : MessageCall.Context) where141 admission : CompleteAdmission tx kind sender142 deployment : Deployment deposit exit143 authorization : SystemAuthorization systemCall144 145 /-- Convenience wrapper projecting the two Prop-valued hooks. The146 Type-valued `Deployment` field is directly accessible as `.deployment`147 on the structure itself. -/148 theorem AllHooks.propHooks {tx : RefundAccounting.Context} {kind : Contract}149 {sender : Account .EVM} {deposit exit : Receipt} {systemCall : MessageCall.Context}150 (h : AllHooks tx kind sender deposit exit systemCall) :151 CompleteAdmission tx kind sender ∧ SystemAuthorization systemCall :=152 ⟨h.admission, h.authorization⟩153 154 #print axioms CompleteAdmission.project155 #print axioms Deployment.linked_hypothesis156 #print axioms SystemAuthorization.project157 #print axioms AllHooks.propHooks158 159 end Eip8282.Audit.Integrator.ReferenceCanonicalHooks160