Derive proof domains from supply and execution-work limits

Eip8282/Audit/Integrator.lean

@@ -1,3 +1,4 @@
+import Eip8282.Audit.Integrator.ResourceAssumptions
 import Eip8282.Audit.EntryReach.FeeQuote
 import Eip8282.Audit.EntryReach.FeeQuotePath
 import Eip8282.Audit.EntryReach.FeeQuoteGetter

Eip8282/Audit/Integrator/ResourceAssumptions.lean

@@ -0,0 +1,152 @@
+import Eip8282.Audit.Integrator.FactoryHistoryGuarantees
+
+/-!
+# Supply and executed-work assumptions
+
+The supply bound concerns the actual world at every transaction entry, not
+lifetime issuance and not just the final world. Admission and the nested
+funding proof derive the bounds at inner calls. Work is the conservative
+marked-LOG0 count of the actual execution trees, including rolled-back work.
+Neither assumption contains a fee, storage or queue invariant.
+-/
+namespace Eip8282.Audit.Integrator.ResourceAssumptions
+open EvmYul EvmYul.EVM NestedEvents
+open ReachableCalls (Contract address)
+open TransactionAppendBudget (Receipt)
+open TransactionCommittedEffects
+open JournalInvariant (modelKind)
+open QueueInvariant SystemSpec
+set_option autoImplicit false
+set_option maxRecDepth 20000
+set_option maxHeartbeats 2400000
+
+/-- 10^50 ETH, expressed in wei. -/
+def supplyLimit : Nat := 10^68
+
+theorem supply_units : supplyLimit = 10^50 * 10^18 := by decide
+
+theorem supply_below_fee_boundary : supplyLimit < FundedDomain.fundingCeiling := by
+  decide +kernel
+
+theorem supply_fits_word : supplyLimit < UInt256.size := by decide
+
+/-- Circulating funds at each actual transaction input. Nested checkpoints
+are handled by the execution funding proof, not additional assumed bounds. -/
+def SupplyBound (receipts : List Receipt) : Prop :=
+  ∀ r ∈ receipts, TransferFunding.worldFunds r.call.world < supplyLimit
+
+/-- Derive state invariants from initialization, linked admitted execution,
+transaction-entry supply and total executed work. External credits may exceed
+this bound over the lifetime if burns keep each transaction entry below it. -/
+theorem preserves {kind : Contract} {initial final : World} {receipts : List Receipt}
+    {credits : Nat} (history : ActualJournalHistory.Trace initial receipts credits final)
+    (seed : JournalInvariant.Invariant kind 0 initial)
+    (supply : SupplyBound receipts) (work : ActualJournalHistory.work receipts < 2^128) :
+    JournalInvariant.Invariant kind (ActualJournalHistory.work receipts) final := by
+  induction history with
+  | initial => exact seed
+  | @transaction receipts credits before prior r linked account admission fit resources ih =>
+    have previousSupply : SupplyBound receipts := by
+      intro x hx
+      exact supply x (List.mem_append_left _ hx)
+    have currentSupply := supply r (List.mem_append_right _ (by simp))
+    rw [ActualJournalHistory.work_append] at work ⊢
+    have previous := ih previousSupply (by omega)
+    have atCall : JournalInvariant.Invariant kind (ActualJournalHistory.work receipts) r.call.world := by
+      rw [linked]
+      exact previous
+    exact ActualJournalHistory.transaction_step r FundingHistory.Trace.initial admission
+      (by simpa using currentSupply.trans supply_below_fee_boundary) fit resources atCall work
+  | system prior t sender zero fit ih =>
+    exact SystemJournal.preserves t sender zero fit work (ih supply work)
+  | transfer prior sender recipient amount funded ih =>
+    exact JournalInvariant.frame (ih supply work)
+      (ProtocolTransfer.frame _ sender recipient (address kind) amount)
+  | credit prior recipient amount ih =>
+    exact JournalInvariant.frame (ih supply work)
+      (FinalizationWorldFrame.credit_frame _ recipient (address kind) amount)
+
+/-- The formula and counter/physical-queue conditions are conclusions of the
+history theorem. Enabled safety includes the inhibitor case. -/
+theorem domains {kind : Contract} {initial final : World} {receipts : List Receipt}
+    {credits : Nat} (history : ActualJournalHistory.Trace initial receipts credits final)
+    (seed : JournalInvariant.Invariant kind 0 initial)
+    (supply : SupplyBound receipts) (work : ActualJournalHistory.work receipts < 2^128) :
+    AccountedState.Bounded (ActualJournalHistory.work receipts) (worldSlot final (address kind)) ∧
+    FundedDomain.EnabledSafe (match kind with | .deposit => 8 | .exit => 2)
+      (worldSlot final (address kind)) ∧
+    ∃ queue : JournalPathQueues.Queue kind,
+      Represents (modelKind kind) (worldSlot final (address kind)) queue := by
+  have hi := preserves history seed supply work
+  obtain ⟨queue,represented⟩ := HistoryCommittedGuarantees.represented_queue hi
+  cases kind with
+  | deposit => exact ⟨hi.2.1,hi.2.2.1,queue,represented⟩
+  | exit => exact ⟨hi.2.1,hi.2.2.1,queue,represented⟩
+
+/-- A next completed plain call, including an independently scheduled SYSTEM
+call, consumes the derived domains directly. Its actual receipt and input
+width remain explicit; scheduling and success are not promised. -/
+theorem completed_call {kind : Contract} {initial before after : World}
+    {receipts : List Receipt} {credits : Nat}
+    (history : ActualJournalHistory.Trace initial receipts credits before)
+    (seed : JournalInvariant.Invariant kind 0 initial)
+    (supply : SupplyBound receipts) (work : ActualJournalHistory.work receipts < 2^128)
+    (call : ReachableCalls.Transition kind before after)
+    (fit : call.call.calldata.size < UInt256.size) :
+    NestedProtectedJournal.Observed kind call.call call.created after call.substate
+      call.success call.output :=
+  JournalGuarantees.completed call (preserves history seed supply work) work fit
+
+/-- All three guarantees and the represented physical queue at any actual
+transaction position. No numeric fee or per-call storage domain is a premise. -/
+theorem guarantees {kind : Contract} {initial final : World} {receipts : List Receipt}
+    {credits : Nat} (history : ActualJournalHistory.Trace initial receipts credits final)
+    (seed : JournalInvariant.Invariant kind 0 initial)
+    (supply : SupplyBound receipts) (work : ActualJournalHistory.work receipts < 2^128)
+    {i : Nat} {r : Receipt} (atIndex : receipts[i]? = some r) :
+    ∃ queue : JournalPathQueues.Queue kind,
+      Represents (modelKind kind) (worldSlot r.call.world (address kind)) queue ∧
+      Effects kind r queue ∧ LocalGuarantees kind r := by
+  obtain ⟨pc,_,prior,account,admission,fit,resources⟩ :=
+    ActualHistoryCalls.transaction_prefix history atIndex
+  have prefixSupply : SupplyBound (receipts.take i) := by
+    intro x hx
+    exact supply x (List.mem_of_mem_take hx)
+  have positionWork := ActualHistoryCalls.position_work atIndex
+  have hi := preserves prior seed prefixSupply (by omega)
+  have funds : TransferFunding.worldFunds r.call.world + 0 < FundedDomain.fundingCeiling := by
+    have member : r ∈ receipts := List.mem_of_getElem? atIndex
+    simpa using (supply r member).trans supply_below_fee_boundary
+  obtain ⟨queue,represented⟩ := HistoryCommittedGuarantees.represented_queue hi
+  refine ⟨queue,represented,receipt_effects r FundingHistory.Trace.initial admission funds fit resources hi
+    (lt_of_le_of_lt positionWork work) queue represented,?_⟩
+  intro path fuel a created world gas ss status out loc ht
+  exact (TransactionJournal.observed r.call FundingHistory.Trace.initial admission funds fit resources hi
+    (TransactionAppendBudget.tree_cert r) (lt_of_le_of_lt positionWork work) loc ht rfl).choose_spec.2.2
+
+/-- The verified factory transaction produces the seed; the consumer supplies
+no initial queue or safe-fee invariant. Factory/address/admission/resource
+inputs remain explicit and are not a claim of canonical installation. -/
+theorem from_deployment {kind : Contract} (deployment : Receipt)
+    (inputs : FactoryHistoryGuarantees.Inputs kind deployment.call)
+    (deploymentSupply : TransferFunding.worldFunds deployment.call.world < supplyLimit)
+    {final : World} {receipts : List Receipt} {credits : Nat}
+    (history : ActualJournalHistory.Trace deployment.world receipts credits final)
+    (supply : SupplyBound receipts) (work : ActualJournalHistory.work receipts < 2^128)
+    {i : Nat} {r : Receipt} (atIndex : receipts[i]? = some r) :
+    deployment.success = true ∧ ∃ queue : JournalPathQueues.Queue kind,
+      Represents (modelKind kind) (worldSlot r.call.world (address kind)) queue ∧
+      Effects kind r queue ∧ LocalGuarantees kind r := by
+  obtain ⟨success,seed,_,_,_⟩ := FactoryHistoryGuarantees.deployment_seed deployment inputs
+    (deploymentSupply.trans supply_fits_word)
+  exact ⟨success,guarantees history seed supply work atIndex⟩
+
+#print axioms supply_units
+#print axioms supply_below_fee_boundary
+#print axioms supply_fits_word
+#print axioms preserves
+#print axioms domains
+#print axioms completed_call
+#print axioms guarantees
+#print axioms from_deployment
+end Eip8282.Audit.Integrator.ResourceAssumptions

Eip8282/Audit/Trust.lean

@@ -3981,3 +3981,14 @@ exercising the aggregate accounting in isolation. -/
 ReferenceFundedHistoryLifecycle.next: receipts telescope + block length. -/
 #print axioms Eip8282.Audit.Integrator.ReferenceHistoryNextComposition.next_next_receipts
 #print axioms Eip8282.Audit.Integrator.ReferenceHistoryNextComposition.next_next_blocks_length
+
+/-! Simple supply and executed-work assumptions, with domains derived. -/
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.supply_units
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.supply_below_fee_boundary
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.supply_fits_word
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.preserves
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.domains
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.guarantees
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.from_deployment
+
+#print axioms Eip8282.Audit.Integrator.ResourceAssumptions.completed_call

README.md

@@ -86,3 +86,10 @@ Historical CFG/model parents and tests remain unchanged in Lean. Their old
 metadata and detailed development narrative are preserved in
 [audit/history](audit/history). No main merge, normative repin, deployment or
 external audit certification follows from these local checks.
+
+## Readable resource assumptions
+
+The history-facing wrappers derive the numerical fee/counter conditions from
+ETH supply below 10^50 ETH and conservative executed work below 2^128 events,
+starting from verified initialization and a linked admitted history. See
+[the exact assumptions and remaining protocol limits](audit/release/RESOURCE-ASSUMPTIONS.md).

audit/assumptions.yaml

@@ -61,8 +61,8 @@
       "severity": "HIGH",
       "scope": "Explicit local theorem hypotheses; their protocol coverage remains to derive.",
       "risk": "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. Drain additionally requires physical FIFO representation and exit source width. Constructor and SYSTEM liveness domains are separate as stated in the theorem and guarantees metadata.",
-      "validation": "DirectGuarantees.Domain, DirectDrain.Domain, DirectInitialization.Domain and SystemProgress.Progress; code-independent mutant domain witnesses.",
-      "removal_path": "Extract these conditions from actual initialized protocol histories using proved funding, event and resource bounds."
+      "validation": "DirectGuarantees.Domain, DirectDrain.Domain, DirectInitialization.Domain and SystemProgress.Progress; code-independent mutant domain witnesses. ResourceAssumptions.domains derives the fee, counter and physical-queue conditions from initialized linked histories, per-transaction supply <10^68 wei and actual work <2^128; see audit/release/RESOURCE-ASSUMPTIONS.md.",
+      "removal_path": "Canonical protocol producers must supply the verified initialization, linked admitted history and explicit supply/work bounds. ResourceAssumptions.from_deployment derives local domains and all three observations for such histories without assuming intermediate invariants."
     },
     {
       "id": "A-PINNED-EVM-SEMANTICS",
@@ -80,8 +80,8 @@
       "accepted": false,
       "severity": "HIGH",
       "scope": "The remaining complete audit objective.",
-      "risk": "Local queue/arithmetic hypotheses are not yet derived for every valid initialized call. Final-world funding, intermediate calls, external credits, fees/escrow/refunds, actual event aggregation including ancestor rollback, block bounds and deployment history must compose.",
-      "validation": "ConcreteHistory is actual linked-call preservation under explicit funding/event-budget inputs. ReturnedGas universally proves remaining-gas monotonicity; TransactionGas derives actual net-gas/refund arithmetic; ordinary and transfer funding are proved. These do not establish the missing history extraction.",
+      "risk": "Canonical Ethereum installation, activation, SYSTEM authorization/scheduling, normative fork selection and complete history/admission extraction remain open. Conditional initialized-history composition now includes nested funding, rolled-back work, queue representation and the three local observations.",
+      "validation": "ResourceAssumptions.from_deployment derives local domains, queue effects and observations from verified factory initialization, linked admitted execution, transaction-entry supply <10^68 wei and counted execution work <2^128. This does not derive these history inputs from canonical Ethereum.",
       "removal_path": "Construct actual execution/event and protocol-history adapters, derive their bounds, then instantiate the registered direct parents without unproved domain premises."
     }
   ],

audit/receipts/resource-assumptions.json

@@ -0,0 +1,84 @@
+{
+  "schema": "eip8282-resource-assumptions-v1",
+  "base_commit": "8adad418061a834e2a19890195d2e6d754cfe290",
+  "source": "Eip8282/Audit/Integrator/ResourceAssumptions.lean",
+  "source_sha256": "5ecc11bb930ad61695eda8d9d613fa51d9408cdc713243a33293c42dae93a37e",
+  "namespace": "Eip8282.Audit.Integrator.ResourceAssumptions",
+  "declarations": [
+    "supply_units",
+    "supply_below_fee_boundary",
+    "supply_fits_word",
+    "preserves",
+    "domains",
+    "completed_call",
+    "guarantees",
+    "from_deployment"
+  ],
+  "numerical_assumptions": {
+    "supply": "worldFunds at every actual transaction entry <10^68 wei (10^50 ETH); deployment entry bounded separately",
+    "work": "ActualJournalHistory.work receipts <2^128; all completed LOG0 operations with length >=68 bytes in actual receipt execution trees, including unrelated matching logs and rolled-back events"
+  },
+  "remaining_inputs": [
+    "actual factory deployment Inputs with installed factory, exact calldata/code, address/hash binding, nonce/collision/admission/resource conditions",
+    "linked ActualJournalHistory.Trace with actual transaction and SYSTEM receipts, funded transfers and explicit credits",
+    "transaction admission, calldata width and sufficient evaluator fuel",
+    "next completed_call additionally takes actual pinned plain-CALL Transition and input width"
+  ],
+  "derived": [
+    "safe natural fee numerator <=2892 or inhibition",
+    "bounded counters and physical queue representation, including exit source width in invariant",
+    "all three local guarantee observations at actual protected calls, including nested calls whose ancestors roll back",
+    "committed transaction queue/log effects",
+    "verified factory initialization supplies initial invariant"
+  ],
+  "not_claimed": [
+    "canonical Ethereum protocol-history extraction",
+    "canonical installation/activation/SYSTEM scheduling",
+    "normative fork or policy adoption",
+    "unconditional call success",
+    "final quoted fee exceeds 256 bits at2893: divergence is from intermediate multiplication overflow"
+  ],
+  "axioms": {
+    "numerical": [
+      "propext"
+    ],
+    "history": [
+      "propext",
+      "Classical.choice",
+      "Quot.sound"
+    ]
+  },
+  "checks": {
+    "ffi": "PASS: lake build EvmYul.FFI.ffi:dynlib (11 jobs)",
+    "target": "PASS: LEAN_NUM_THREADS=2 lake build Eip8282.Audit.Integrator.ResourceAssumptions (3354 jobs)",
+    "full": {
+      "command": "LEAN_NUM_THREADS=2 make check",
+      "exit_code": 0,
+      "results": [
+        "audit-check ok",
+        "prove ok",
+        "test ok",
+        "check ok"
+      ],
+      "default_build_jobs": 3678,
+      "mutation_build_jobs": 3608,
+      "log_sha256": "1a580b02c7f28adb868681c9851bc19b7b106ddc4c89da34e1cbaf5fb555c31b"
+    },
+    "independent": {
+      "verdict": "CLEAN",
+      "reviewer_lane": "validate_resource_bounds",
+      "command": "LEAN_NUM_THREADS=2 lake env lean --load-dynlib=.lake/packages/evmyul/.lake/build/lib/libleanffi.dylib --load-dynlib=.lake/packages/evmyul/.lake/build/lib/lean/evmyul_EvmYul_FFI_ffi.dylib Eip8282/Audit/Integrator/ResourceAssumptions.lean",
+      "exit_code": 0,
+      "metadata_exit_code": 0,
+      "diff_check_exit_code": 0,
+      "source_sha256_before_and_after": "5ecc11bb930ad61695eda8d9d613fa51d9408cdc713243a33293c42dae93a37e",
+      "log_sha256": "6deb296e2a835749eec144fe786b122ec30cec6bead4c69da98f8e5ca4a47459"
+    }
+  },
+  "validated_at_utc": "2026-09-15T12:05:49.783551+00:00",
+  "changed_lean_sources_sha256": {
+    "Eip8282/Audit/Integrator/ResourceAssumptions.lean": "5ecc11bb930ad61695eda8d9d613fa51d9408cdc713243a33293c42dae93a37e",
+    "Eip8282/Audit/Integrator.lean": "e272be05ab01eb365cb33bc4bafb9ceb965f528800b515eca90364fe92c4a61e",
+    "Eip8282/Audit/Trust.lean": "92c9ed245de3671cbfe4d153336ba53790e99b65a84996a06754fedfde81fdf1"
+  }
+}