SolidityABI:Isabelle形式化的Solidity ABI编码和解码 源码

经验证的Solidity ABI编码器/解码器 该存储库包含编码器和解码器的规范,实现和验证(在Isabelle中)。 注意:此开发尚未针对Isabelle2021更新。 它应与Isabelle2020一起使用。 存储库的结构如下: ABI类型和其他基本概念: AbiTypes.thy Isabelle用于编写ABI类型的语法糖: AbiTypesSyntax.thy 编码器和解码器实现中使用的错误消息的构造: Ok.thy 正式AbiEncodeSpec.thy ABI编码规范: AbiEncodeSpec.thy 编码器实现: AbiEncode.thy 解码器实现: AbiDecode.thy 编码器正确性定理: AbiEncodeCorrect.thy 解码器正确性定理: AbiDecodeCorrect.thy 关于解码编码结果的“往返”定理(反之亦然):