State Map

Mapping KEVM to EvmYul states.

SortGeneratedTopCell Getters

Getters for accessing cells from the Generated Top Cell.

def SortGeneratedTopCell.evm (tc : SortGeneratedTopCell) : SortEvmCell

Equations

• tc.evm = tc.kevm.ethereum.evm

def SortGeneratedTopCell.callState (tc : SortGeneratedTopCell) : SortCallStateCell

Equations

• tc.callState = tc.kevm.ethereum.evm.callState

def SortGeneratedTopCell.wordStackCell (tc : SortGeneratedTopCell) : SortWordStackCell

Equations

• tc.wordStackCell = tc.kevm.ethereum.evm.callState.wordStack

def SortGeneratedTopCell.pc (tc : SortGeneratedTopCell) : SortPcCell

Equations

• tc.pc = tc.kevm.ethereum.evm.callState.pc

def SortGeneratedTopCell.gas (tc : SortGeneratedTopCell) : SortGasCell

Equations

• tc.gas = tc.kevm.ethereum.evm.callState.gas

def SortGeneratedTopCell.program (tc : SortGeneratedTopCell) : SortProgramCell

Equations

• tc.program = tc.kevm.ethereum.evm.callState.program

def SortGeneratedTopCell.output (tc : SortGeneratedTopCell) : SortOutputCell

Equations

• tc.output = tc.kevm.ethereum.evm.output

def SortGeneratedTopCell.accessedStorage (tc : SortGeneratedTopCell) : SortAccessedStorageCell

Equations

• tc.accessedStorage = tc.kevm.ethereum.evm.substate.accessedStorage

def SortGeneratedTopCell.refund (tc : SortGeneratedTopCell) : SortRefundCell

Equations

• tc.refund = tc.kevm.ethereum.evm.substate.refund

def SortGeneratedTopCell.accounts (tc : SortGeneratedTopCell) : SortAccountsCell

Equations

• tc.accounts = tc.kevm.ethereum.network.accounts

def SortGeneratedTopCell.Iₐ (tc : SortGeneratedTopCell) : SortIdCell

Equations

• tc.Iₐ = tc.kevm.ethereum.evm.callState.id

def SortGeneratedTopCell.isStatic (tc : SortGeneratedTopCell) : SortStaticCell

Equations

• tc.isStatic = tc.kevm.ethereum.evm.callState.static

def SortGeneratedTopCell.memoryUsed (tc : SortGeneratedTopCell) : SortMemoryUsedCell

Equations

• tc.memoryUsed = tc.kevm.ethereum.evm.callState.memoryUsed

def SortGeneratedTopCell.memory (tc : SortGeneratedTopCell) : SortLocalMemCell

Equations

• tc.memory = tc.kevm.ethereum.evm.callState.localMem

def SortGeneratedTopCell.origin (tc : SortGeneratedTopCell) : SortOriginCell

Equations

• tc.origin = tc.kevm.ethereum.evm.origin

def SortGeneratedTopCell.caller (tc : SortGeneratedTopCell) : SortCallerCell

Equations

• tc.caller = tc.kevm.ethereum.evm.callState.caller

def SortGeneratedTopCell.gasPrice (tc : SortGeneratedTopCell) : SortGasPriceCell

Equations

• tc.gasPrice = tc.kevm.ethereum.evm.gasPrice

def SortGeneratedTopCell.coinbase (tc : SortGeneratedTopCell) : SortCoinbaseCell

Equations

• tc.coinbase = tc.kevm.ethereum.evm.block.coinbase

def SortGeneratedTopCell.timestamp (tc : SortGeneratedTopCell) : SortTimestampCell

Equations

• tc.timestamp = tc.kevm.ethereum.evm.block.timestamp

def SortGeneratedTopCell.mixhash (tc : SortGeneratedTopCell) : SortMixHashCell

Equations

• tc.mixhash = tc.kevm.ethereum.evm.block.mixHash

def SortGeneratedTopCell.number (tc : SortGeneratedTopCell) : SortNumberCell

Equations

• tc.number = tc.kevm.ethereum.evm.block.number

def SortGeneratedTopCell.gaslimit (tc : SortGeneratedTopCell) : SortGasLimitCell

Equations

• tc.gaslimit = tc.kevm.ethereum.evm.block.gasLimit

def SortGeneratedTopCell.chainid (tc : SortGeneratedTopCell) : SortChainIDCell

Equations

• tc.chainid = tc.kevm.ethereum.network.chainID

def SortKItem.toAccountSort (k : SortKItem) : Option SortAccount

KItem projections to subsorts

Equations

• (SortKItem.inj_SortAccount acc).toAccountSort = some acc
• k.toAccountSort = none

def SortKItem.ofAccountSort (acc : SortAccount) : SortKItem

Subsort projections to KItem

Equations

• SortKItem.ofAccountSort acc = SortKItem.inj_SortAccount acc

Type Mapping

Maps from K types to EvmYul types.

@[reducible, inline]

abbrev StateMap.intMap (n : SortInt) : EvmYul.UInt256

Equations

• StateMap.intMap n = EvmYul.UInt256.toSigned n

def StateMap.wordStackMap (ws : SortWordStack) : EvmYul.Stack EvmYul.UInt256

Equations

• StateMap.wordStackMap SortWordStack.«.WordStack_EVM-TYPES_WordStack» = []
• StateMap.wordStackMap (SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» w ws_2) = StateMap.intMap w :: StateMap.wordStackMap ws_2

def StateMap.wordStackCellMap (wsc : SortWordStackCell) : EvmYul.Stack EvmYul.UInt256

Equations

• StateMap.wordStackCellMap wsc = StateMap.wordStackMap wsc.val

def StateMap.pcCellMap (pcc : SortPcCell) : EvmYul.UInt256

Equations

• StateMap.pcCellMap pcc = StateMap.intMap pcc.val

def StateMap.gasMap : SortGas → EvmYul.UInt256

Equations

• StateMap.gasMap (SortGas.inj_SortInt g) = StateMap.intMap g

def StateMap.gasCellMap (gc : SortGasCell) : EvmYul.UInt256

Equations

• StateMap.gasCellMap gc = StateMap.gasMap gc.val

def StateMap.accountAddressMap : SortAccount → EvmYul.AccountAddress

Equations

• StateMap.accountAddressMap SortAccount.«.Account_EVM-TYPES_Account» = 0
• StateMap.accountAddressMap (SortAccount.inj_SortInt n) = EvmYul.AccountAddress.ofNat (Int.toNat n)

def StateMap.idMap (idc : SortIdCell) : EvmYul.AccountAddress

Equations

• StateMap.idMap idc = StateMap.accountAddressMap idc.val

noncomputable def StateMap.storageMap (stor : SortStorageCell) : EvmYul.Storage

Equations

• StateMap.storageMap stor = Axioms.SortStorageCellMap stor

noncomputable def StateMap.transStorageMap (tstor : SortTransientStorageCell) : EvmYul.Storage

Equations

• StateMap.transStorageMap tstor = Axioms.SortTransientStorageCellMap tstor

def StateMap.accCodeMap : SortAccountCode → ByteArray

Equations

• StateMap.accCodeMap (SortAccountCode.inj_SortBytes code) = code

noncomputable def StateMap.accountMap (acc : SortAccountCell) : EvmYul.Account

Equations

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

noncomputable def StateMap.substate_map (sc : SortSubstateCell) (s : EvmYul.Substate) : EvmYul.Substate

Equations

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

def StateMap.memory_map : SortLocalMemCell → ByteArray

Equations

• StateMap.memory_map { val := b } = b

def StateMap.blockHeader_map (tc : SortGeneratedTopCell) (s : EvmYul.EVM.State) : EvmYul.BlockHeader

Equations

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

def StateMap.executionEnv_map (tc : SortGeneratedTopCell) (s : EvmYul.EVM.State) : EvmYul.ExecutionEnv

Equations

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

State Map

The function mapping KEVM states to EvmYul states.

noncomputable def StateMap.stateMap (symState : EvmYul.EVM.State) (tc : SortGeneratedTopCell) : EvmYul.EVM.State

State Mapping: Mapping KEVM states to EvmYul states

We temporarely require the symState argument since we don't map the entire KEVM state yet

The following data structures are axiomatically mapped:

1. Substate.accessedStorageKeys: The EvmYul data representation for this is an RBSet, which is hard to reason about. The mapping will remain an axiom until a better reasoning interface is provided or we have time to implement it
2. State.accountMap: Similar reasons as above

Equations

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

State Mapping Results

Theorems to make life easier.

theorem StateMap.intMap_sub_dist {n m : SortInt} (le_m_n : m ≤ n) (pos : 0 ≤ m) (size : n < ↑EvmYul.UInt256.size) : intMap (n - m) = intMap n - intMap m

theorem StateMap.intMap_add_dist {n m : SortInt} (nh : 0 ≤ n) (mh : 0 ≤ m) : intMap ((n + m) % ↑EvmYul.UInt256.size) = intMap n + intMap m

theorem StateMap.intMap_toNat {n : SortInt} (nh : 0 ≤ n) (size : n < ↑EvmYul.UInt256.size) : (intMap n).toNat = Int.toNat n

State Map Axioms

Axioms that have to do with the axiomatic state mapping.

axiom Axioms.findAccountInAccountCellMap {ID_CELL : SortInt} {balance : SortBalanceCell} {code : SortCodeCell} {STORAGE_CELL ORIG_STORAGE_CELL : SortMap} {tstorage : SortTransientStorageCell} {nonce : SortNonceCell} {accCellMap dotVar accCellMap2 : SortAccountCellMap} (accCellMap_def : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce } = some accCellMap) (accCellMap2_def : _AccountCellMap_ accCellMap dotVar = some accCellMap2) : Batteries.RBMap.find? (SortAccountsCellMap { val := accCellMap2 }) (EvmYul.AccountAddress.ofNat (Int.toNat ID_CELL)) = some (StateMap.accountMap { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce })

This axiom states that if an account is in an AccountCellMap, then Batteries.RBMap.find? finds it in the image of the axiomatized mapping

The second element of AccountCellMapItem is provided embedded in accCellMap_def for ease of use when proving theorems

axiom Axioms.accountsCell_map_find? {ID_CELL : SortInt} {balance : SortBalanceCell} {code : SortCodeCell} {STORAGE_CELL ORIG_STORAGE_CELL : SortMap} {tstorage : SortTransientStorageCell} {nonce : SortNonceCell} {accCellMap dotVar accCellMap2 : SortAccountCellMap} (acc : SortAccountCell) (acc_def : acc = { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce }) (accCellMap_def : AccountCellMapItem { val := ID_CELL } acc = some accCellMap) (accCellMap2_def : _AccountCellMap_ accCellMap dotVar = some accCellMap2) : Batteries.RBMap.find? (SortAccountsCellMap { val := accCellMap2 }) (EvmYul.AccountAddress.ofNat (Int.toNat ID_CELL)) = some (StateMap.accountMap acc)

Expected behavior of SortAccountsCellMap w.r.t. Batteries.RBMap.find?

This axiom states that

• Given an accountsCell (accCellMap2) containing an account identifiable by ID_CELL (acc)
• The (axiomatic) mapping of accCellMap2 contains the mapping of acc
• And, in particular, RBMap.find? correctly finds the mapped acc if provided with the mapped ID_CELL

axiom Axioms.accountsCell_map_insert {ID_CELL key value : SortInt} {balance : SortBalanceCell} {code : SortCodeCell} {tstorage : SortTransientStorageCell} {nonce : SortNonceCell} {ACCESSEDSTORAGE_CELL ORIG_STORAGE_CELL STORAGE_CELL stor_update : SortMap} {emptySet kitemToSet keySet fullSet : SortSet} {kitemLookup : SortKItem} {dotvar initAccount initCellMap updatedAccount updatedCellMap : SortAccountCellMap} (defn_Val34 : «.Set» = some emptySet) (defn_Val35 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj emptySet) = some kitemLookup) (defn_Val36 : «project:Set» (SortK.kseq kitemLookup SortK.dotk) = some kitemToSet) (defn_Val37 : SetItem (inj key) = some keySet) (defn_Val38 : «_|Set__SET_Set_Set_Set» kitemToSet keySet = some fullSet) (defn_Val40 : «Map:update» STORAGE_CELL (inj key) (inj value) = some stor_update) (defn_Val41 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := stor_update }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce } = some updatedAccount) (defn_Val42 : _AccountCellMap_ updatedAccount dotvar = some updatedCellMap) (defn_Val19 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce } = some initAccount) (defn_Val20 : _AccountCellMap_ initAccount dotvar = some initCellMap) : Batteries.RBMap.insert (SortAccountsCellMap { val := initCellMap }) (StateMap.accountAddressMap (inj ID_CELL)) ((StateMap.accountMap { acctID := { val := ID_CELL }, balance := balance, code := code, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := tstorage, nonce := nonce }).updateStorage (StateMap.intMap key) (StateMap.intMap value)) = SortAccountsCellMap { val := updatedCellMap }

Expected behavior of SortAccountsCellMap w.r.t. Batteries.RBMap.insert

This axiom states that

• Given an accountsCell (initCellMap) containing an account identifiable by ID_CELL (initAccount) with symbolic storage STORAGE_CELL
• Given an updated accountsCell (updatedCellMap) consisting of initAccount with an updated STORAGE_CELL which contains the symbolic (key, value) pair (stor_update)
• RBMap.inserting the mapped (key, value) pair into the (axiomatically) mapped initCellMap equals to the (axiomatic) mapping of updatedCellMap

axiom Axioms.accessedStorageCell_map_insert {ID_CELL key : SortInt} {ACCESSEDSTORAGE_CELL stor_update : SortMap} {emptySet kitemToSet keySet fullSet : SortSet} {kitemLookup : SortKItem} (defn_Val34 : «.Set» = some emptySet) (defn_Val35 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj emptySet) = some kitemLookup) (defn_Val36 : «project:Set» (SortK.kseq kitemLookup SortK.dotk) = some kitemToSet) (defn_Val37 : SetItem (inj key) = some keySet) (defn_Val38 : «_|Set__SET_Set_Set_Set» kitemToSet keySet = some fullSet) (defn_Val39 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj fullSet) = some stor_update) : (SortAccessedStorageCellMap { val := ACCESSEDSTORAGE_CELL }).insert (EvmYul.AccountAddress.ofNat (Int.toNat ID_CELL), StateMap.intMap key) = SortAccessedStorageCellMap { val := stor_update }

Expected behavior of SortAccessedStorageCellMap w.r.t. Batteries.RBSet.insert

This axiom states that

• Given a symbolic map of accessed storage keys ACCESSEDSTORAGE_CELL
• Given an update of ACCESSEDSTORAGE_CELL containing the account ID_CELL and the key key (stor_update)
• RBMap.inserting the mapped pair (ID_CELL, key) into the (axiomatically) mapped ACCESSEDSTORAGE_CELL equals to the (axiomatic) mapping of stor_update

axiom Axioms.lookup_mapped_storage (storage : SortMap) (key result : SortInt) : lookup storage key = some result → Batteries.RBMap.findD (SortStorageCellMap { val := storage }) (StateMap.intMap key) { val := 0 } = StateMap.intMap result

Mapping a SortStorageCell through Axioms.SortStorageCellMap results in an equivalence of behavior between K's lookup function and EvmYul's findD. Provided that lookup results in some result.

axiom Axioms.contains_accessedStorage_map {contained : Bool} {stor : SortMap} {acc key : SortInt} : #inStorage stor (SortAccount.inj_SortInt acc) key = some contained → (SortAccessedStorageCellMap { val := stor }).contains (EvmYul.AccountAddress.ofNat (Int.toNat acc), StateMap.intMap key) = contained

Mapping a SortAccessedStorageCell through Axioms.SortAccessedStorageCellMap results in an equivalence of behavior between K's «#inStorage» function and EvmYul's RBSet.contains.