EvmEquivalence.Equivalence.StateGettersEquivalence

let lhs := oneOpLHS op; 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 _Gen16.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 := _Gen10.val, H_return := symState.H_return, pc := StateMap.intMap PC_CELL, stack := StateMap.wordStackMap WS, execLength := symState.execLength }

source

theorem StateGettersEquivalence.oneOp_poststate_equiv {TOP_STACK ID_CELL ORIGIN_CELL CALLER_CELL GASPRICE_CELL COINBASE_CELL TIMESTAMP_CELL MIXHASH_CELL NUMBER_CELL GASLIMIT_CELL CHAINID_CELL PC_CELL _Val5 _Val6 _Val8 : SortInt} {SCHEDULE_CELL : SortSchedule} {WS : SortWordStack} {_DotVar0 : SortGeneratedCounterCell} {_DotVar2 : SortNetworkCell} {_Gen0 : SortProgramCell} {_Gen1 : SortJumpDestsCell} {_Gen10 : SortOutputCell} {_Gen11 : SortStatusCodeCell} {_Gen12 : SortCallStackCell} {_Gen13 : SortInterimStatesCell} {_Gen14 : SortTouchedAccountsCell} {_Gen15 : SortVersionedHashesCell} {_Gen16 : SortSubstateCell} {_Gen19 : SortBlockhashesCell} {_Gen20 : SortBlockCell} {_Gen21 : SortExitCodeCell} {_Gen22 : SortModeCell} {_Gen3 : SortCallDataCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortStaticCell} {_Gen9 : SortCallDepthCell} {_K_CELL : SortK} (defn_Val6 : «_+Int_» PC_CELL 1 = some _Val6) (symState : EvmYul.EVM.State) :

let rhs := oneOpRHS; 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 _Gen16.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 := _Gen10.val, H_return := symState.H_return, pc := StateMap.intMap (PC_CELL + 1), stack := StateMap.intMap TOP_STACK :: StateMap.wordStackMap WS, execLength := symState.execLength }

source

def StateGettersEquivalence.stateGetter_op.gas (op : stateGetter_op) :

ℕ

Equations

op.gas = GasConstants.Gbase

Instances For

source

theorem StateGettersEquivalence.step_oneOp_equiv (op : stateGetter_op) {GAS_CELL ID_CELL ORIGIN_CELL CALLER_CELL GASPRICE_CELL COINBASE_CELL TIMESTAMP_CELL MIXHASH_CELL NUMBER_CELL GASLIMIT_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 : SortOutputCell} {_Gen11 : SortStatusCodeCell} {_Gen12 : SortCallStackCell} {_Gen13 : SortInterimStatesCell} {_Gen14 : SortTouchedAccountsCell} {_Gen15 : SortVersionedHashesCell} {_Gen16 : SortSubstateCell} {_Gen19 : SortBlockhashesCell} {_Gen20 : SortBlockCell} {_Gen21 : SortExitCodeCell} {_Gen22 : SortModeCell} {_Gen3 : SortCallDataCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortStaticCell} {_Gen9 : SortCallDepthCell} {_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) (gas gasCost : ℕ) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (gasEnough : 0 < gas) (gavailEnough : ↑op.gas ≤ GAS_CELL) (gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size) (gasCostValue : gasCost = op.gas) (pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size) (pcountNonneg : 0 ≤ PC_CELL) (ID_CELL_small : ID_CELL < ↑EvmYul.AccountAddress.size) (ID_CELL_nonneg : 0 ≤ ID_CELL) (ORIGIN_CELL_small : ORIGIN_CELL < ↑EvmYul.AccountAddress.size) (ORIGIN_CELL_nonneg : 0 ≤ ORIGIN_CELL) (CALLER_CELL_small : CALLER_CELL < ↑EvmYul.AccountAddress.size) (CALLER_CELL_nonneg : 0 ≤ CALLER_CELL) (GASPRICE_CELL_nonneg : 0 ≤ GASPRICE_CELL) (COINBASE_CELL_small : COINBASE_CELL < ↑EvmYul.AccountAddress.size) (COINBASE_CELL_nonneg : 0 ≤ COINBASE_CELL) (TIMESTAMP_CELL_nonneg : 0 ≤ TIMESTAMP_CELL) (NUMBER_CELL_nonneg : 0 ≤ NUMBER_CELL) (GASLIMIT_CELL_nonneg : 0 ≤ GASLIMIT_CELL) :

let lhs := oneOpLHS op; let rhs := oneOpRHS; StateGettersSummary.EVM.step_arith op.from_k gas gasCost (StateMap.stateMap symState lhs) = Except.ok (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 } rhs)

source

theorem StateGettersEquivalence.X_oneOp_equiv (op : stateGetter_op) {GAS_CELL ID_CELL ORIGIN_CELL CALLER_CELL GASPRICE_CELL COINBASE_CELL TIMESTAMP_CELL MIXHASH_CELL NUMBER_CELL GASLIMIT_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 : SortOutputCell} {_Gen11 : SortStatusCodeCell} {_Gen12 : SortCallStackCell} {_Gen13 : SortInterimStatesCell} {_Gen14 : SortTouchedAccountsCell} {_Gen15 : SortVersionedHashesCell} {_Gen16 : SortSubstateCell} {_Gen19 : SortBlockhashesCell} {_Gen2 : SortCallerCell} {_Gen20 : SortBlockCell} {_Gen21 : SortExitCodeCell} {_Gen22 : SortModeCell} {_Gen3 : SortCallDataCell} {_Gen4 : SortCallValueCell} {_Gen5 : SortLocalMemCell} {_Gen6 : SortMemoryUsedCell} {_Gen7 : SortCallGasCell} {_Gen8 : SortStaticCell} {_Gen9 : SortCallDepthCell} {_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) (codeDiv : _Gen0 = { val := op.from_k.to_bin }) (pcZero : PC_CELL = 0) (enoughGas : ↑op.gas < GAS_CELL) (boundedGas : GAS_CELL < ↑EvmYul.UInt256.size) (ID_CELL_small : ID_CELL < ↑EvmYul.AccountAddress.size) (ID_CELL_nonneg : 0 ≤ ID_CELL) (ORIGIN_CELL_small : ORIGIN_CELL < ↑EvmYul.AccountAddress.size) (ORIGIN_CELL_nonneg : 0 ≤ ORIGIN_CELL) (CALLER_CELL_small : CALLER_CELL < ↑EvmYul.AccountAddress.size) (CALLER_CELL_nonneg : 0 ≤ CALLER_CELL) (GASPRICE_CELL_nonneg : 0 ≤ GASPRICE_CELL) (COINBASE_CELL_small : COINBASE_CELL < ↑EvmYul.AccountAddress.size) (COINBASE_CELL_nonneg : 0 ≤ COINBASE_CELL) (TIMESTAMP_CELL_nonneg : 0 ≤ TIMESTAMP_CELL) (NUMBER_CELL_nonneg : 0 ≤ NUMBER_CELL) (GASLIMIT_CELL_nonneg : 0 ≤ GASLIMIT_CELL) :

let lhs := oneOpLHS op; let rhs := oneOpRHS; 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)