Documentation

EvmEquivalence.Equivalence.Operations.TwoOpEquivalence

TwoOp Stack Operations #

Equivalence proofs for opcodes that perform operations on the elements of the stack.

The opcodes on this file are summarized on the KEVM side with two operations.

source
inductive TwoOpEquivalence.stackOps_op :
Type
Instances For
    source
    def TwoOpEquivalence.stackOps_op.to_binop :
    stackOps_op → SortBinStackOp ⊕ SortTernStackOp ⊕ SortUnStackOp
    Equations
    Instances For
      source
      def TwoOpEquivalence.stackOps_op.to_maybeOpcode (op : stackOps_op) :
      SortMaybeOpCode
      Equations
      Instances For
        source
        def TwoOpEquivalence.stackOps_op.from_k :
        stackOps_op → StackOpsSummary.stackOps_op
        Equations
        Instances For
          source
          def TwoOpEquivalence.stackOps_op.to_stack (op : stackOps_op) (W0 W1 W2 : SortInt) (WS : SortWordStack) :
          SortWordStack
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def TwoOpEquivalence.twoOpLHS (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 W2 : SortInt} {K_CELL : SortK} {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} :
            SortGeneratedTopCell
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def TwoOpEquivalence.twoOpRHS {_Val0 _Val4 _Val5 _Val6 _Val7 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {_Val1 _Val2 : 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} :
              SortGeneratedTopCell
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def TwoOpEquivalence.stackOps_op.to_defn_Val3 (op : stackOps_op) (W0 W1 _Val3_int : SortInt) (_Val3_bool : SortBool) :
                Prop

                First Op for summarization

                Equations
                Instances For
                  source
                  def TwoOpEquivalence.stackOps_op.to_defn_Val4 (op : stackOps_op) (_Val3_bool : SortBool) (_Val3_int _Val4 W2 : SortInt) :
                  Prop

                  Second Op for summarization

                  Equations
                  Instances For
                    source
                    def TwoOpEquivalence.stackOps_op.to_gas :
                    stackOps_op → SortScheduleConst
                    Equations
                    Instances For
                      source
                      theorem TwoOpEquivalence.rw_twoOpLHS_twoOpRHS (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 W2 _Val0 _Val3_int _Val4 _Val5 _Val6 _Val7 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val1 _Val2 _Val3_bool : 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} (defn_Val0 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val0) (defn_Val1 : «_<=Int_» _Val0 GAS_CELL = some _Val1) (defn_Val2 : _andBool_ USEGAS_CELL _Val1 = some _Val2) (defn_Val3 : op.to_defn_Val3 W0 W1 _Val3_int _Val3_bool) (defn_Val4 : op.to_defn_Val4 _Val3_bool _Val3_int _Val4 W2) (defn_Val5 : «_+Int_» PC_CELL 1 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val6) (defn_Val7 : «_-Int_» GAS_CELL _Val6 = some _Val7) (req : _Val2 = true) :
                      Rewrites (twoOpLHS op) twoOpRHS
                      source
                      theorem TwoOpEquivalence.twoOp_prestate_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 W2 : SortInt} {K_CELL : SortK} {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} (symState : EvmYul.EVM.State) :
                      let lhs := twoOpLHS 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 _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 := op.from_k.stack (StateMap.intMap W0) (StateMap.intMap W1) (StateMap.intMap W2) (StateMap.wordStackMap WS), execLength := symState.execLength }
                      source
                      def TwoOpEquivalence.modWord (n m : SortInt) :
                      SortInt
                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem TwoOpEquivalence.modWord_eq (n m : SortInt) :
                        «_%Word__EVM-TYPES_Int_Int_Int» n m = some (modWord n m)
                        source
                        def TwoOpEquivalence.stackOps_op.do (op : stackOps_op) (W0 W1 W2 : SortInt) :
                        SortInt
                        Equations
                        Instances For
                          source
                          def TwoOpEquivalence.stackOps_op.gas_comp :
                          stackOps_op → SortInt
                          Equations
                          Instances For
                            source
                            theorem TwoOpEquivalence.twoOp_poststate_equiv (op : stackOps_op) {PC_CELL W0 W1 W2 _Val0 _Val3_int _Val4 _Val5 _Val6 _Val7 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {_Val1 _Val2 _Val3_bool : 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} (defn_Val3 : op.to_defn_Val3 W0 W1 _Val3_int _Val3_bool) (defn_Val4 : op.to_defn_Val4 _Val3_bool _Val3_int _Val4 W2) (defn_Val5 : «_+Int_» PC_CELL 1 = some _Val5) (symState : EvmYul.EVM.State) :
                            let rhs := twoOpRHS; 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 _Val7, 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 := StateMap.intMap (op.do W0 W1 W2) :: StateMap.wordStackMap WS, execLength := symState.execLength }
                            source
                            theorem TwoOpEquivalence.step_twoOp_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 W2 _Val0 _Val3_int _Val4 _Val5 _Val6 _Val7 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val1 _Val2 _Val3_bool : 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} (defn_Val0 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val0) (defn_Val1 : «_<=Int_» _Val0 GAS_CELL = some _Val1) (defn_Val2 : _andBool_ USEGAS_CELL _Val1 = some _Val2) (defn_Val3 : op.to_defn_Val3 W0 W1 _Val3_int _Val3_bool) (defn_Val4 : op.to_defn_Val4 _Val3_bool _Val3_int _Val4 W2) (defn_Val5 : «_+Int_» PC_CELL 1 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val6) (defn_Val7 : «_-Int_» GAS_CELL _Val6 = some _Val7) (req : _Val2 = true) (symState : EvmYul.EVM.State) (gas gasCost : ℕ) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (gasEnough : 0 < gas) (gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size) (gasCostValue : gasCost = op.from_k.C'_noexp) (pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size) (pcountNonneg : 0 ≤ PC_CELL) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) :
                            StackOpsSummary.EVM.step_stackOps op.from_k gas gasCost (StateMap.stateMap symState (twoOpLHS op)) = Except.ok (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 } twoOpRHS)
                            source
                            theorem TwoOpEquivalence.X_twoOp_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 W2 _Val0 _Val3_int _Val4 _Val5 _Val6 _Val7 : SortInt} {K_CELL : SortK} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val1 _Val2 _Val3_bool : 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} (defn_Val0 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val0) (defn_Val1 : «_<=Int_» _Val0 GAS_CELL = some _Val1) (defn_Val2 : _andBool_ USEGAS_CELL _Val1 = some _Val2) (defn_Val3 : op.to_defn_Val3 W0 W1 _Val3_int _Val3_bool) (defn_Val4 : op.to_defn_Val4 _Val3_bool _Val3_int _Val4 W2) (defn_Val5 : «_+Int_» PC_CELL 1 = some _Val5) (defn_Val6 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val6) (defn_Val7 : «_-Int_» GAS_CELL _Val6 = some _Val7) (req : _Val2 = true) (symState : EvmYul.EVM.State) (symValidJumps : Array EvmYul.UInt256) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (codeTwoOp : _Gen0 = { val := op.from_k.to_bin }) (pcZero : PC_CELL = 0) (enoughGas : op.gas_comp < GAS_CELL) (boundedGas : GAS_CELL < ↑EvmYul.UInt256.size) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) (wordStackOk : sizeWordStackAux WS 0 < do let a ← some op.from_k.to_stack_length pure ↑a) :
                            EvmYul.EVM.X (StateMap.intMap GAS_CELL).toNat symValidJumps (StateMap.stateMap symState (twoOpLHS op)) = Except.ok (EvmYul.EVM.ExecutionResult.success (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 2 } twoOpRHS) ByteArray.empty)