文件名称：SolidityABI:Isabelle形式化的Solidity ABI编码和解码
文件大小：118KB
文件格式：ZIP
更新时间：2024-03-30 22:25:40
Isabelle
经验证的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 关于解码编码结果的“往返”定理（反之亦然）：
【文件预览】：
SolidityABI-master
----AbiDecode.thy(18KB)
----AbiEncodeSpec.thy(4KB)
----AbiTypesSyntax.thy(13KB)
----ROOT(323B)
----Hex.thy(9KB)
----Ok.thy(915B)
----AbiDecodeCorrect.thy(240KB)
----AbiEncode.thy(7KB)
----YulSyntaxOld.thy(6KB)
----AbiTests()
--------FBytes16.thy(876B)
--------FArray.thy(1KB)
--------FBytes.thy(852B)
--------FArray_Tuple.thy(2KB)
--------Ufixed.thy(0B)
--------Array_Array.thy(3KB)
--------BytesOdd.thy(1KB)
--------StringTest.thy(1KB)
--------Bytes.thy(1KB)
--------Tuple_Tuple.thy(2KB)
--------Tuple.thy(1KB)
--------Uint160.thy(731B)
--------FArray_Bytes.thy(170B)
--------Sint160.thy(753B)
--------Address.thy(801B)
--------Uint256.thy(887B)
--------FArray_FArray.thy(2KB)
--------Sint256.thy(897B)
--------Bool.thy(690B)
--------FBytes32.thy(930B)
--------Tuple_Array_Tuple.thy(5KB)
--------Tuple_FArray.thy(2KB)
--------Tuple_Array.thy(3KB)
--------Farray_Array.thy(3KB)
--------Array_FArray.thy(2KB)
--------Array_Tuple.thy(3KB)
--------NonCanonical_Overlap.thy(3KB)
--------Array_Tuple_Array.thy(8KB)
--------Array.thy(2KB)
--------Fixed.thy(0B)
----Inverses.thy(2KB)
----WordUtils.thy(539B)
----AbiTypes.thy(12KB)
----YulSemantics.thy(18KB)
----AbiEncodeCorrect.thy(147KB)
----YulSemanticsOld.thy(9KB)
----README.md(1KB)
----Export.thy(17KB)
----libabicoder()
--------abicoder.cpp(3KB)
--------test.cpp(787B)
--------abicoder.hpp(661B)
--------abicoder.mlb(63B)
--------export()
--------Makefile(1KB)
--------mlton_export.sml(661B)
----LICENSE.txt(1KB)
----YulSyntaxUtils.thy(4KB)