def
Push0Equivalence.push0LHS
{GAS_CELL PC_CELL : SortInt}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Push0Equivalence.push0RHS
{_Val6 _Val8 : SortInt}
{SCHEDULE_CELL : SortSchedule}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Push0Equivalence.rw_push0LHS_push0RHS
{GAS_CELL PC_CELL _Val0 _Val2 _Val6 _Val7 _Val8 : SortInt}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val1 _Val3 _Val4 _Val5 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
(defn_Val0 : sizeWordStackAux WS 0 = some _Val0)
(defn_Val1 : «_<=Int_» _Val0 1023 = some _Val1)
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 : «_<=Int_» _Val2 GAS_CELL = some _Val3)
(defn_Val4 : _andBool_ _Val1 _Val3 = some _Val4)
(defn_Val5 : _andBool_ USEGAS_CELL _Val4 = some _Val5)
(defn_Val6 : «_+Int_» PC_CELL 1 = some _Val6)
(defn_Val7 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val7)
(defn_Val8 : «_-Int_» GAS_CELL _Val7 = some _Val8)
(req : _Val5 = true)
:
theorem
Push0Equivalence.push0_prestate_equiv
{GAS_CELL PC_CELL : SortInt}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
{symState : EvmYul.EVM.State}
:
let lhs := push0LHS;
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 _Gen17.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 := _Gen11.val, H_return := symState.H_return,
pc := StateMap.intMap PC_CELL, stack := StateMap.wordStackMap WS, execLength := symState.execLength }
theorem
Push0Equivalence.push0_poststate_equiv
{PC_CELL _Val6 _Val8 : SortInt}
{SCHEDULE_CELL : SortSchedule}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
{symState : EvmYul.EVM.State}
(defn_Val11 : «_+Int_» PC_CELL 1 = some _Val6)
:
let rhs := push0RHS;
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 _Gen17.refund.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 _Val8, activeWords := StateMap.intMap rhs.memoryUsed.val,
memory := StateMap.memory_map rhs.memory, returnData := _Gen11.val, H_return := symState.H_return,
pc := StateMap.intMap (PC_CELL + 1), stack := EvmYul.UInt256.ofNat 0 :: StateMap.wordStackMap WS,
execLength := symState.execLength }
theorem
Push0Equivalence.step_push0_equiv
{GAS_CELL PC_CELL _Val0 _Val2 _Val6 _Val7 _Val8 : SortInt}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val1 _Val3 _Val4 _Val5 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 : «_<=Int_» _Val2 GAS_CELL = some _Val3)
(defn_Val5 : _andBool_ USEGAS_CELL _Val4 = some _Val5)
(defn_Val6 : «_+Int_» PC_CELL 1 = some _Val6)
(defn_Val7 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val7)
(defn_Val8 : «_-Int_» GAS_CELL _Val7 = some _Val8)
(req : _Val5 = true)
(symState : EvmYul.EVM.State)
(gas gasCost : ℕ)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gasEnough : 0 < gas)
(gavailEnough : 2 ≤ GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(gasCostValue : gasCost = GasConstants.Gbase)
(pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size)
(pcountNonneg : 0 ≤ PC_CELL)
:
Push0Summary.EVM.step_push0 gas gasCost (StateMap.stateMap symState push0LHS) = Except.ok
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 1 }
push0RHS)
theorem
Push0Equivalence.X_push0_equiv
{GAS_CELL PC_CELL _Val0 _Val2 _Val6 _Val7 _Val8 : SortInt}
{SCHEDULE_CELL : SortSchedule}
{USEGAS_CELL _Val1 _Val3 _Val4 _Val5 : SortBool}
{WS : SortWordStack}
{_DotVar0 : SortGeneratedCounterCell}
{_DotVar2 : SortNetworkCell}
{_Gen0 : SortProgramCell}
{_Gen1 : SortJumpDestsCell}
{_Gen10 : SortCallDepthCell}
{_Gen11 : SortOutputCell}
{_Gen12 : SortStatusCodeCell}
{_Gen13 : SortCallStackCell}
{_Gen14 : SortInterimStatesCell}
{_Gen15 : SortTouchedAccountsCell}
{_Gen16 : SortVersionedHashesCell}
{_Gen17 : SortSubstateCell}
{_Gen18 : SortGasPriceCell}
{_Gen19 : SortOriginCell}
{_Gen2 : SortIdCell}
{_Gen20 : SortBlockhashesCell}
{_Gen21 : SortBlockCell}
{_Gen22 : SortExitCodeCell}
{_Gen23 : SortModeCell}
{_Gen3 : SortCallerCell}
{_Gen4 : SortCallDataCell}
{_Gen5 : SortCallValueCell}
{_Gen6 : SortLocalMemCell}
{_Gen7 : SortMemoryUsedCell}
{_Gen8 : SortCallGasCell}
{_Gen9 : SortStaticCell}
{_K_CELL : SortK}
(defn_Val0 : sizeWordStackAux WS 0 = some _Val0)
(defn_Val1 : «_<=Int_» _Val0 1023 = some _Val1)
(defn_Val2 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2)
(defn_Val3 : «_<=Int_» _Val2 GAS_CELL = some _Val3)
(defn_Val4 : _andBool_ _Val1 _Val3 = some _Val4)
(defn_Val5 : _andBool_ USEGAS_CELL _Val4 = some _Val5)
(defn_Val6 : «_+Int_» PC_CELL 1 = some _Val6)
(defn_Val7 :
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gbase_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val7)
(defn_Val8 : «_-Int_» GAS_CELL _Val7 = some _Val8)
(req : _Val5 = true)
(symState : EvmYul.EVM.State)
(symValidJumps : Array EvmYul.UInt256)
(cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM)
(gavailEnough : 2 < GAS_CELL)
(gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size)
(pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size)
(pcountNonneg : 0 ≤ PC_CELL)
(codePush0 : _Gen0 = { val := { data := #[95] } })
(pcZero : PC_CELL = 0)
(returnEmpty : _Gen11 = { val := ByteArray.empty })
:
EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState push0LHS) = Except.ok
(EvmYul.EVM.ExecutionResult.success
(StateMap.stateMap
{ toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack,
execLength := symState.execLength + 2 }
push0RHS)
ByteArray.empty)