def SstoreOpcodeEquivalence.sstoreLHS {ACCESSEDSTORAGE_CELL : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val20 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} : SortGeneratedTopCell

Equations

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

def SstoreOpcodeEquivalence.sstoreRHS {_Val39 _Val40 : SortMap} {ID_CELL _Val1 _Val10 _Val11 _Val13 _Val2 _Val21 _Val22 _Val23 _Val24 _Val25 _Val27 _Val28 _Val29 _Val3 _Val30 _Val31 _Val32 _Val33 _Val6 _Val7 _Val8 _Val9 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {_Val0 _Val12 _Val14 _Val15 _Val16 _Val17 _Val18 _Val26 _Val4 _Val5 : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val19 _Val20 _Val41 _Val42 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} {_Val34 _Val36 _Val37 _Val38 : SortSet} {_Val35 : SortKItem} : SortGeneratedTopCell

Equations

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

theorem SstoreOpcodeEquivalence.rw_sstoreLHS_sstoreRHS {ACCESSEDSTORAGE_CELL ORIG_STORAGE_CELL STORAGE_CELL _Val39 _Val40 : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 _Val1 _Val10 _Val11 _Val13 _Val2 _Val21 _Val22 _Val23 _Val24 _Val25 _Val27 _Val28 _Val29 _Val3 _Val30 _Val31 _Val32 _Val33 _Val6 _Val7 _Val8 _Val9 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val12 _Val14 _Val15 _Val16 _Val17 _Val18 _Val26 _Val4 _Val5 : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val19 _Val20 _Val41 _Val42 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} {K_CELL : SortK} {_Val34 _Val36 _Val37 _Val38 : SortSet} {_Val35 : SortKItem} (defn_Val0 : «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0) (defn_Val1 : lookup STORAGE_CELL W0 = some _Val1) (defn_Val2 : lookup ORIG_STORAGE_CELL W0 = some _Val2) (defn_Val3 : Csstore SCHEDULE_CELL W1 _Val1 _Val2 = some _Val3) (defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4) (defn_Val5 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val6) (defn_Val7 : kite _Val5 0 _Val6 = some _Val7) (defn_Val8 : lookup STORAGE_CELL W0 = some _Val8) (defn_Val9 : lookup ORIG_STORAGE_CELL W0 = some _Val9) (defn_Val10 : Csstore SCHEDULE_CELL W1 _Val8 _Val9 = some _Val10) (defn_Val11 : «_-Int_» GAS_CELL _Val10 = some _Val11) (defn_Val12 : «_<=Int_» _Val7 _Val11 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcallstipend_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<Int_» _Val13 GAS_CELL = some _Val14) (defn_Val15 : _andBool_ _Val12 _Val14 = some _Val15) (defn_Val16 : _andBool_ _Val4 _Val15 = some _Val16) (defn_Val17 : _andBool_ _Val0 _Val16 = some _Val17) (defn_Val18 : _andBool_ USEGAS_CELL _Val17 = some _Val18) (defn_Val19 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val19) (defn_Val20 : _AccountCellMap_ _Val19 _DotVar6 = some _Val20) (defn_Val21 : «_+Int_» PC_CELL 1 = some _Val21) (defn_Val22 : lookup STORAGE_CELL W0 = some _Val22) (defn_Val23 : lookup ORIG_STORAGE_CELL W0 = some _Val23) (defn_Val24 : Csstore SCHEDULE_CELL W1 _Val22 _Val23 = some _Val24) (defn_Val25 : «_-Int_» GAS_CELL _Val24 = some _Val25) (defn_Val26 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val26) (defn_Val27 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val27) (defn_Val28 : kite _Val26 0 _Val27 = some _Val28) (defn_Val29 : «_-Int_» _Val25 _Val28 = some _Val29) (defn_Val30 : lookup STORAGE_CELL W0 = some _Val30) (defn_Val31 : lookup ORIG_STORAGE_CELL W0 = some _Val31) (defn_Val32 : Rsstore SCHEDULE_CELL W1 _Val30 _Val31 = some _Val32) (defn_Val33 : «_+Int_» REFUND_CELL _Val32 = some _Val33) (defn_Val34 : «.Set» = some _Val34) (defn_Val35 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val34) = some _Val35) (defn_Val36 : «project:Set» (SortK.kseq _Val35 SortK.dotk) = some _Val36) (defn_Val37 : SetItem (inj W0) = some _Val37) (defn_Val38 : «_|Set__SET_Set_Set_Set» _Val36 _Val37 = some _Val38) (defn_Val39 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val38) = some _Val39) (defn_Val40 : «Map:update» STORAGE_CELL (inj W0) (inj W1) = some _Val40) (defn_Val41 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := _Val40 }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val41) (defn_Val42 : _AccountCellMap_ _Val41 _DotVar6 = some _Val42) (req : _Val18 = true) : Rewrites sstoreLHS sstoreRHS

theorem SstoreOpcodeEquivalence.sstore_prestate_equiv {ACCESSEDSTORAGE_CELL : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val20 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} (symState : EvmYul.EVM.State) : let lhs := sstoreLHS; StateMap.stateMap symState lhs = { accountMap := Axioms.SortAccountsCellMap lhs.accounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := StateMap.intMap REFUND_CELL, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := Axioms.SortAccessedStorageCellMap lhs.accessedStorage, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := StateMap.accountAddressMap (inj ID_CELL), sender := StateMap.accountAddressMap lhs.origin.val, source := StateMap.accountAddressMap lhs.caller.val, weiValue := __src.weiValue, inputData := __src.inputData, code := _Gen0.val, gasPrice := Int.toNat lhs.gasPrice.val, header := StateMap.blockHeader_map lhs symState, depth := __src.depth, perm := true, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := StateMap.intMap GAS_CELL, activeWords := StateMap.intMap lhs.memoryUsed.val, memory := StateMap.memory_map lhs.memory, returnData := _Gen13.val, H_return := symState.H_return, pc := StateMap.intMap PC_CELL, stack := StateMap.intMap W0 :: StateMap.intMap W1 :: StateMap.wordStackMap WS, execLength := symState.execLength }

def SstoreOpcodeEquivalence.Csstore_compute (value stor_val ostor_val : SortInt) : SortInt

Equations

• SstoreOpcodeEquivalence.Csstore_compute value stor_val ostor_val = if stor_val = value ∨ ¬ostor_val = stor_val then 100 else if ostor_val = 0 then 20000 else 2900

@[simp]

theorem SstoreOpcodeEquivalence.Csstore_def {value stor_val ostor_val : SortInt} : Csstore SortSchedule.CANCUN_EVM value stor_val ostor_val = some (Csstore_compute value stor_val ostor_val)

noncomputable def SstoreOpcodeEquivalence.sstore_gas (map : SortMap) (value stor_val ostor_val acc key : SortInt) : SortInt

Remaining gas after deducting to gas the cost of executing sstore

• map will be the accessed storage map
• value is the stored value
• stor_val is the current value in storage
• ostor_val is the value from the origin storage
• acc is the account in question
• key is where the value will be stored

The addition is because this whole expression is to be deducted from the current gas available

Equations

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

theorem SstoreOpcodeEquivalence.sstore_gas_pos (map : SortMap) (value stor_val ostor_val acc key : SortInt) : 0 < sstore_gas map value stor_val ostor_val acc key

def SstoreOpcodeEquivalence.rsstore (new current original : SortInt) : SortInt

Computational content of GAS_FEES_Rsstore_new The function is named rsstore instead of rsstore_new because if the schedule is Cancun, Rsstore equates to this function

Equations

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

theorem SstoreOpcodeEquivalence.rsstore_new_def {new current original : SortInt} {sched : SortSchedule} (h : sched = SortSchedule.CANCUN_EVM) : GAS_FEES_Rsstore_new sched new current original = some (rsstore new current original)

theorem SstoreOpcodeEquivalence.rsstore_def {new current original : SortInt} {sched : SortSchedule} (h : sched = SortSchedule.CANCUN_EVM) : Rsstore sched new current original = some (rsstore new current original)

Rsstore is GAS_FEES_Rsstore_new when schedule is .CANCUN_EVM

theorem SstoreOpcodeEquivalence.Aᵣ_rsstore_eq (symRefund key : EvmYul.UInt256) (symCode : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner : EvmYul.AccountAddress) {new : SortInt} {symState : EvmYul.State} (owner_exists : ¬Batteries.RBMap.find? symAccounts symCodeOwner = none) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := __src.sender, source := __src.source, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := __src.gasPrice, header := __src.header, depth := __src.depth, perm := __src.perm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts }; SstoreSummary.Aᵣ_sstore { accountMap := SstoreSummary.accountMap_sstore ss key (StateMap.intMap new), σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := SstoreSummary.Aᵣ_sstore ss key (StateMap.intMap new), accessedAccounts := __src.accessedAccounts, accessedStorageKeys := SstoreSummary.accessedStorageKeys_sstore symState key, logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts } key (StateMap.intMap new) = symRefund + StateMap.intMap (rsstore new (Int.ofNat ↑(Batteries.RBMap.findD (Batteries.RBMap.find! symState.accountMap symCodeOwner).storage key { val := 0 }).val) (Int.ofNat ↑(Batteries.RBMap.findD (Batteries.RBMap.find! symState.σ₀ symCodeOwner).storage key { val := 0 }).val))

theorem SstoreOpcodeEquivalence.sstore_poststate_equiv {ACCESSEDSTORAGE_CELL _Val39 _Val40 : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 _Val1 _Val10 _Val11 _Val13 _Val2 _Val21 _Val22 _Val23 _Val24 _Val25 _Val27 _Val28 _Val29 _Val3 _Val30 _Val31 _Val32 _Val33 _Val6 _Val7 _Val8 _Val9 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {_Val0 _Val12 _Val14 _Val15 _Val16 _Val17 _Val18 _Val26 _Val4 _Val5 : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val19 _Val20 _Val41 _Val42 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} {_Val34 _Val36 _Val37 _Val38 : SortSet} {_Val35 : SortKItem} (defn_Val21 : «_+Int_» PC_CELL 1 = some _Val21) (defn_Val24 : Csstore SCHEDULE_CELL W1 _Val22 _Val23 = some _Val24) (defn_Val25 : «_-Int_» GAS_CELL _Val24 = some _Val25) (defn_Val26 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val26) (defn_Val27 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val27) (defn_Val28 : kite _Val26 0 _Val27 = some _Val28) (defn_Val29 : «_-Int_» _Val25 _Val28 = some _Val29) (defn_Val33 : «_+Int_» REFUND_CELL _Val32 = some _Val33) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (symState : EvmYul.EVM.State) : let rhs := sstoreRHS; StateMap.stateMap symState rhs = { accountMap := Axioms.SortAccountsCellMap rhs.accounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := StateMap.intMap (REFUND_CELL + _Val32), accessedAccounts := __src.accessedAccounts, accessedStorageKeys := Axioms.SortAccessedStorageCellMap rhs.accessedStorage, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := StateMap.accountAddressMap (inj ID_CELL), sender := StateMap.accountAddressMap rhs.origin.val, source := StateMap.accountAddressMap rhs.caller.val, weiValue := __src.weiValue, inputData := __src.inputData, code := _Gen0.val, gasPrice := Int.toNat rhs.gasPrice.val, header := StateMap.blockHeader_map rhs symState, depth := __src.depth, perm := true, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := StateMap.intMap (GAS_CELL - sstore_gas ACCESSEDSTORAGE_CELL W1 _Val22 _Val23 ID_CELL W0), activeWords := StateMap.intMap rhs.memoryUsed.val, memory := StateMap.memory_map rhs.memory, returnData := _Gen13.val, H_return := symState.H_return, pc := StateMap.intMap (PC_CELL + 1), stack := StateMap.wordStackMap WS, execLength := symState.execLength }

theorem SstoreOpcodeEquivalence.step_sstore_equiv {ACCESSEDSTORAGE_CELL ORIG_STORAGE_CELL STORAGE_CELL _Val39 _Val40 : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 _Val1 _Val10 _Val11 _Val13 _Val2 _Val21 _Val22 _Val23 _Val24 _Val25 _Val27 _Val28 _Val29 _Val3 _Val30 _Val31 _Val32 _Val33 _Val6 _Val7 _Val8 _Val9 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val12 _Val14 _Val15 _Val16 _Val17 _Val18 _Val26 _Val4 _Val5 : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val19 _Val20 _Val41 _Val42 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} {_Val34 _Val36 _Val37 _Val38 : SortSet} {_Val35 : SortKItem} (defn_Val0 : «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0) (defn_Val1 : lookup STORAGE_CELL W0 = some _Val1) (defn_Val2 : lookup ORIG_STORAGE_CELL W0 = some _Val2) (defn_Val3 : Csstore SCHEDULE_CELL W1 _Val1 _Val2 = some _Val3) (defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4) (defn_Val5 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val6) (defn_Val7 : kite _Val5 0 _Val6 = some _Val7) (defn_Val8 : lookup STORAGE_CELL W0 = some _Val8) (defn_Val9 : lookup ORIG_STORAGE_CELL W0 = some _Val9) (defn_Val10 : Csstore SCHEDULE_CELL W1 _Val8 _Val9 = some _Val10) (defn_Val11 : «_-Int_» GAS_CELL _Val10 = some _Val11) (defn_Val12 : «_<=Int_» _Val7 _Val11 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcallstipend_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<Int_» _Val13 GAS_CELL = some _Val14) (defn_Val15 : _andBool_ _Val12 _Val14 = some _Val15) (defn_Val16 : _andBool_ _Val4 _Val15 = some _Val16) (defn_Val17 : _andBool_ _Val0 _Val16 = some _Val17) (defn_Val18 : _andBool_ USEGAS_CELL _Val17 = some _Val18) (defn_Val19 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val19) (defn_Val20 : _AccountCellMap_ _Val19 _DotVar6 = some _Val20) (defn_Val21 : «_+Int_» PC_CELL 1 = some _Val21) (defn_Val22 : lookup STORAGE_CELL W0 = some _Val22) (defn_Val23 : lookup ORIG_STORAGE_CELL W0 = some _Val23) (defn_Val24 : Csstore SCHEDULE_CELL W1 _Val22 _Val23 = some _Val24) (defn_Val25 : «_-Int_» GAS_CELL _Val24 = some _Val25) (defn_Val26 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val26) (defn_Val27 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val27) (defn_Val28 : kite _Val26 0 _Val27 = some _Val28) (defn_Val29 : «_-Int_» _Val25 _Val28 = some _Val29) (defn_Val30 : lookup STORAGE_CELL W0 = some _Val30) (defn_Val31 : lookup ORIG_STORAGE_CELL W0 = some _Val31) (defn_Val32 : Rsstore SCHEDULE_CELL W1 _Val30 _Val31 = some _Val32) (defn_Val33 : «_+Int_» REFUND_CELL _Val32 = some _Val33) (defn_Val34 : «.Set» = some _Val34) (defn_Val35 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val34) = some _Val35) (defn_Val36 : «project:Set» (SortK.kseq _Val35 SortK.dotk) = some _Val36) (defn_Val37 : SetItem (inj W0) = some _Val37) (defn_Val38 : «_|Set__SET_Set_Set_Set» _Val36 _Val37 = some _Val38) (defn_Val39 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val38) = some _Val39) (defn_Val40 : «Map:update» STORAGE_CELL (inj W0) (inj W1) = some _Val40) (defn_Val41 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := _Val40 }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val41) (defn_Val42 : _AccountCellMap_ _Val41 _DotVar6 = some _Val42) (req : _Val18 = true) (symState : EvmYul.EVM.State) (gasCost : ℕ) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (gavailEnough : sstore_gas ACCESSEDSTORAGE_CELL W1 _Val22 _Val23 ID_CELL W0 ≤ GAS_CELL) (gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size) (gasCostValue : ↑gasCost = sstore_gas ACCESSEDSTORAGE_CELL W1 _Val22 _Val23 ID_CELL W0) (pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size) (pcountNonneg : 0 ≤ PC_CELL) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) (ID_CELLSize : Int.toNat ID_CELL < EvmYul.AccountAddress.size) : SstoreSummary.EVM.step_sstore (Int.toNat GAS_CELL) gasCost (StateMap.stateMap symState sstoreLHS) = Except.ok (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 } sstoreRHS)

theorem SstoreOpcodeEquivalence.X_sstore_equiv {ACCESSEDSTORAGE_CELL ORIG_STORAGE_CELL STORAGE_CELL _Val39 _Val40 : SortMap} {GAS_CELL ID_CELL PC_CELL REFUND_CELL W0 W1 _Val1 _Val10 _Val11 _Val13 _Val2 _Val21 _Val22 _Val23 _Val24 _Val25 _Val27 _Val28 _Val29 _Val3 _Val30 _Val31 _Val32 _Val33 _Val6 _Val7 _Val8 _Val9 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val12 _Val14 _Val15 _Val16 _Val17 _Val18 _Val26 _Val4 _Val5 : SortBool} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar6 _Val19 _Val20 _Val41 _Val42 : SortAccountCellMap} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortLogCell} {_Gen11 : SortAccessedAccountsCell} {_Gen12 : SortCreatedAccountsCell} {_Gen13 : SortOutputCell} {_Gen14 : SortStatusCodeCell} {_Gen15 : SortCallStackCell} {_Gen16 : SortInterimStatesCell} {_Gen17 : SortTouchedAccountsCell} {_Gen18 : SortVersionedHashesCell} {_Gen19 : SortGasPriceCell} {_Gen2 : SortCallerCell} {_Gen20 : SortOriginCell} {_Gen21 : SortBlockhashesCell} {_Gen22 : SortBlockCell} {_Gen23 : SortBalanceCell} {_Gen24 : SortCodeCell} {_Gen25 : SortTransientStorageCell} {_Gen26 : SortNonceCell} {_Gen27 : SortChainIDCell} {_Gen28 : SortTxOrderCell} {_Gen29 : SortTxPendingCell} {_Gen3 : SortCallDataCell} {_Gen30 : SortMessagesCell} {_Gen31 : SortWithdrawalsPendingCell} {_Gen32 : SortWithdrawalsOrderCell} {_Gen33 : SortWithdrawalsCell} {_Gen34 : SortExitCodeCell} {_Gen35 : SortModeCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortCallDepthCell} {_Gen9 : SortSelfDestructCell} {_Val34 _Val36 _Val37 _Val38 : SortSet} {_Val35 : SortKItem} (defn_Val0 : «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0) (defn_Val1 : lookup STORAGE_CELL W0 = some _Val1) (defn_Val2 : lookup ORIG_STORAGE_CELL W0 = some _Val2) (defn_Val3 : Csstore SCHEDULE_CELL W1 _Val1 _Val2 = some _Val3) (defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4) (defn_Val5 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val6) (defn_Val7 : kite _Val5 0 _Val6 = some _Val7) (defn_Val8 : lookup STORAGE_CELL W0 = some _Val8) (defn_Val9 : lookup ORIG_STORAGE_CELL W0 = some _Val9) (defn_Val10 : Csstore SCHEDULE_CELL W1 _Val8 _Val9 = some _Val10) (defn_Val11 : «_-Int_» GAS_CELL _Val10 = some _Val11) (defn_Val12 : «_<=Int_» _Val7 _Val11 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcallstipend_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<Int_» _Val13 GAS_CELL = some _Val14) (defn_Val15 : _andBool_ _Val12 _Val14 = some _Val15) (defn_Val16 : _andBool_ _Val4 _Val15 = some _Val16) (defn_Val17 : _andBool_ _Val0 _Val16 = some _Val17) (defn_Val18 : _andBool_ USEGAS_CELL _Val17 = some _Val18) (defn_Val19 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := STORAGE_CELL }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val19) (defn_Val20 : _AccountCellMap_ _Val19 _DotVar6 = some _Val20) (defn_Val21 : «_+Int_» PC_CELL 1 = some _Val21) (defn_Val22 : lookup STORAGE_CELL W0 = some _Val22) (defn_Val23 : lookup ORIG_STORAGE_CELL W0 = some _Val23) (defn_Val24 : Csstore SCHEDULE_CELL W1 _Val22 _Val23 = some _Val24) (defn_Val25 : «_-Int_» GAS_CELL _Val24 = some _Val25) (defn_Val26 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val26) (defn_Val27 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val27) (defn_Val28 : kite _Val26 0 _Val27 = some _Val28) (defn_Val29 : «_-Int_» _Val25 _Val28 = some _Val29) (defn_Val30 : lookup STORAGE_CELL W0 = some _Val30) (defn_Val31 : lookup ORIG_STORAGE_CELL W0 = some _Val31) (defn_Val32 : Rsstore SCHEDULE_CELL W1 _Val30 _Val31 = some _Val32) (defn_Val33 : «_+Int_» REFUND_CELL _Val32 = some _Val33) (defn_Val34 : «.Set» = some _Val34) (defn_Val35 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val34) = some _Val35) (defn_Val36 : «project:Set» (SortK.kseq _Val35 SortK.dotk) = some _Val36) (defn_Val37 : SetItem (inj W0) = some _Val37) (defn_Val38 : «_|Set__SET_Set_Set_Set» _Val36 _Val37 = some _Val38) (defn_Val39 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val38) = some _Val39) (defn_Val40 : «Map:update» STORAGE_CELL (inj W0) (inj W1) = some _Val40) (defn_Val41 : AccountCellMapItem { val := ID_CELL } { acctID := { val := ID_CELL }, balance := _Gen23, code := _Gen24, storage := { val := _Val40 }, origStorage := { val := ORIG_STORAGE_CELL }, transientStorage := _Gen25, nonce := _Gen26 } = some _Val41) (defn_Val42 : _AccountCellMap_ _Val41 _DotVar6 = some _Val42) (req : _Val18 = true) (symState : EvmYul.EVM.State) (symValidJumps : Array EvmYul.UInt256) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (gavailEnough : sstore_gas ACCESSEDSTORAGE_CELL W1 _Val22 _Val23 ID_CELL W0 ≤ GAS_CELL) (gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size) (codeSstoreLHS : _Gen0 = { val := { data := #[85] } }) (codeSstoreRHS : _Gen24 = { val := SortAccountCode.inj_SortBytes { data := #[85] } }) (pcZero : PC_CELL = 0) (key_pos : 0 ≤ W0) (val_pos : 0 ≤ W1) (ID_CELLSize : Int.toNat ID_CELL < EvmYul.AccountAddress.size) (stackOk : List.length (StateMap.wordStackMap WS) < 1024) (callStipendGas : GasConstants.Gcallstipend < (StateMap.intMap GAS_CELL).toNat) : EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState sstoreLHS) = Except.ok (EvmYul.EVM.ExecutionResult.success (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 2 } sstoreRHS) ByteArray.empty)