@[simp]

theorem StopSummary.decode_singleton_stop {n : UInt8} : EvmYul.EVM.decode { data := #[n] } (EvmYul.UInt256.ofNat 1) = none

@[simp]

theorem StopSummary.C'_stop (symState : EvmYul.EVM.State) : EvmYul.EVM.C' symState EvmYul.Operation.STOP = 0

@[simp]

theorem StopSummary.memoryExpansionCost_stop (symState : EvmYul.EVM.State) : EvmYul.EVM.memoryExpansionCost symState EvmYul.Operation.STOP = 0

theorem StopSummary.EvmYul.step_stop_summary_simple (symState : EvmYul.EVM.State) : EvmYul.step EvmYul.Operation.STOP symState = Except.ok { toState := symState.toState, gasAvailable := symState.gasAvailable, activeWords := symState.activeWords, memory := symState.memory, returnData := ByteArray.empty, H_return := symState.H_return, pc := symState.pc, stack := symState.stack, execLength := symState.execLength }

theorem StopSummary.EvmYul.step_stop_summary (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable : EvmYul.UInt256) (symExecLength : ℕ) (symState : EvmYul.EVM.State) : EvmYul.step EvmYul.Operation.STOP { toState := symState.toState, gasAvailable := symGasAvailable, activeWords := symState.activeWords, memory := symState.memory, returnData := symState.returnData, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength } = Except.ok { toState := symState.toState, gasAvailable := symGasAvailable, activeWords := symState.activeWords, memory := symState.memory, returnData := ByteArray.empty, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength }

theorem StopSummary.EVM.step_stop_summary_simple (gas gasCost : ℕ) (gpos : 0 < gas) (symState : EvmYul.EVM.State) : EvmYul.EVM.step gas gasCost (some (EvmYul.Operation.STOP, none)) symState = Except.ok { toState := symState.toState, gasAvailable := symState.gasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := symState.activeWords, memory := symState.memory, returnData := ByteArray.empty, H_return := symState.H_return, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 }

theorem StopSummary.EVM.step_stop_summary (gas gasCost : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable : EvmYul.UInt256) (symExecLength : ℕ) (gpos : 0 < gas) (symState : EvmYul.EVM.State) : EvmYul.EVM.step gas gasCost (some (EvmYul.Operation.STOP, none)) { toState := symState.toState, gasAvailable := symGasAvailable, activeWords := symState.activeWords, memory := symState.memory, returnData := symState.returnData, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength } = Except.ok { toState := symState.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := symState.activeWords, memory := symState.memory, returnData := ByteArray.empty, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength + 1 }