def
SloadOpcodeEquivalence.sloadLHS
{ACCESSEDSTORAGE_CELL : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
SloadOpcodeEquivalence.sloadRHS
{_Val22 : SortMap}
{ID_CELL _Val10 _Val11 _Val13 _Val14 _Val15 _Val16 _Val2 _Val3 _Val4 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{_Val0 _Val1 _Val12 _Val5 _Val6 _Val7 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val23 _Val24 _Val8 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
{_Val17 _Val19 _Val20 _Val21 : SortSet}
{_Val18 : SortKItem}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SloadOpcodeEquivalence.rw_sloadLHS_sloadRHS
{ACCESSEDSTORAGE_CELL STORAGE_CELL _Val22 : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 _Val10 _Val11 _Val13 _Val14 _Val15 _Val16 _Val2 _Val3 _Val4 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val0 _Val1 _Val12 _Val5 _Val6 _Val7 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val23 _Val24 _Val8 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
{_Val17 _Val19 _Val20 _Val21 : SortSet}
{_Val18 : SortKItem}
(defn_Val0 :
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0)
(defn_Val1 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val1)
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val3)
(defn_Val4 : kite _Val1 _Val2 _Val3 = some _Val4)
(defn_Val5 : «_<=Int_» _Val4 GAS_CELL = some _Val5)
(defn_Val6 : _andBool_ _Val0 _Val5 = some _Val6)
(defn_Val7 : _andBool_ USEGAS_CELL _Val6 = some _Val7)
(defn_Val8 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val8)
(defn_Val9 : _AccountCellMap_ _Val8 _DotVar6 = some _Val9)
(defn_Val10 : lookup STORAGE_CELL W0 = some _Val10)
(defn_Val11 : «_+Int_» PC_CELL 1 = some _Val11)
(defn_Val12 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val12)
(defn_Val13 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13)
(defn_Val14 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14)
(defn_Val15 : kite _Val12 _Val13 _Val14 = some _Val15)
(defn_Val16 : «_-Int_» GAS_CELL _Val15 = some _Val16)
(defn_Val17 : «.Set» = some _Val17)
(defn_Val18 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val17) = some _Val18)
(defn_Val19 : «project:Set» (SortK.kseq _Val18 SortK.dotk) = some _Val19)
(defn_Val20 : SetItem (inj W0) = some _Val20)
(defn_Val21 : «_|Set__SET_Set_Set_Set» _Val19 _Val20 = some _Val21)
(defn_Val22 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val21) = some _Val22)
(defn_Val23 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val23)
(defn_Val24 : _AccountCellMap_ _Val23 _DotVar6 = some _Val24)
(req : _Val7 = true)
:
theorem
SloadOpcodeEquivalence.sload_prestate_equiv
{ACCESSEDSTORAGE_CELL : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
(symState : EvmYul.EVM.State)
:
let lhs := sloadLHS;
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 lhs.refund.val, accessedAccounts := __src.accessedAccounts,
accessedStorageKeys := Axioms.SortAccessedStorageCellMap lhs.accessedStorage, logSeries := __src.logSeries },
executionEnv := StateMap.executionEnv_map lhs symState, 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 := _Gen15.val, H_return := symState.H_return,
pc := StateMap.intMap PC_CELL, stack := StateMap.intMap W0 :: StateMap.wordStackMap WS,
execLength := symState.execLength }
theorem
SloadOpcodeEquivalence.sload_poststate_equiv
{ACCESSEDSTORAGE_CELL _Val22 : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 _Val10 _Val11 _Val13 _Val14 _Val15 _Val16 _Val2 _Val3 _Val4 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{_Val0 _Val1 _Val12 _Val5 _Val6 _Val7 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val23 _Val24 _Val8 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
{_Val17 _Val19 _Val20 _Val21 : SortSet}
{_Val18 : SortKItem}
(defn_Val11 : «_+Int_» PC_CELL 1 = some _Val11)
(defn_Val12 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val12)
(defn_Val13 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13)
(defn_Val14 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14)
(defn_Val15 : kite _Val12 _Val13 _Val14 = some _Val15)
(defn_Val16 : «_-Int_» GAS_CELL _Val15 = some _Val16)
(gasEnough : _Val15 ≤ GAS_CELL)
(gasSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(symState : EvmYul.EVM.State)
:
let rhs := sloadRHS;
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 _Gen12.val, accessedAccounts := __src.accessedAccounts,
accessedStorageKeys := Axioms.SortAccessedStorageCellMap rhs.accessedStorage, logSeries := __src.logSeries },
executionEnv := StateMap.executionEnv_map rhs symState, blocks := symState.blocks,
genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts,
gasAvailable := StateMap.intMap GAS_CELL - StateMap.intMap _Val15,
activeWords := StateMap.intMap rhs.memoryUsed.val, memory := StateMap.memory_map rhs.memory,
returnData := _Gen15.val, H_return := symState.H_return, pc := StateMap.intMap (PC_CELL + 1),
stack := StateMap.intMap _Val10 :: StateMap.wordStackMap WS, execLength := symState.execLength }
theorem
SloadOpcodeEquivalence.step_sload_equiv
{ACCESSEDSTORAGE_CELL STORAGE_CELL _Val22 : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 _Val10 _Val11 _Val13 _Val14 _Val15 _Val16 _Val2 _Val3 _Val4 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val0 _Val1 _Val12 _Val5 _Val6 _Val7 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val23 _Val24 _Val8 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
{_Val17 _Val19 _Val20 _Val21 : SortSet}
{_Val18 : SortKItem}
(defn_Val0 :
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0)
(defn_Val1 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val1)
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val3)
(defn_Val4 : kite _Val1 _Val2 _Val3 = some _Val4)
(defn_Val5 : «_<=Int_» _Val4 GAS_CELL = some _Val5)
(defn_Val7 : _andBool_ USEGAS_CELL _Val6 = some _Val7)
(defn_Val8 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val8)
(defn_Val9 : _AccountCellMap_ _Val8 _DotVar6 = some _Val9)
(defn_Val10 : lookup STORAGE_CELL W0 = some _Val10)
(defn_Val11 : «_+Int_» PC_CELL 1 = some _Val11)
(defn_Val12 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val12)
(defn_Val13 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13)
(defn_Val14 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14)
(defn_Val15 : kite _Val12 _Val13 _Val14 = some _Val15)
(defn_Val16 : «_-Int_» GAS_CELL _Val15 = some _Val16)
(defn_Val17 : «.Set» = some _Val17)
(defn_Val18 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val17) = some _Val18)
(defn_Val19 : «project:Set» (SortK.kseq _Val18 SortK.dotk) = some _Val19)
(defn_Val20 : SetItem (inj W0) = some _Val20)
(defn_Val21 : «_|Set__SET_Set_Set_Set» _Val19 _Val20 = some _Val21)
(defn_Val22 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val21) = some _Val22)
(defn_Val23 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val23)
(defn_Val24 : _AccountCellMap_ _Val23 _DotVar6 = some _Val24)
(req : _Val7 = true)
(symState : EvmYul.EVM.State)
(gasCost : ℕ)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gavailEnough : _Val15 ≤ GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(gasCostValue : gasCost = Int.toNat _Val15)
(pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size)
(pcountNonneg : 0 ≤ PC_CELL)
:
SloadSummary.EVM.step_sload (Int.toNat GAS_CELL) gasCost (StateMap.stateMap symState sloadLHS) = Except.ok
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 1 }
sloadRHS)
theorem
SloadOpcodeEquivalence.X_sload_equiv
{ACCESSEDSTORAGE_CELL STORAGE_CELL _Val22 : SortMap}
{GAS_CELL ID_CELL PC_CELL W0 _Val10 _Val11 _Val13 _Val14 _Val15 _Val16 _Val2 _Val3 _Val4 : SortInt}
{K_CELL : SortK}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val0 _Val1 _Val12 _Val5 _Val6 _Val7 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar6 _Val23 _Val24 _Val8 _Val9 : SortAccountCellMap}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortSelfDestructCell}
{_Gen11 : SortLogCell}
{_Gen12 : SortRefundCell}
{_Gen13 : SortAccessedAccountsCell}
{_Gen14 : SortCreatedAccountsCell}
{_Gen15 : SortOutputCell}
{_Gen16 : SortStatusCodeCell}
{_Gen17 : SortCallStackCell}
{_Gen18 : SortInterimStatesCell}
{_Gen19 : SortTouchedAccountsCell}
{_Gen2 : SortCallerCell}
{_Gen20 : SortVersionedHashesCell}
{_Gen21 : SortGasPriceCell}
{_Gen22 : SortOriginCell}
{_Gen23 : SortBlockhashesCell}
{_Gen24 : SortBlockCell}
{_Gen25 : SortBalanceCell}
{_Gen26 : SortCodeCell}
{_Gen27 : SortOrigStorageCell}
{_Gen28 : SortTransientStorageCell}
{_Gen29 : SortNonceCell}
{_Gen3 : SortCallDataCell}
{_Gen30 : SortChainIDCell}
{_Gen31 : SortTxOrderCell}
{_Gen32 : SortTxPendingCell}
{_Gen33 : SortMessagesCell}
{_Gen34 : SortWithdrawalsPendingCell}
{_Gen35 : SortWithdrawalsOrderCell}
{_Gen36 : SortWithdrawalsCell}
{_Gen37 : SortExitCodeCell}
{_Gen38 : SortModeCell}
{_Gen4 : SortCallValueCell}
{_Gen5 : SortLocalMemCell}
{_Gen6 : SortMemoryUsedCell}
{_Gen7 : SortCallGasCell}
{_Gen8 : SortStaticCell}
{_Gen9 : SortCallDepthCell}
{_Val17 _Val19 _Val20 _Val21 : SortSet}
{_Val18 : SortKItem}
(defn_Val0 :
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag SCHEDULE_CELL = some _Val0)
(defn_Val1 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val1)
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val3)
(defn_Val4 : kite _Val1 _Val2 _Val3 = some _Val4)
(defn_Val5 : «_<=Int_» _Val4 GAS_CELL = some _Val5)
(defn_Val7 : _andBool_ USEGAS_CELL _Val6 = some _Val7)
(defn_Val8 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val8)
(defn_Val9 : _AccountCellMap_ _Val8 _DotVar6 = some _Val9)
(defn_Val10 : lookup STORAGE_CELL W0 = some _Val10)
(defn_Val11 : «_+Int_» PC_CELL 1 = some _Val11)
(defn_Val12 : #inStorage ACCESSEDSTORAGE_CELL (inj ID_CELL) W0 = some _Val12)
(defn_Val13 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13)
(defn_Val14 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14)
(defn_Val15 : kite _Val12 _Val13 _Val14 = some _Val15)
(defn_Val16 : «_-Int_» GAS_CELL _Val15 = some _Val16)
(defn_Val17 : «.Set» = some _Val17)
(defn_Val18 : «Map:lookupOrDefault» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val17) = some _Val18)
(defn_Val19 : «project:Set» (SortK.kseq _Val18 SortK.dotk) = some _Val19)
(defn_Val20 : SetItem (inj W0) = some _Val20)
(defn_Val21 : «_|Set__SET_Set_Set_Set» _Val19 _Val20 = some _Val21)
(defn_Val22 : «Map:update» ACCESSEDSTORAGE_CELL (inj ID_CELL) (inj _Val21) = some _Val22)
(defn_Val23 :
AccountCellMapItem { val := ID_CELL }
{ acctID := { val := ID_CELL }, balance := _Gen25, code := _Gen26, storage := { val := STORAGE_CELL },
origStorage := _Gen27, transientStorage := _Gen28, nonce := _Gen29 } = some _Val23)
(defn_Val24 : _AccountCellMap_ _Val23 _DotVar6 = some _Val24)
(req : _Val7 = true)
(symState : EvmYul.EVM.State)
(symValidJumps : Array EvmYul.UInt256)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gavailEnough : _Val15 < GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(codeSloadLHS : _Gen0 = { val := { data := #[84] } })
(codeSloadRHS : _Gen26 = { val := SortAccountCode.inj_SortBytes { data := #[84] } })
(pcZero : PC_CELL = 0)
(wordStackOk : sizeWordStackAux WS 0 < some 1024)
:
EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState sloadLHS) = Except.ok
(EvmYul.EVM.ExecutionResult.success
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 2 }
sloadRHS)
ByteArray.empty)