def
MloadOpcodeEquivalence.mloadLHS
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{_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}
{_WS : SortWordStack}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MloadOpcodeEquivalence.mloadRHS
{_Val15 _Val16 _Val23 _Val24 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{_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}
{_WS : SortWordStack}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MloadOpcodeEquivalence.rw_mloadLHS_mloadRHS
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 _Val0 _Val1 _Val10 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{_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}
{_WS : SortWordStack}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = 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 32 = 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 : #range LOCALMEM_CELL W0 32 = some _Val14)
(defn_Val15 : asWord _Val14 = some _Val15)
(defn_Val16 : «_+Int_» PC_CELL 1 = some _Val16)
(defn_Val17 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val17)
(defn_Val18 : Cmem SCHEDULE_CELL _Val17 = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val19)
(defn_Val20 : «_-Int_» _Val18 _Val19 = some _Val20)
(defn_Val21 : «_-Int_» GAS_CELL _Val20 = some _Val21)
(defn_Val22 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val22)
(defn_Val23 : «_-Int_» _Val21 _Val22 = some _Val23)
(defn_Val24 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val24)
(req : _Val13 = true)
:
theorem
MloadOpcodeEquivalence.mload_prestate_equiv
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{_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}
{_WS : SortWordStack}
(symState : EvmYul.EVM.State)
:
let lhs := mloadLHS;
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.wordStackMap _WS, execLength := symState.execLength }
theorem
MloadOpcodeEquivalence.mload_poststate_equiv
{PC_CELL _Val15 _Val16 _Val23 _Val24 : SortInt}
{LOCALMEM_CELL : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{_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}
{_WS : SortWordStack}
(defn_Val16 : «_+Int_» PC_CELL 1 = some _Val16)
(symState : EvmYul.EVM.State)
:
let rhs := mloadRHS;
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 _Val23,
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.intMap _Val15 :: StateMap.wordStackMap _WS, execLength := symState.execLength }
theorem
MloadOpcodeEquivalence.range_lookupMemory_eq
{LOCALMEM_CELL _Val14 : SortBytes}
{W0 MEMORYUSED_CELL _Val15 : SortInt}
(defn_Val14 : #range LOCALMEM_CELL W0 32 = some _Val14)
(defn_Val15 : asWord _Val14 = some _Val15)
(W0ge0 : 0 ≤ W0)
(W0small : W0 < ↑EvmYul.UInt256.size)
:
(if ByteArray.size LOCALMEM_CELL ≤ (StateMap.intMap W0).toNat ∨ StateMap.intMap MEMORYUSED_CELL * { val := 32 } ≤ StateMap.intMap W0 then
{ val := 0 }
else EvmYul.UInt256.ofNat
(EvmYul.fromByteArrayBigEndian (ByteArray.readWithPadding LOCALMEM_CELL (StateMap.intMap W0).toNat 32))) = StateMap.intMap _Val15
Theorem stating that asWord (#range LM W0 32) = LM.lookupMemory W0
MachineState.lookupMemory is simped to abstract the rest of the MachineState
theorem
MloadOpcodeEquivalence.EVM.step_mload_equiv
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 _Val0 _Val1 _Val10 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{_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}
{_WS : SortWordStack}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = 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 32 = 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 : #range LOCALMEM_CELL W0 32 = some _Val14)
(defn_Val15 : asWord _Val14 = some _Val15)
(defn_Val16 : «_+Int_» PC_CELL 1 = some _Val16)
(defn_Val17 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val17)
(defn_Val18 : Cmem SCHEDULE_CELL _Val17 = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val19)
(defn_Val20 : «_-Int_» _Val18 _Val19 = some _Val20)
(defn_Val21 : «_-Int_» GAS_CELL _Val20 = some _Val21)
(defn_Val22 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val22)
(defn_Val23 : «_-Int_» _Val21 _Val22 = some _Val23)
(defn_Val24 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val24)
(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)
(W0small : W0 < ↑EvmYul.UInt256.size)
(mucge0 : 0 ≤ MEMORYUSED_CELL)
(mucsmall : MEMORYUSED_CELL < ↑EvmYul.UInt256.size)
(W0small_realpolitik : W0 < ↑UInt32.size)
:
let lhs := mloadLHS;
let rhs := mloadRHS;
MloadSummary.EVM.step_mload (Int.toNat GAS_CELL) gasCost (StateMap.stateMap symState lhs) = Except.ok
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 1 }
rhs)
theorem
MloadOpcodeEquivalence.X_mload_equiv
{GAS_CELL MEMORYUSED_CELL PC_CELL W0 _Val0 _Val1 _Val10 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22
_Val23 _Val24 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
{LOCALMEM_CELL _Val14 : SortBytes}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
{_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}
{_WS : SortWordStack}
(defn_Val0 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = 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 32 = 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 : #range LOCALMEM_CELL W0 32 = some _Val14)
(defn_Val15 : asWord _Val14 = some _Val15)
(defn_Val16 : «_+Int_» PC_CELL 1 = some _Val16)
(defn_Val17 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val17)
(defn_Val18 : Cmem SCHEDULE_CELL _Val17 = some _Val18)
(defn_Val19 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val19)
(defn_Val20 : «_-Int_» _Val18 _Val19 = some _Val20)
(defn_Val21 : «_-Int_» GAS_CELL _Val20 = some _Val21)
(defn_Val22 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val22)
(defn_Val23 : «_-Int_» _Val21 _Val22 = some _Val23)
(defn_Val24 : #memoryUsageUpdate MEMORYUSED_CELL W0 32 = some _Val24)
(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)
(W0small : W0 < ↑EvmYul.UInt256.size)
(mucge0 : 0 ≤ MEMORYUSED_CELL)
(mucsmall : MEMORYUSED_CELL < ↑EvmYul.UInt256.size)
(codeMstore : _Gen0 = { val := { data := #[81] } })
(pcZero : PC_CELL = 0)
(stackOk : List.length (StateMap.wordStackMap _WS) < 1024)
(W0small_realpolitik : W0 < ↑UInt32.size)
:
let lhs := mloadLHS;
let rhs := mloadRHS;
EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState lhs) = Except.ok
(EvmYul.EVM.ExecutionResult.success
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 2 }
rhs)
ByteArray.empty)