evm semantics:以太坊虚拟机(EVM)的K语义 源码

KEVM:K中的EVM语义 在此存储库中,我们提供了K中的EVM模型。 文档/支持 这些对于学习KEVM和K(最新到最旧)可能很有用: ,使用。 在。 ,尤其是第3和第5节。 。 要获得对KEVM的支持,请加入我们的。 储存库结构 以下文件构成了KEVM语义: 提供在执行异常时报告给以太坊客户端的状态代码。 是K中JSON RPC的实现。 提供EVM的(功能性)数据(256位字,字堆栈等)。 提供了用于解析和解析数据(十六进制字符串,递归长度前缀,merkle树等)的帮助器。 是主要的KEVM语义,包含EVM的配置和转换规则。 这些附加文件扩展了语义,使存储库更有用: 定义了#buf字节缓冲区抽象,供在符号执行期间使用。 定义了,用于证明和简单的合同/功能规范。 定义了#hashedLocation抽象,这使指定#hashedLocation生成的存储布局更加