|
| 1 | +import Verity.EVM.Uint256 |
| 2 | +import Verity.EVM.MemoryModel |
| 3 | +import Verity.Core.Uint256 |
| 4 | + |
| 5 | +namespace Verity.EVM.Frame |
| 6 | + |
| 7 | +open Verity.Core (Uint256) |
| 8 | +open Verity.EVM.MemoryModel |
| 9 | + |
| 10 | +/-! |
| 11 | +# EVM `CALL` boundary frame conditions |
| 12 | +
|
| 13 | +Models the slice of EVM `CALL` semantics that touches the caller's |
| 14 | +frame, and proves the frame conditions that downstream contract proofs |
| 15 | +need to reason about external calls without quantifying over callee |
| 16 | +bytecode. |
| 17 | +
|
| 18 | +Promoted from `Benchmark.Cases.ERC4337.EntryPointInvariant.EvmYulFrame`. |
| 19 | +
|
| 20 | +## What this discharges |
| 21 | +
|
| 22 | +Before this module, every benchmark that touched external calls had to |
| 23 | +assume (or reproduce in their own file) the EVM-level frame condition |
| 24 | +that external `CALL` cannot SSTORE the caller's slots and cannot write |
| 25 | +to caller memory outside the declared output buffer. That assumption is |
| 26 | +documented in `AXIOMS.md` under "External Call Module". This module |
| 27 | +makes the assumption a *theorem* of `Verity.EVM`, parameterised over an |
| 28 | +abstract `CalleeResult` whose universal quantification over its |
| 29 | +inhabitants is equivalent to quantifying over arbitrary EVM callee |
| 30 | +bytecode. |
| 31 | +
|
| 32 | +## Roadmap |
| 33 | +
|
| 34 | +A subsequent PR will prove that this abstract `CallerFrame` / |
| 35 | +`CalleeResult` model is the projection of EvmYul's actual `CALL` opcode |
| 36 | +semantics, closing the gap between this layer and the deeper EvmYul |
| 37 | +correctness theorems. |
| 38 | +-/ |
| 39 | + |
| 40 | +/-- An EVM address (160-bit; we expose identity only). -/ |
| 41 | +abbrev Address := Nat |
| 42 | + |
| 43 | +/-- The caller-side EVM frame at a `CALL` boundary. The four mutable |
| 44 | + sub-states the EVM exposes to a contract are modelled explicitly. -/ |
| 45 | +structure CallerFrame where |
| 46 | + thisAddress : Address |
| 47 | + memory : Nat → Uint256 |
| 48 | + storageMap : Nat → Uint256 |
| 49 | + transientStorage : Nat → Uint256 |
| 50 | + returnDataBuf : Nat → Uint256 |
| 51 | + |
| 52 | +/-- Everything an arbitrary callee can return to the caller across a |
| 53 | + `CALL` boundary. The callee's internal storage updates are scoped to |
| 54 | + its own address and so do not appear here — they cannot affect the |
| 55 | + caller's frame. Quantifying over inhabitants of this type is |
| 56 | + equivalent to quantifying over arbitrary EVM callee programs that |
| 57 | + produce any `(success, returndata)` pair. -/ |
| 58 | +structure CalleeResult where |
| 59 | + success : Uint256 |
| 60 | + returnedData : Nat → Uint256 |
| 61 | + |
| 62 | +/-- The portion of EVM `CALL` semantics that touches the caller's frame. |
| 63 | +
|
| 64 | +By the Yellow Paper, `CALL` to a target ≠ self with the caller's output |
| 65 | +buffer `[outOff, outOff + outSize)` updates the caller's memory by |
| 66 | +copying `outSize` words of the callee's returndata into that range, |
| 67 | +leaves storage and transient storage untouched, and writes the new |
| 68 | +returndata buffer to the caller's `returnDataBuf`. -/ |
| 69 | +def applyCallToCaller |
| 70 | + (caller : CallerFrame) (outOff outSize : Nat) (callee : CalleeResult) |
| 71 | + : CallerFrame := |
| 72 | + { caller with |
| 73 | + memory := fun i => |
| 74 | + if outOff ≤ i ∧ i < outOff + outSize then |
| 75 | + callee.returnedData (i - outOff) |
| 76 | + else |
| 77 | + caller.memory i |
| 78 | + returnDataBuf := callee.returnedData } |
| 79 | + |
| 80 | +/-! ## Single-CALL frame theorems -/ |
| 81 | + |
| 82 | +theorem external_call_preserves_caller_storage |
| 83 | + (caller : CallerFrame) (outOff outSize : Nat) (callee : CalleeResult) |
| 84 | + (slotIdx : Nat) : |
| 85 | + (applyCallToCaller caller outOff outSize callee).storageMap slotIdx = |
| 86 | + caller.storageMap slotIdx := by |
| 87 | + simp [applyCallToCaller] |
| 88 | + |
| 89 | +theorem external_call_preserves_caller_transient_storage |
| 90 | + (caller : CallerFrame) (outOff outSize : Nat) (callee : CalleeResult) |
| 91 | + (slotIdx : Nat) : |
| 92 | + (applyCallToCaller caller outOff outSize callee).transientStorage slotIdx = |
| 93 | + caller.transientStorage slotIdx := by |
| 94 | + simp [applyCallToCaller] |
| 95 | + |
| 96 | +theorem external_call_preserves_caller_memory_outside_output_buffer |
| 97 | + (caller : CallerFrame) (outOff outSize : Nat) (callee : CalleeResult) |
| 98 | + (i : Nat) (hOutside : ¬ (outOff ≤ i ∧ i < outOff + outSize)) : |
| 99 | + (applyCallToCaller caller outOff outSize callee).memory i = |
| 100 | + caller.memory i := by |
| 101 | + simp [applyCallToCaller, hOutside] |
| 102 | + |
| 103 | +/-- Headline form: caller-memory preservation under a disjoint output |
| 104 | + buffer. Composes directly with `MemoryModel.Disjoint`. -/ |
| 105 | +theorem external_call_preserves_caller_memory |
| 106 | + (caller : CallerFrame) (outOff outSize : Nat) (callee : CalleeResult) |
| 107 | + (regionLo regionHi : Nat) |
| 108 | + (hDisj : outOff + outSize ≤ regionLo ∨ regionHi ≤ outOff) |
| 109 | + (i : Nat) (hLo : regionLo ≤ i) (hHi : i < regionHi) : |
| 110 | + (applyCallToCaller caller outOff outSize callee).memory i = |
| 111 | + caller.memory i := by |
| 112 | + apply external_call_preserves_caller_memory_outside_output_buffer |
| 113 | + rintro ⟨h1, h2⟩ |
| 114 | + rcases hDisj with h | h <;> omega |
| 115 | + |
| 116 | +/-! ## Iterated-CALL frame theorems -/ |
| 117 | + |
| 118 | +theorem external_calls_preserve_caller_storage |
| 119 | + (caller : CallerFrame) |
| 120 | + (calls : List (Nat × Nat × CalleeResult)) |
| 121 | + (slotIdx : Nat) : |
| 122 | + (calls.foldl |
| 123 | + (fun s c => applyCallToCaller s c.1 c.2.1 c.2.2) caller).storageMap slotIdx = |
| 124 | + caller.storageMap slotIdx := by |
| 125 | + induction calls generalizing caller with |
| 126 | + | nil => rfl |
| 127 | + | cons c rest ih => |
| 128 | + have hStep := external_call_preserves_caller_storage caller c.1 c.2.1 c.2.2 slotIdx |
| 129 | + have := ih (applyCallToCaller caller c.1 c.2.1 c.2.2) |
| 130 | + simp [List.foldl]; rw [this, hStep] |
| 131 | + |
| 132 | +theorem external_calls_preserve_caller_transient_storage |
| 133 | + (caller : CallerFrame) |
| 134 | + (calls : List (Nat × Nat × CalleeResult)) |
| 135 | + (slotIdx : Nat) : |
| 136 | + (calls.foldl |
| 137 | + (fun s c => applyCallToCaller s c.1 c.2.1 c.2.2) caller).transientStorage slotIdx = |
| 138 | + caller.transientStorage slotIdx := by |
| 139 | + induction calls generalizing caller with |
| 140 | + | nil => rfl |
| 141 | + | cons c rest ih => |
| 142 | + have hStep := external_call_preserves_caller_transient_storage |
| 143 | + caller c.1 c.2.1 c.2.2 slotIdx |
| 144 | + have := ih (applyCallToCaller caller c.1 c.2.1 c.2.2) |
| 145 | + simp [List.foldl]; rw [this, hStep] |
| 146 | + |
| 147 | +theorem external_calls_preserve_caller_memory_in_disjoint_region |
| 148 | + (caller : CallerFrame) |
| 149 | + (regionLo regionHi : Nat) |
| 150 | + (calls : List (Nat × Nat × CalleeResult)) |
| 151 | + (hAllDisj : ∀ c ∈ calls, |
| 152 | + c.1 + c.2.1 ≤ regionLo ∨ regionHi ≤ c.1) |
| 153 | + (i : Nat) (hLo : regionLo ≤ i) (hHi : i < regionHi) : |
| 154 | + (calls.foldl |
| 155 | + (fun s c => applyCallToCaller s c.1 c.2.1 c.2.2) caller).memory i = |
| 156 | + caller.memory i := by |
| 157 | + induction calls generalizing caller with |
| 158 | + | nil => rfl |
| 159 | + | cons c rest ih => |
| 160 | + have hStep := external_call_preserves_caller_memory caller c.1 c.2.1 c.2.2 |
| 161 | + regionLo regionHi (hAllDisj c (List.mem_cons_self ..)) i hLo hHi |
| 162 | + have hRest : ∀ d ∈ rest, d.1 + d.2.1 ≤ regionLo ∨ regionHi ≤ d.1 := by |
| 163 | + intro d hd; exact hAllDisj d (List.mem_cons_of_mem _ hd) |
| 164 | + have hIH := ih (applyCallToCaller caller c.1 c.2.1 c.2.2) hRest |
| 165 | + simp [List.foldl]; rw [hIH, hStep] |
| 166 | + |
| 167 | +end Verity.EVM.Frame |
0 commit comments