KEVM Interface

This file provides a proving interface for the KEVM function definitions. Some of the contents of this file may be ported to a utils file in the future.

Simple function behavior

Behavioral results about simple functions like arithmetic or boolean operations.

@[simp]

theorem KEVMInterface.plusIntIsSome {m n : SortInt} : «_+Int_» n m = some (n + m)

@[simp]

theorem KEVMInterface.subIntIsSome {m n : SortInt} : «_-Int_» n m = some (n - m)

theorem KEVMInterface.mulIntIsSome {m n : SortInt} : «_*Int_» n m = some (n * m)

theorem KEVMInterface.chopIsSome {n : SortInt} : chop n = some (n % ↑EvmYul.UInt256.size)

axiom KEVMInterface.Axioms.Keq_def (k₁ k₂ : SortK) : «_==K_» k₁ k₂ = some (k₁ == k₂)

axiom KEVMInterface.Axioms.Kneq_def (k₁ k₂ : SortK) : «_=/=K_» k₁ k₂ = some (k₁ != k₂)

@[simp]

theorem KEVMInterface.orBool_def (b₁ b₂ : SortBool) : _orBool_ b₁ b₂ = some (b₁ || b₂)

@[simp]

theorem KEVMInterface.andBool_def (b₁ b₂ : SortBool) : _andBool_ b₁ b₂ = some (b₁ && b₂)

@[simp]

theorem KEVMInterface.notBool_def (b : SortBool) : notBool_ b = some !b

@[simp]

theorem KEVMInterface.eqInt_def (n m : SortInt) : «_==Int_» n m = some (n == m)

@[simp]

theorem KEVMInterface.neqInt_def (n m : SortInt) : «_=/=Int_» n m = some (n != m)

@[simp]

theorem KEVMInterface.ltInt_def (n m : SortInt) : «_<Int_» n m = some (decide (n < m))

@[simp]

theorem KEVMInterface.kite_def {SortSort : Type} (cnd : SortBool) (true_branch false_branch : SortSort) : kite cnd true_branch false_branch = some (if cnd = true then true_branch else false_branch)

Behavior of «#sizeWordStack»

Equating #sizeWordStack to List.length.

def KEVMInterface.wsLength (ws : SortWordStack) : ℕ

Equations

• KEVMInterface.wsLength SortWordStack.«.WordStack_EVM-TYPES_WordStack» = 0
• KEVMInterface.wsLength (SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» x0 ws_2) = KEVMInterface.wsLength ws_2 + 1

theorem KEVMInterface.sizeWordStackNotEmpty {n w : SortInt} {ws : SortWordStack} : sizeWordStackAux (SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» w ws) n = sizeWordStackAux ws (n + 1)

theorem KEVMInterface.sizeWordStack_add_one {w n : SortInt} {ws : SortWordStack} : sizeWordStackAux (SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» w ws) n = do let val0 ← sizeWordStackAux ws n let val1 ← «_+Int_» val0 1 pure val1

theorem KEVMInterface.sizeWordStackAuxAdd {n : SortInt} {ws : SortWordStack} : sizeWordStackAux ws (n + 1) = do let a ← sizeWordStackAux ws n let b ← «_+Int_» a 1 pure b

theorem KEVMInterface.sizeWordStackIsSome {ws : SortWordStack} : sizeWordStackAux ws 0 = do let a ← some (wsLength ws) pure ↑a

theorem KEVMInterface.wsLength_eq_length_wordStackMap {ws : SortWordStack} : wsLength ws = List.length (StateMap.wordStackMap ws)

theorem KEVMInterface.sizeWordStack_def {ws : SortWordStack} : sizeWordStackAux ws 0 = do let a ← some (List.length (StateMap.wordStackMap ws)) pure ↑a

Behavior of K's in_keys function

Axiomatically asserting in_keys behavior.

NOTE: These functions depend on the dummy implementation as maps being List (Key × Value).

def KEVMInterface.keys {K V : Type} (l : List (K × V)) : List K

Equations

• KEVMInterface.keys l = List.map (fun (pair : K × V) => pair.1) l

def KEVMInterface.inKeys_compute (map : SortMap) (key : SortInt) : Bool

Equations

• KEVMInterface.inKeys_compute map key = List.elem (inj key) (KEVMInterface.keys map.coll)

@[simp]

axiom KEVMInterface.Axioms.inKeys_def (map : SortMap) (key : SortInt) : «_in_keys(_)_MAP_Bool_KItem_Map» (inj (inj key)) map = some (inKeys_compute map key)

Behavior of #inStorage function

This definition of #inStorage depends on the above inKeys_compute.

noncomputable def KEVMInterface.inStorage_compute (map : SortMap) (acc key : SortInt) : Bool

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem KEVMInterface.inStorage_def {ACCESSEDSTORAGE_CELL : SortMap} {ID_CELL W0 : SortInt} : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some (inStorage_compute ACCESSEDSTORAGE_CELL ID_CELL W0)

Memory results

Results that have to do with memory-related operations.

theorem KEVMInterface.memoryUsageUpdate_rw (MEMORYUSED_CELL offset width : SortInt) (width_pos : 0 < width) : #memoryUsageUpdate MEMORYUSED_CELL offset width = some (max MEMORYUSED_CELL (Int.tdiv (offset + width + 31) 32))

Explicit account for «#memoryUsageUpdate» with positive width.

theorem KEVMInterface.mapWriteRange_rw (mem content : SortBytes) (index : SortInt) : mapWriteRange mem index content = if x : index < 0 then some ByteArray.empty else if x : ByteArray.size content = 0 then some mem else have padded := («padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» mem (index + ↑(ByteArray.size content)) 0).get ⋯; «replaceAtBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Bytes» padded index content

Explicit account for mapWriteRange.

Bytes manipulation

Results to ease the reasoning about SortBytes manipulation functions.

theorem KEVMInterface.padToWidth_rw (len : SortInt) (b : SortBytes) : #padToWidth len b = if len < 0 then some b else some { data := Array.leftpad (Int.toNat len) 0 b.data }

Explicit account for «#padToWidth».

axiom KEVMInterface.Axioms.BE_IntToBytes_eq (n : ℕ) : «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness» ((↑(n + 1).log2 + 8).tdiv 8) (↑n + 1) SortEndianness.bigEndianBytes = some (BE (n + 1))

This axiom states the following:

Int2Bytes behaves as BE for positive integers and big endian representation.

Note that the first parameter of Int2Bytes is the length of the corresponding encoding sequence.

theorem KEVMInterface.asByteStack_rw {n : ℕ} : #asByteStack ↑n = some (BE n)

Explicit account for «#asByteStack».

This result notoriously depends on Axioms.BE_IntToBytes_eq, which should be a theorem at some point.

theorem KEVMInterface.padToWidth32_asByteStack_rw {n : ℕ} {b : SortBytes} (n_small : n < EvmYul.UInt256.size) (asByteStack_def : #asByteStack ↑n = some b) : #padToWidth 32 b = some (ffi.ByteArray.zeroes { toBitVec := 32#System.Platform.numBits - BitVec.ofNat System.Platform.numBits (BE n).size } ++ BE n)

Given n : ℕ with n < UInt256.size, converting it to byteStack and padding the result to width 32, is the same as UInt256.toByteArray (n : UInt256).

theorem KEVMInterface.Bytes2Int_fromByteArrayBigEndian_eq (b : ByteArray) : «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» b SortEndianness.bigEndianBytes SortSignedness.unsignedBytes = some (Int.ofNat (EvmYul.fromByteArrayBigEndian b))

For any ByteArray b, Bytes2Int b .bigEndianBytes .unsignedBytes computes the same as fromByteArrayBigEndian b.

This should be proved at some point.

theorem KEVMInterface.range_rw (b : SortBytes) (start width : SortInt) : #range b start width = if start < 0 ∨ width < 0 then some ByteArray.empty else if 0 ≤ start ∧ 0 ≤ width ∧ start < ↑(ByteArray.size b) then have len := Int.ofNat (ByteArray.size b); have pad := («padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b len 0).get ⋯; «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» pad start len else some ByteArray.empty

Friendlier interface for #range.

This should be proven at some point.

theorem KEVMInterface.chop_self_eq {LM b : SortBytes} {start n : SortInt} (defn_b : #range LM start 32 = some b) (defn_n : «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» b SortEndianness.bigEndianBytes SortSignedness.unsignedBytes = some n) : chop n = some n

Converting a 32-byte chunk of memory into an unsigned integer never overflows chop.

@[simp]

theorem KEVMInterface.asWord_empty : asWord ByteArray.empty = some 0

Misc

Miscellaneous and helpful results.

@[simp]

theorem KEVMInterface.inj_ID_CELL (ID_CELL : SortInt) : inj ID_CELL = SortAccount.inj_SortInt ID_CELL

Explicit account for the SortInt → SortAccount injection instance.