Documentation

EvmEquivalence.Summaries.Push0Summary

source
@[reducible, inline]
abbrev Push0Summary.push0EVM :
EvmYul.Operation EvmYul.OperationType.EVM
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Push0Summary.push0_instr :
    Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))
    Equations
    Instances For
      source
      def Push0Summary.EVM.step_push0 (gas gasCost : ℕ) :
      EvmYul.EVM.Transformer
      Equations
      Instances For
        source
        def Push0Summary.EvmYul.step_push0 :
        EvmYul.EVM.Transformer
        Equations
        Instances For
          source
          theorem Push0Summary.EvmYul.step_push0_summary (symStack : EvmYul.Stack EvmYul.UInt256) (symPc : EvmYul.UInt256) (symState : EvmYul.EVM.State) :
          step_push0 { toSharedState := symState.toSharedState, pc := symPc, stack := symStack, execLength := symState.execLength } = default
          source
          theorem Push0Summary.EVM.step_push0_summary_simple (gas gasCost : ℕ) (gpos : 0 < gas) (symState : EvmYul.EVM.State) :
          step_push0 gas gasCost symState = Except.ok { toState := symState.toState, gasAvailable := symState.gasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := symState.activeWords, memory := symState.memory, returnData := symState.returnData, H_return := symState.H_return, pc := symState.pc + EvmYul.UInt256.ofNat 1, stack := EvmYul.UInt256.ofNat 0 :: symState.stack, execLength := symState.execLength + 1 }
          source
          theorem Push0Summary.EVM.step_push0_summary (gas gasCost symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symCode symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (gpos : 0 < gas) (symState : EvmYul.EVM.State) :
          let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength }; step_push0 gas gasCost ss = Except.ok { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := ss.activeWords, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := EvmYul.UInt256.ofNat 0 :: symStack, execLength := symExecLength + 1 }
          source
          @[simp]
          theorem Push0Summary.decode_singleton_push0 :
          EvmYul.EVM.decode { data := #[95] } (EvmYul.UInt256.ofNat 0) = some (push0EVM, none)
          source
          @[simp]
          theorem Push0Summary.memoryExpansionCost_push0 (symState : EvmYul.EVM.State) :
          EvmYul.EVM.memoryExpansionCost symState push0EVM = 0
          source
          @[simp]
          theorem Push0Summary.C'_push0 (symState : EvmYul.EVM.State) :
          EvmYul.EVM.C' symState push0EVM = GasConstants.Gbase
          source
          theorem Push0Summary.X_push0_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (symValidJumps : Array EvmYul.UInt256) (enoughGas : GasConstants.Gbase < symGasAvailable.toNat) (symStack_ok : List.length symStack < 1024) (symState : EvmYul.EVM.State) :
          let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := { data := #[95] }, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := EvmYul.UInt256.ofNat 0, stack := symStack, execLength := symExecLength }; EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat GasConstants.Gbase, activeWords := ss.activeWords, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := EvmYul.UInt256.ofNat 0 :: symStack, execLength := symExecLength + 2 } ByteArray.empty)