Documentation

EvmEquivalence.Equivalence.Operations.OneOpEquivalence

OneOp 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 only one operation.

source
inductive OneOpEquivalence.stackOps_op :
Type
Instances For
    source
    def OneOpEquivalence.stackOps_op.to_binop :
    stackOps_op → SortBinStackOp ⊕ SortUnStackOp
    Equations
    Instances For
      source
      def OneOpEquivalence.stackOps_op.to_maybeOpcode (op : stackOps_op) :
      SortMaybeOpCode
      Equations
      Instances For
        source
        def OneOpEquivalence.stackOps_op.from_k :
        stackOps_op → StackOpsSummary.stackOps_op
        Equations
        Instances For
          source
          def OneOpEquivalence.stackOps_op.to_stack (op : stackOps_op) (W0 W1 : SortInt) (WS : SortWordStack) :
          SortWordStack
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def OneOpEquivalence.oneOpLHS (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 : 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} :
            SortGeneratedTopCell
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def OneOpEquivalence.oneOpRHS {_Val3 _Val4 _Val5 _Val6 : SortInt} {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} {_K_CELL : SortK} :
              SortGeneratedTopCell
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def OneOpEquivalence.stackOps_op.to_defn_Val3 (op : stackOps_op) (W0 W1 _Val3 : SortInt) :
                Prop
                Equations
                Instances For
                  source
                  def OneOpEquivalence.stackOps_op.to_gas :
                  stackOps_op → SortScheduleConst
                  Equations
                  Instances For
                    source
                    theorem OneOpEquivalence.rw_oneOpLHS_oneOpRHS (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 _Val0 _Val3 _Val4 _Val5 _Val6 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _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} {_K_CELL : SortK} (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) (defn_Val4 : «_+Int_» PC_CELL 1 = some _Val4) (defn_Val5 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val5) (defn_Val6 : «_-Int_» GAS_CELL _Val5 = some _Val6) (req : _Val2 = true) :
                    Rewrites (oneOpLHS op) oneOpRHS
                    source
                    theorem OneOpEquivalence.oneOp_prestate_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 : 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 := 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 _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) default (StateMap.wordStackMap WS), execLength := symState.execLength }
                    source
                    def OneOpEquivalence.divWord (n m : SortInt) :
                    SortInt
                    Equations
                    Instances For
                      source
                      theorem OneOpEquivalence.divWord_divInt_eq (n m : SortInt) :
                      «_/Word__EVM-TYPES_Int_Int_Int» n m = some (divWord n m)
                      source
                      def OneOpEquivalence.stackOps_op.do (op : stackOps_op) :
                      SortInt → SortInt → SortInt
                      Equations
                      Instances For
                        source
                        theorem OneOpEquivalence.oneOp_poststate_equiv (op : stackOps_op) {PC_CELL W0 W1 _Val3 _Val4 _Val5 _Val6 : SortInt} {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} {_K_CELL : SortK} (defn_Val3 : op.to_defn_Val3 W0 W1 _Val3) (defn_Val4 : «_+Int_» PC_CELL 1 = some _Val4) (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 _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 _Val6, 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) :: StateMap.wordStackMap WS, execLength := symState.execLength }
                        source
                        def OneOpEquivalence.stackOps_op.gas (op : stackOps_op) :
                        ℕ
                        Equations
                        Instances For
                          source
                          theorem OneOpEquivalence.step_oneOp_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 _Val0 _Val3 _Val4 _Val5 _Val6 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _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} {_K_CELL : SortK} (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) (defn_Val4 : «_+Int_» PC_CELL 1 = some _Val4) (defn_Val5 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val5) (defn_Val6 : «_-Int_» GAS_CELL _Val5 = some _Val6) (req : _Val2 = 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) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) :
                          let lhs := oneOpLHS op; let rhs := oneOpRHS; StackOpsSummary.EVM.step_stackOps 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 OneOpEquivalence.X_oneOp_equiv (op : stackOps_op) {GAS_CELL PC_CELL W0 W1 _Val0 _Val3 _Val4 _Val5 _Val6 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _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} {_K_CELL : SortK} (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) (defn_Val4 : «_+Int_» PC_CELL 1 = some _Val4) (defn_Val5 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» op.to_gas SCHEDULE_CELL = some _Val5) (defn_Val6 : «_-Int_» GAS_CELL _Val5 = some _Val6) (req : _Val2 = 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) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) (wordStackOk : sizeWordStackAux WS 0 < do let a ← some op.from_k.to_stack_length pure ↑a) :
                          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)