EXP opcode

Equivalence proofs for the exp opcode

The exp opcode requires a satandalone file because its summaries are not easily generalizable to the OneOp or TwoOp ones.

inductive ExpOpcodeEquivalence.exp_case : Type

We have two cases for the summaries: one where the exponent is 0, and where the exponent is greater than 0

• gt0 : exp_case
• eq0 : exp_case

def ExpOpcodeEquivalence.expLHS {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.

def ExpOpcodeEquivalence.expRHS {_Val11 _Val12 _Val20 : 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} : SortGeneratedTopCell

Equations

• One or more equations did not get rendered due to their size.

def ExpOpcodeEquivalence.exp_case.to_defn_Val0 (ec : exp_case) (W1 : SortInt) (_Val0 : SortBool) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_defn_Val0 W1 _Val0 = («_<Int_» 0 W1 = some _Val0)
• ExpOpcodeEquivalence.exp_case.eq0.to_defn_Val0 W1 _Val0 = («_<=Int_» W1 0 = some _Val0)

def ExpOpcodeEquivalence.exp_case.to_defn_Val8 (ec : exp_case) (GAS_CELL _Val1 _Val7 : SortInt) (_Val8 _Val2 : SortBool) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_defn_Val8 GAS_CELL _Val1 _Val7 _Val8 _Val2 = («_<=Int_» _Val7 GAS_CELL = some _Val8)
• ExpOpcodeEquivalence.exp_case.eq0.to_defn_Val8 GAS_CELL _Val1 _Val7 _Val8 _Val2 = («_<=Int_» _Val1 GAS_CELL = some _Val2)

def ExpOpcodeEquivalence.exp_case.to_defn_Val9 (ec : exp_case) (_Val0 _Val2 _Val3 _Val8 _Val9 : SortBool) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_defn_Val9 _Val0 _Val2 _Val3 _Val8 _Val9 = (_andBool_ _Val0 _Val8 = some _Val9)
• ExpOpcodeEquivalence.exp_case.eq0.to_defn_Val9 _Val0 _Val2 _Val3 _Val8 _Val9 = (_andBool_ _Val0 _Val2 = some _Val3)

def ExpOpcodeEquivalence.exp_case.to_defn_Val10 (ec : exp_case) (USEGAS_CELL _Val3 _Val4 _Val9 _Val10 : SortBool) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_defn_Val10 USEGAS_CELL _Val3 _Val4 _Val9 _Val10 = (_andBool_ USEGAS_CELL _Val9 = some _Val10)
• ExpOpcodeEquivalence.exp_case.eq0.to_defn_Val10 USEGAS_CELL _Val3 _Val4 _Val9 _Val10 = (_andBool_ USEGAS_CELL _Val3 = some _Val4)

def ExpOpcodeEquivalence.exp_case.to_defn_Val20 (ec : exp_case) (GAS_CELL _Val1 _Val19 _Val20 : SortInt) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_defn_Val20 GAS_CELL _Val1 _Val19 _Val20 = («_-Int_» GAS_CELL _Val19 = some _Val20)
• ExpOpcodeEquivalence.exp_case.eq0.to_defn_Val20 GAS_CELL _Val1 _Val19 _Val20 = («_-Int_» GAS_CELL _Val1 = some _Val20)

def ExpOpcodeEquivalence.exp_case.to_req (ec : exp_case) (_Val4 _Val10 : SortBool) : Prop

Equations

• ExpOpcodeEquivalence.exp_case.gt0.to_req _Val4 _Val10 = (_Val10 = true)
• ExpOpcodeEquivalence.exp_case.eq0.to_req _Val4 _Val10 = (_Val4 = true)

theorem ExpOpcodeEquivalence.rw_expLHS_expRHS (ec : exp_case) {GAS_CELL PC_CELL W0 W1 _Val1 _Val11 _Val12 _Val13 _Val14 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val3 _Val4 _Val5 _Val6 _Val7 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val10 _Val8 _Val9 _Val2_eq _Val3_eq _Val4_eq : 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 : ec.to_defn_Val0 W1 _Val0) (defn_Val1 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val1) (defn_Val2 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2) (defn_Val3 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val3) (defn_Val4 : «_/Int_» _Val3 8 = some _Val4) (defn_Val5 : «_+Int_» _Val4 1 = some _Val5) (defn_Val6 : «_*Int_» _Val2 _Val5 = some _Val6) (defn_Val7 : «_+Int_» _Val1 _Val6 = some _Val7) (defn_Val8 : ec.to_defn_Val8 GAS_CELL _Val1 _Val7 _Val8 _Val2_eq) (defn_Val9 : ec.to_defn_Val9 _Val0 _Val2_eq _Val3_eq _Val8 _Val9) (defn_Val10 : ec.to_defn_Val10 USEGAS_CELL _Val3_eq _Val4_eq _Val9 _Val10) (defn_Val11 : powmod W0 W1 115792089237316195423570985008687907853269984665640564039457584007913129639936 = some _Val11) (defn_Val12 : «_+Int_» PC_CELL 1 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14) (defn_Val15 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val15) (defn_Val16 : «_/Int_» _Val15 8 = some _Val16) (defn_Val17 : «_+Int_» _Val16 1 = some _Val17) (defn_Val18 : «_*Int_» _Val14 _Val17 = some _Val18) (defn_Val19 : «_+Int_» _Val13 _Val18 = some _Val19) (defn_Val20 : ec.to_defn_Val20 GAS_CELL _Val13 _Val19 _Val20) (req : ec.to_req _Val4_eq _Val10) : Rewrites expLHS expRHS

We have three different kinds of hypotheses:

1. Hypotheses that apply to both summaries (e.g., defn_Val1)
2. Hypotheses that change depending on the summary (e.g., defn_Val0)
3. Hypotheses that only apply to the case gt0 and are irrelevant for eq0 (e.g., defn_Val2 through defn_Val7)

theorem ExpOpcodeEquivalence.exp_prestate_equiv {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 := expLHS; 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.intMap W0 :: StateMap.intMap W1 :: StateMap.wordStackMap WS, execLength := symState.execLength }

opaque ExpOpcodeEquivalence.TODO.exp_representation : SortInt → SortInt → SortInt

We should specify a reasoning friendly exp behavior

theorem ExpOpcodeEquivalence.exp_poststate_equiv {PC_CELL W0 W1 _Val6 _Val11 _Val12 _Val20 : 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} (defn_Val11 : powmod W0 W1 115792089237316195423570985008687907853269984665640564039457584007913129639936 = some _Val11) (defn_Val12 : «_+Int_» PC_CELL 1 = some _Val12) (symState : EvmYul.EVM.State) : let rhs := expRHS; 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 _Val20, 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 (TODO.exp_representation W0 W1) :: StateMap.wordStackMap WS, execLength := symState.execLength }

def ExpOpcodeEquivalence.exp_case.gas (ec : exp_case) : ℕ

Equations

• ExpOpcodeEquivalence.exp_case.eq0.gas = GasConstants.Gexp
• ExpOpcodeEquivalence.exp_case.gt0.gas = GasConstants.Gexp + GasConstants.Gexpbyte

theorem ExpOpcodeEquivalence.step_exp_equiv (ec : exp_case) {GAS_CELL PC_CELL W0 W1 _Val1 _Val11 _Val12 _Val13 _Val14 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val3 _Val4 _Val5 _Val6 _Val7 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val10 _Val8 _Val9 _Val2_eq _Val3_eq _Val4_eq : 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 : ec.to_defn_Val0 W1 _Val0) (defn_Val1 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val1) (defn_Val2 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2) (defn_Val3 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val3) (defn_Val4 : «_/Int_» _Val3 8 = some _Val4) (defn_Val5 : «_+Int_» _Val4 1 = some _Val5) (defn_Val6 : «_*Int_» _Val2 _Val5 = some _Val6) (defn_Val7 : «_+Int_» _Val1 _Val6 = some _Val7) (defn_Val8 : ec.to_defn_Val8 GAS_CELL _Val1 _Val7 _Val8 _Val2_eq) (defn_Val9 : ec.to_defn_Val9 _Val0 _Val2_eq _Val3_eq _Val8 _Val9) (defn_Val10 : ec.to_defn_Val10 USEGAS_CELL _Val3_eq _Val4_eq _Val9 _Val10) (defn_Val11 : powmod W0 W1 115792089237316195423570985008687907853269984665640564039457584007913129639936 = some _Val11) (defn_Val12 : «_+Int_» PC_CELL 1 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14) (defn_Val15 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val15) (defn_Val16 : «_/Int_» _Val15 8 = some _Val16) (defn_Val17 : «_+Int_» _Val16 1 = some _Val17) (defn_Val18 : «_*Int_» _Val14 _Val17 = some _Val18) (defn_Val19 : «_+Int_» _Val13 _Val18 = some _Val19) (defn_Val20 : ec.to_defn_Val20 GAS_CELL _Val13 _Val19 _Val20) (req : ec.to_req _Val4_eq _Val10) (symState : EvmYul.EVM.State) (gas gasCost : ℕ) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (gasEnough : 0 < gas) (gavailEnough : ↑ec.gas ≤ GAS_CELL) (gavailSmall : GAS_CELL < ↑EvmYul.UInt256.size) (gasCostValue : gasCost = ec.gas) (pcountSmall : PC_CELL + 1 < ↑EvmYul.UInt256.size) (pcountNonneg : 0 ≤ PC_CELL) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) : let lhs := expLHS; let rhs := expRHS; StackOpsSummary.EVM.step_stackOps StackOpsSummary.stackOps_op.exp gas gasCost (StateMap.stateMap symState lhs) = Except.ok (StateMap.stateMap { toSharedState := symState.toSharedState, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 } rhs)

theorem ExpOpcodeEquivalence.X_exp_equiv (ec : exp_case) {GAS_CELL PC_CELL W0 W1 _Val1 _Val11 _Val12 _Val13 _Val14 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val3 _Val4 _Val5 _Val6 _Val7 : SortInt} {SCHEDULE_CELL : SortSchedule} {USEGAS_CELL _Val0 _Val10 _Val8 _Val9 _Val2_eq _Val3_eq _Val4_eq : 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 : ec.to_defn_Val0 W1 _Val0) (defn_Val1 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val1) (defn_Val2 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val2) (defn_Val3 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val3) (defn_Val4 : «_/Int_» _Val3 8 = some _Val4) (defn_Val5 : «_+Int_» _Val4 1 = some _Val5) (defn_Val6 : «_*Int_» _Val2 _Val5 = some _Val6) (defn_Val7 : «_+Int_» _Val1 _Val6 = some _Val7) (defn_Val8 : ec.to_defn_Val8 GAS_CELL _Val1 _Val7 _Val8 _Val2_eq) (defn_Val9 : ec.to_defn_Val9 _Val0 _Val2_eq _Val3_eq _Val8 _Val9) (defn_Val10 : ec.to_defn_Val10 USEGAS_CELL _Val3_eq _Val4_eq _Val9 _Val10) (defn_Val11 : powmod W0 W1 115792089237316195423570985008687907853269984665640564039457584007913129639936 = some _Val11) (defn_Val12 : «_+Int_» PC_CELL 1 = some _Val12) (defn_Val13 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexp_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val13) (defn_Val14 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val14) (defn_Val15 : «log2Int(_)_INT-COMMON_Int_Int» W1 = some _Val15) (defn_Val16 : «_/Int_» _Val15 8 = some _Val16) (defn_Val17 : «_+Int_» _Val16 1 = some _Val17) (defn_Val18 : «_*Int_» _Val14 _Val17 = some _Val18) (defn_Val19 : «_+Int_» _Val13 _Val18 = some _Val19) (defn_Val20 : ec.to_defn_Val20 GAS_CELL _Val13 _Val19 _Val20) (req : ec.to_req _Val4_eq _Val10) (symState : EvmYul.EVM.State) (symValidJumps : Array EvmYul.UInt256) (cancun : SCHEDULE_CELL = SortSchedule.CANCUN_EVM) (codeDiv : _Gen0 = { val := { data := #[10] } }) (pcZero : PC_CELL = 0) (enoughGas : ↑ec.gas < GAS_CELL) (boundedGas : GAS_CELL < ↑EvmYul.UInt256.size) (W0ge0 : 0 ≤ W0) (W1ge0 : 0 ≤ W1) (boundedW1 : W1 < ↑EvmYul.UInt256.size) (wordStackOk : sizeWordStackAux WS 0 < some 1023) : let lhs := expLHS; let rhs := expRHS; 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)