Instances For
Equations
Instances For
def
MstoreOpcodeEquivalence.mstore_op.to_defn_Val14
(op : mstore_op)
(v14Bytes : SortBytes)
(v14Int W1 : SortInt)
:
Assigns defn_Val14 to the following propositions depending on the opcode:
«#asByteStack» W1 = some _Val14 for MSTORE
_modInt_ W1 256 = some _Val14 for MSTORE8
Equations
- MstoreOpcodeEquivalence.mstore_op.mstore.to_defn_Val14 v14Bytes v14Int W1 = (#asByteStack W1 = some v14Bytes)
- MstoreOpcodeEquivalence.mstore_op.mstore8.to_defn_Val14 v14Bytes v14Int W1 = (_modInt_ W1 256 = some v14Int)
Instances For
def
MstoreOpcodeEquivalence.mstore_op.to_defn_Val15
(op : mstore_op)
(v14Bytes _Val15 : SortBytes)
(v14Int : SortInt)
:
Assigns defn_Val15 to the following propositions depending on the opcode:
«#asByteStack» W1 = some _Val14 for MSTORE
_modInt_ W1 256 = some _Val14 for MSTORE8
Equations
- MstoreOpcodeEquivalence.mstore_op.mstore.to_defn_Val15 v14Bytes _Val15 v14Int = (#padToWidth 32 v14Bytes = some _Val15)
- MstoreOpcodeEquivalence.mstore_op.mstore8.to_defn_Val15 v14Bytes _Val15 v14Int = (buf 1 v14Int = some _Val15)
Instances For
def
MstoreOpcodeEquivalence.mstoreLHS
(op : mstore_op)
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MstoreOpcodeEquivalence.mstoreRHS
{_Val17 _Val24 _Val25 : SortInt}
{_Val16 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MstoreOpcodeEquivalence.rw_mstoreLHS_mstoreRHS
(op : mstore_op)
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 _Val0 _Val1 _Val10 _Val14mstore8 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val25 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14mstore _Val15 _Val16 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val0)
(defn_Val1 : Cmem SCHEDULE_CELL _Val0 = some _Val1)
(defn_Val2 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val2)
(defn_Val3 : «_-Int_» _Val1 _Val2 = some _Val3)
(defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4)
(defn_Val5 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val5)
(defn_Val6 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val6)
(defn_Val7 : Cmem SCHEDULE_CELL _Val6 = some _Val7)
(defn_Val8 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val8)
(defn_Val9 : «_-Int_» _Val7 _Val8 = some _Val9)
(defn_Val10 : «_-Int_» GAS_CELL _Val9 = some _Val10)
(defn_Val11 : «_<=Int_» _Val5 _Val10 = some _Val11)
(defn_Val12 : _andBool_ _Val4 _Val11 = some _Val12)
(defn_Val13 : _andBool_ USEGAS_CELL _Val12 = some _Val13)
(defn_Val14 : op.to_defn_Val14 _Val14mstore _Val14mstore8 W1)
(defn_Val15 : op.to_defn_Val15 _Val14mstore _Val15 _Val14mstore8)
(defn_Val16 : mapWriteRange LOCALMEM_CELL W0 _Val15 = some _Val16)
(defn_Val17 : «_+Int_» PC_CELL 1 = some _Val17)
(defn_Val18 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL _Val18 = some _Val19)
(defn_Val20 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val20)
(defn_Val21 : «_-Int_» _Val19 _Val20 = some _Val21)
(defn_Val22 : «_-Int_» GAS_CELL _Val21 = some _Val22)
(defn_Val23 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val23)
(defn_Val24 : «_-Int_» _Val22 _Val23 = some _Val24)
(defn_Val25 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val25)
(req : _Val13 = true)
:
theorem
MstoreOpcodeEquivalence.mstore_prestate_equiv
(op : mstore_op)
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
(symState : EvmYul.EVM.State)
:
let lhs := mstoreLHS op;
StateMap.stateMap symState lhs = { accountMap := Axioms.SortAccountsCellMap lhs.accounts, σ₀ := symState.σ₀,
totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts,
substate := StateMap.substate_map _Gen15 symState.substate, 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 := _Gen9.val, H_return := symState.H_return, pc := StateMap.intMap PC_CELL,
stack := StateMap.intMap W0 :: StateMap.intMap W1 :: StateMap.wordStackMap WS, execLength := symState.execLength }
theorem
MstoreOpcodeEquivalence.mstore_poststate_equiv
{PC_CELL _Val17 _Val24 _Val25 : SortInt}
{_Val16 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{_Val4 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
(defn_Val17 : «_+Int_» PC_CELL 1 = some _Val17)
(symState : EvmYul.EVM.State)
:
let rhs := mstoreRHS;
StateMap.stateMap symState rhs = { accountMap := Axioms.SortAccountsCellMap rhs.accounts, σ₀ := symState.σ₀,
totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts,
substate := StateMap.substate_map _Gen15 symState.substate, executionEnv := StateMap.executionEnv_map rhs symState,
blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader,
createdAccounts := symState.createdAccounts, gasAvailable := StateMap.intMap _Val24,
activeWords := StateMap.intMap rhs.memoryUsed.val, memory := StateMap.memory_map rhs.memory,
returnData := _Gen9.val, H_return := symState.H_return, pc := StateMap.intMap (PC_CELL + 1),
stack := StateMap.wordStackMap WS, execLength := symState.execLength }
theorem
MstoreOpcodeEquivalence.activeWords_eq
(op : mstore_op)
{MEMORYUSED_CELL W0 _Val25 : SortInt}
(defn_Val25 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val25)
(W0ge0 : 0 ≤ W0)
(W0small : W0 < ↑EvmYul.UInt256.size)
(mucge0 : 0 ≤ MEMORYUSED_CELL)
(mucsmall : MEMORYUSED_CELL < ↑EvmYul.UInt256.size)
:
MstoreSummary.activeWords_comp (StateMap.intMap W0) (StateMap.intMap MEMORYUSED_CELL) op.to_width = StateMap.intMap _Val25
theorem
MstoreOpcodeEquivalence.mstore_memory_write_eq
{W0 W1 : SortInt}
{LOCALMEM_CELL _Val14 _Val15 _Val16 : SortBytes}
(defn_Val14 : #asByteStack W1 = some _Val14)
(defn_Val15 : #padToWidth 32 _Val14 = some _Val15)
(defn_Val16 : mapWriteRange LOCALMEM_CELL W0 _Val15 = some _Val16)
(W0ge0 : 0 ≤ W0)
(W1ge0 : 0 ≤ W1)
(W0small : W0 < ↑EvmYul.UInt256.size)
(W1small : W1 < ↑EvmYul.UInt256.size)
(W0small_realpolitik : W0 < ↑UInt32.size)
:
theorem
MstoreOpcodeEquivalence.step_mstore_equiv
(op : mstore_op)
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 _Val0 _Val1 _Val10 _Val14mstore8 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val25 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14mstore _Val15 _Val16 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val0)
(defn_Val1 : Cmem SCHEDULE_CELL _Val0 = some _Val1)
(defn_Val2 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val2)
(defn_Val3 : «_-Int_» _Val1 _Val2 = some _Val3)
(defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4)
(defn_Val5 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val5)
(defn_Val6 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val6)
(defn_Val7 : Cmem SCHEDULE_CELL _Val6 = some _Val7)
(defn_Val8 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val8)
(defn_Val9 : «_-Int_» _Val7 _Val8 = some _Val9)
(defn_Val10 : «_-Int_» GAS_CELL _Val9 = some _Val10)
(defn_Val11 : «_<=Int_» _Val5 _Val10 = some _Val11)
(defn_Val12 : _andBool_ _Val4 _Val11 = some _Val12)
(defn_Val13 : _andBool_ USEGAS_CELL _Val12 = some _Val13)
(defn_Val14 : op.to_defn_Val14 _Val14mstore _Val14mstore8 W1)
(defn_Val15 : op.to_defn_Val15 _Val14mstore _Val15 _Val14mstore8)
(defn_Val16 : mapWriteRange LOCALMEM_CELL W0 _Val15 = some _Val16)
(defn_Val17 : «_+Int_» PC_CELL 1 = some _Val17)
(defn_Val18 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL _Val18 = some _Val19)
(defn_Val20 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val20)
(defn_Val21 : «_-Int_» _Val19 _Val20 = some _Val21)
(defn_Val22 : «_-Int_» GAS_CELL _Val21 = some _Val22)
(defn_Val23 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val23)
(defn_Val24 : «_-Int_» _Val22 _Val23 = some _Val24)
(defn_Val25 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val25)
(req : _Val13 = true)
(symState : EvmYul.EVM.State)
(gasCost : ℕ)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gavailEnough : 0 < GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size)
(pcountNonneg : 0 ≤ PC_CELL)
(W0ge0 : 0 ≤ W0)
(W1ge0 : 0 ≤ W1)
(W0small : W0 < ↑EvmYul.UInt256.size)
(W1small : W1 < ↑EvmYul.UInt256.size)
(mucge0 : 0 ≤ MEMORYUSED_CELL)
(mucsmall : MEMORYUSED_CELL < ↑EvmYul.UInt256.size)
(W0small_realpolitik : W0 < ↑UInt32.size)
:
MstoreSummary.EVM.step_mstore op.from_k (Int.toNat GAS_CELL) gasCost (StateMap.stateMap symState (mstoreLHS op)) = Except.ok
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 1 }
mstoreRHS)
theorem
MstoreOpcodeEquivalence.X_mstore_equiv
(op : mstore_op)
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 _Val0 _Val1 _Val10 _Val14mstore8 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val25 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14mstore _Val15 _Val16 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortStatusCodeCell}
{_Gen11 : SortCallStackCell}
{_Gen12 : SortInterimStatesCell}
{_Gen13 : SortTouchedAccountsCell}
{_Gen14 : SortVersionedHashesCell}
{_Gen15 : SortSubstateCell}
{_Gen16 : SortGasPriceCell}
{_Gen17 : SortOriginCell}
{_Gen18 : SortBlockhashesCell}
{_Gen19 : SortBlockCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortExitCodeCell}
{_Gen21 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortCallGasCell}
{_Gen7 : SortStaticCell}
{_Gen8 : SortCallDepthCell}
{_Gen9 : SortOutputCell}
{_K_CELL : SortK}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val0)
(defn_Val1 : Cmem SCHEDULE_CELL _Val0 = some _Val1)
(defn_Val2 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val2)
(defn_Val3 : «_-Int_» _Val1 _Val2 = some _Val3)
(defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4)
(defn_Val5 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val5)
(defn_Val6 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val6)
(defn_Val7 : Cmem SCHEDULE_CELL _Val6 = some _Val7)
(defn_Val8 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val8)
(defn_Val9 : «_-Int_» _Val7 _Val8 = some _Val9)
(defn_Val10 : «_-Int_» GAS_CELL _Val9 = some _Val10)
(defn_Val11 : «_<=Int_» _Val5 _Val10 = some _Val11)
(defn_Val12 : _andBool_ _Val4 _Val11 = some _Val12)
(defn_Val13 : _andBool_ USEGAS_CELL _Val12 = some _Val13)
(defn_Val14 : op.to_defn_Val14 _Val14mstore _Val14mstore8 W1)
(defn_Val15 : op.to_defn_Val15 _Val14mstore _Val15 _Val14mstore8)
(defn_Val16 : mapWriteRange LOCALMEM_CELL W0 _Val15 = some _Val16)
(defn_Val17 : «_+Int_» PC_CELL 1 = some _Val17)
(defn_Val18 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL _Val18 = some _Val19)
(defn_Val20 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val20)
(defn_Val21 : «_-Int_» _Val19 _Val20 = some _Val21)
(defn_Val22 : «_-Int_» GAS_CELL _Val21 = some _Val22)
(defn_Val23 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val23)
(defn_Val24 : «_-Int_» _Val22 _Val23 = some _Val24)
(defn_Val25 : #memoryUsageUpdate MEMORYUSED_CELL W0 ↑op.to_width = some _Val25)
(req : _Val13 = true)
(symState : EvmYul.EVM.State)
(symValidJumps : Array EvmYul.UInt256)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gavailEnough : 0 < GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size)
(pcountNonneg : 0 ≤ PC_CELL)
(W0ge0 : 0 ≤ W0)
(W1ge0 : 0 ≤ W1)
(W0small : W0 < ↑EvmYul.UInt256.size)
(W1small : W1 < ↑EvmYul.UInt256.size)
(mucge0 : 0 ≤ MEMORYUSED_CELL)
(mucsmall : MEMORYUSED_CELL < ↑EvmYul.UInt256.size)
(codeMstore : _Gen0 = { val := op.from_k.to_bin })
(pcZero : PC_CELL = 0)
(stackOk : List.length (StateMap.wordStackMap WS) < 1024)
(W0small_realpolitik : W0 < ↑UInt32.size)
:
EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState (mstoreLHS op)) = Except.ok
(EvmYul.EVM.ExecutionResult.success
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 2 }
mstoreRHS)
ByteArray.empty)