1 EVM 概念与定位
1.1 EVM 的定义与角色
EVM（Ethereum Virtual Machine，太坊虚拟机）是一种运行在区块链系统上的抽象执行环境。它把“智能合约”理解为一段可执行的指令序列，并规定这些指令在读取与更新合约状态时应遵循的规则。由于执行结果会被写入区块链账本，EVM 的核心任务是：在不依赖特定硬件实现差异的前提下，使同一交易与同一合约调用在网络内产生一致的状态变化。
从形式化科学的语境看，EVM 可被视为“带语义的状态机”：指令语义规定每条操作如何改变程序的内部结构与可观测状态；状态转移约束则保证更新规则可被严格描述与推导；燃料（gas）等机制进一步约束执行的资源使用与终止行为。
1.2 与区块链执行环境的关系
在区块链系统中，交易通常包含：发送者、目标（或创建新合约的意图）、输入数据与支付方式。区块链节点在验证交易时，需要执行合约相关逻辑并得到新状态。EVM 作为统一的执行规范，相当于把“合约调用的解释器”标准化。
因此，区块链层面提供数据结构与共识机制；而 EVM 提供执行层面的确定规则，使得节点在相同输入下能对“合约如何算”达成一致。
1.3 EVM 的确定性执行特征
EVM 的确定性执行特征主要体现在：给定相同的链上状态、同一交易内容、相同的执行上下文参数时，指令序列的每一步状态更新都由形式化规则唯一决定。这降低了节点实现差异导致的“分叉风险”。
此外，EVM 的外部可见效果也被严格刻画：状态如何变化、日志如何产生、失败时如何回滚，都遵循可推导的语义流程。确定性并不意味着永远成功，而是意味着“失败或成功”的原因与影响同样可被一致判定。
2 计算模型与运行状态
2.1 状态（state）组成：账户、存储与余额
EVM 运行所依赖的链上状态可概括为若干账户及其相关数据。常见组成包括：
- 账户标识与基本属性（如余额与合约代码所在位置等）
- 合约存储（storage），用于保存合约自己的持久化数据
- 余额（balance），用于表示账户持有的价值，用于支付转账或资金调度
在执行过程中，EVM 通过指令读写合约存储，通过指令更新余额，并在必要时改变账户关联的代码或状态数据。由于这些变化会被写入账本，状态变化的可追溯性是 EVM 语义的重要目标。
2.2 运行上下文：调用栈与消息语义
合约执行往往包含多层调用：一个合约可以调用另一个合约，层层嵌套形成调用链。为刻画这种结构，EVM 使用调用栈（call stack）来管理当前执行帧的上下文。
“消息语义”可理解为：每次调用都携带输入数据、目标地址、转移价值（如有）以及调用方与被调用方之间的关联信息。EVM 的指令会基于当前调用帧读取这些上下文，并在返回时把结果回传给上一层调用。
2.3 内存（memory）与存储（storage）的差异
EVM 中常把“内存（memory）”与“存储（storage）”分开定义，差异体现在可持久化与读写成本的语义上。
- memory：通常是与一次执行相关的临时区，生命周期随执行而结束；读写通常表现为对局部数据的操作。
- storage：用于持久化保存的合约数据，跨交易存在；写入可能影响后续交易的执行结果。
这种区分使得语义层面能够表达：哪些数据只在本次计算中存在，哪些数据进入账本并影响未来的状态转移。
2.4 堆栈（stack）与控制流机制
EVM 指令主要依赖堆栈（stack）来传递操作数：大多数操作码会从栈顶取出若干值进行计算，再把结果压回栈顶。该设计在形式语义上通常表现为“栈效应”（stack effect）：每条指令对栈的元素数量与类型约束有明确描述。
控制流机制则通过跳转类操作码与条件判断来实现。例如，某些指令会根据栈顶条件决定下一条指令的位置，从而形成循环或分支。形式化语义需要同时刻画：在何种栈状态下跳转发生，以及跳转后如何继续执行。
3 指令集与语义
3.1 字节码（bytecode）结构概览
合约通常以字节码形式存在。字节码由操作码（opcode）与其可能携带的数据构成，EVM 根据程序计数器逐步读取并解释。
从形式科学角度，字节码可被视为“语法对象”，而语义则把语法映射为状态转移关系。也就是说：字节码本身提供指令序列；EVM 语义规则规定它在给定状态时如何一步步“运行”。
3.2 操作码（opcode）与栈效应
操作码是执行的基本原子。它们通常伴随固定的栈效应：例如从栈中弹出若干元素、对它们执行算术或逻辑变换、再压入结果。
这种“栈效应”对于形式化分析非常关键，因为它把数据流约束转化为可验证的局部规则。通过对每条操作码建立精确定义，可以进一步推导整个程序的行为特征，例如数值计算如何传播、条件跳转如何依赖栈状态等。
3.3 表达式与算术/逻辑操作的语义
EVM 提供算术、位运算、比较与逻辑相关指令。其语义需要明确诸如：
- 数值在固定位宽下的行为（例如溢出如何处理）
- 比较指令的真值表示方式（例如结果如何编码为整数）
- 逻辑运算与条件分支的衔接方式（值如何影响后续跳转）
在形式化写法中，这些通常被描述为对当前栈元素的函数映射，并返回确定的结果值。
3.4 环境相关指令与外部调用
除内部计算外，EVM 还包含与环境信息相关的指令，例如读取调用上下文、合约地址、调用数据或区块/交易层面的某些字段（具体字段随版本与规范而定）。这类指令把“外部环境”纳入语义，使程序能够依据上下文改变行为。
外部调用相关机制则涉及把控制权交给另一个执行实例，并在返回时获取返回数据与状态影响。形式化语义通常把这种交互表示为：在调用帧创建、参数绑定、子执行评估与返回处理等阶段的组合。
4 Gas（燃料）与资源约束
4.1 Gas 的目的：避免无限计算
EVM 的 gas 机制用于为计算资源设定配额，从而避免恶意程序或意外逻辑导致无限循环或过度消耗资源。其语义意义不仅是“计费”，更是“计算资源边界”的形式化体现：执行不是无约束地进行，而是在每步或每类操作上消耗有限的预算。
从可计算边界的角度看，gas 让“是否终止”与“可计算工作量”之间建立了可刻画的关系。虽然语义不要求程序一定终止，但在资源耗尽时会触发确定的处理流程。
4.2 Gas 计费与执行阶段
在执行过程中，gas 的扣减通常与操作码类别、访问存储的代价、内存扩展等因素有关。规范会对不同操作的成本给出明确规则，并把成本与执行阶段相绑定。
因此，从形式语义上可以把 EVM 执行理解为：每步转移不仅改变状态，还在并行维度上减少 gas 预算。当预算不足以完成下一步所需成本时，执行将进入失败路径。
4.3 失败/回滚与 Gas 消耗的关系
失败通常由两类原因触发：一类是运行时错误或异常条件导致的失败；另一类是资源预算不足。EVM 的语义会指定当执行失败时：
- 当前执行帧对状态的影响是否回滚（通常采用回滚语义，即子执行对状态的写入不保留）
- 发生失败后 gas 如何处理（例如：已经消耗的部分与未消耗部分如何区分）
这种关系使得“回滚不是免费的”，从而在系统层面形成激励与安全边界。
4.4 资源模型的形式化含义
从抽象语义角度，gas 可被建模为额外的度量变量，与操作的转移规则耦合。常见做法是把计算过程视为带资源约束的状态转移系统：状态包含常规存储与控制信息，同时包含剩余预算。
这样一来，很多性质可以被表述为：在给定资源上界时，程序在语义上只能执行有限步；或在特定条件下，执行必然在某个预算边界内结束。
5 合约执行流程
5.1 部署（deployment）过程
部署合约是把一段“初始化逻辑”与合约代码结果绑定的过程。执行部署时，EVM 会运行与合约相关的初始化字节码，用其返回或赋值的结果生成最终合约代码，并把该代码与新账户关联。
部署阶段需要处理输入参数、初始化过程中的状态读写、以及在部署成功后把“合约代码”持久化到新账户。语义上，部署可以看作一种特殊的合约创建：它不仅返回结果，还在链上引入新的可调用实体。
5.2 调用（call）过程与返回值
调用合约时，EVM 需要创建或复用调用帧，绑定参数（包括调用数据与转移价值等），随后从目标合约字节码入口开始执行。
调用过程会产生返回值，并把返回数据（以及可能的失败信息）传回给调用方。返回值的语义还涉及：返回数据如何在内存中安置、调用方如何读取、以及失败时如何影响上层的状态更新与控制流。
5.3 创建合约（contract creation）机制
除部署合约外，合约内部也可能通过创建指令在运行过程中生成新合约。这种机制允许一个合约在执行时产生新的合约实例，并返回新实例的地址。
形式化地讲，合约创建涉及：新账户的生成、初始化字节码的执行、最终代码的固化，以及对新账户状态与调用结果的绑定。与直接部署类似，但它发生在合约执行的嵌套上下文中，因此调用栈与回滚语义会共同影响整体结果。
5.4 事件（logs）与可观测输出
EVM 的可观测输出不仅包括最终状态变化，还包括事件日志（logs）。日志通常由日志指令产生，包含若干可检索字段与数据内容。
在语义层面，日志一般被视为对外可见的记录：它们不直接等同于状态存储的持久化字段，但会被节点用于索引与后续审计。因此，日志的生成规则同样需要被形式化定义，包括何时产生、产生哪些字段以及与回滚是否联动。
6 可验证性与形式语义视角
6.1 一致性：为何所有节点得到同结果
可验证性的一致性依赖于两个方面：一是语义规则的确定性，二是状态更新的可推导性。只要每个节点严格按照规范解释字节码、按同样的成本与资源规则执行、并在失败时按同样的回滚策略处理，那么在相同输入条件下，得到的最终账本状态就应保持一致。
这使得共识能够把“执行正确”转化为可计算验证任务，而不是诉诸实现者的经验。
6.2 终止性与“可计算边界”
EVM 语义并不要求程序一定会成功结束；但 gas 机制提供了“计算边界”。从形式化角度，可以把执行看作在资源度量上运行的过程：只要预算有限，就只能经历有限步的状态转移。
因此，虽然任意字节码序列在不受约束的抽象模型下可能表现出非终止行为，但在 EVM 的资源约束下，执行会以确定方式结束（成功或失败），从而提升语义可分析性。
6.3 语义保持与实现一致
“语义保持”关注的是：形式化语义与实际实现之间的一致性。即便实现语言、优化策略、底层数据结构不同，只要其对外行为满足规范的语义关系，就能被认为与规范一致。
在形式化方法中，这通常对应于证明或验证“实现步骤”与“语义步骤”的对应关系，例如：某个实现的状态转移能否在规范语义中被模拟，或反之是否可由规范语义推导出实现的结果。
6.4 从抽象语义到具体执行的桥接
将抽象语义落地到真实系统，需要解释诸如：内存扩展、存储读写、外部调用、日志输出等细节如何在实现中对应。桥接工作通常涉及：抽象状态到实现状态的映射函数、以及每条指令在具体实现中的数据处理方式。
这类桥接的目标不是“让实现更像数学”，而是确保数学规则能预测实现行为，并让形式分析结果能够对真实执行提供可靠保证。
7 形式化方法相关应用（面向形式科学）
7.1 形式验证的输入对象：字节码与语义规则
在形式验证中，常见输入对象包括：待验证的字节码程序，以及该字节码所遵循的语义规则。验证任务可以是对程序性质进行证明，也可以是对实现的正确性进行约束检查。
由于 EVM 语义强调可确定推导，形式验证通常能够把“程序行为”转化为“逻辑命题”或“可达性问题”，从而采用自动化或半自动化的推理工具。
7.2 规格与模型的常见抽象层
规格（specification）往往以不变量、前置/后置条件、或时序性质等形式给出。抽象层的选择影响可验证性：
- 细粒度：直接对指令级语义建模，能更精确但成本更高
- 中粒度：对栈、内存、存储的抽象进行归纳，保留关键数据流
- 高层抽象：对合约行为模式进行概括，以更少细节表达性质
常见目标是在保证结论可靠的同时，尽量降低验证所需的状态空间。
7.3 正确性性质：安全性与一致性
形式化方法中常验证的性质包括安全性（safety）与一致性（consistency）等类型。例如：
- 指定某些恶意行为路径不可达
- 确保失败回滚与日志输出在规范下保持一致
- 保证特定状态不变量在执行中不被破坏
在一致性方面，常把“语义规则导致的结果”作为参照，证明程序在满足前提条件时与期望行为一致。
7.4 工具化验证的常见路径（示例性）
工具化路径通常遵循从语义建模到推理求解的链条。例如：
1 EVM 概念与定位
2 计算模型与运行状态
3 指令集与语义
4 Gas（燃料）与资源约束
此处属于示例性概括；具体工具与方法会根据研究路线与目标性质而变化，但总体思路是把执行语义与逻辑推理衔接起来。
8 约定俗成的生态术语（轻松梗向）
8.1 “EVM 里一切都是栈”的流行说法
在开发者圈层里常会调侃：“EVM 里一切都是栈”。这类说法的核心是强调 EVM 的计算很大程度依赖堆栈传递数据：算术、比较、跳转等指令都围绕栈顶数据运转。它当然不等同于 EVM 的全部结构（还有内存、存储、上下文等），但用作口头记忆法确实很贴切。
8.2 Gas：程序员的“精算焦虑”来源
gas 常被视为程序员的“精算焦虑”。原因在于：同一逻辑在不同写法下可能产生不同成本；而预算不足会导致失败，让“功能正确”还不够，得“成本可控”才算稳妥。于是优化与估算成为日常工作的一部分，形成了带有情绪色彩的术语共识。
8.3 回滚（revert）与“白忙一场”的直觉比喻
回滚在直觉上常被比作“白忙一场”：执行过程中状态变更可能被撤销，最终呈现为失败结果。不过需要注意的是，回滚语义并不代表计算毫无代价，gas 仍会消耗。因此“白忙一场”更多体现心理落差，而不是对资源事实的准确描述。
8.4 调试语境中的常见误区与笑点
调试语境里也有不少口头梗：例如把“看见事件/返回数据”误当作“状态一定成功更新”，或把“某段指令没报错”当作“整体语义必然成功”。这些误区之所以反复出现，是因为执行结果与日志、返回值、回滚状态之间需要严格对应语义规则才能下结论。