This software package satisfies these specifications with these assumptions (see below). Specifically, everything shown with green text or background is auto-certified by VeriLib (and you can trivially re-verify it yourself), while what's shown with white background are unverified claims by the project team, included for pedagogy.
lean-zip is a Lean 4 library that provides compression and archive support for zlib (RFC 1950), gzip (RFC 1952), raw DEFLATE (RFC 1951), tar, and ZIP formats. It offers two implementation paths:
The formal verification effort covers the pure Lean native implementations in Zip/Native/ and their specifications in Zip/Spec/. The library proves roundtrip correctness — that compressing and then decompressing data returns the original input — for the DEFLATE, gzip, and zlib formats across all compression levels (0–9).
lean-zip was autoformalized from zlib (a C compression library) to Lean by a general-purpose AI, with no special training for theorem proving. If lean-zip is a faithful translation of zlib, then this verification of lean-zip would imply the correctness of zlib.
| # | Property/Area | Description | File | Theorem |
|---|---|---|---|---|
| 1 | DEFLATE Roundtrip | Unified roundtrip for all compression levels 0–9: inflate (deflateRaw data level) = .ok data |
Zip/Spec/DeflateRoundtrip.lean |
inflate_deflateRaw |
| 2 | Gzip Roundtrip | Gzip format roundtrip with CRC-32 verification (RFC 1952) | Zip/Spec/GzipCorrect.lean |
gzip_decompressSingle_compress |
| 3 | Zlib Roundtrip | Zlib format roundtrip with Adler-32 verification (RFC 1950) | Zip/Spec/ZlibCorrect.lean |
zlib_decompressSingle_compress |
| 4 | Decoder Correctness | Native inflate agrees with formal bitstream specification | Zip/Spec/InflateCorrect.lean |
inflate_correct |
| 5 | Decoder Completeness | All spec-valid inputs are accepted by the decoder | Zip/Spec/InflateComplete.lean |
inflateLoop_complete |
| 6 | Huffman Prefix-Free | Canonical Huffman codes are prefix-free | Zip/Spec/HuffmanTheorems.lean |
canonical_prefix_free |
| 7 | LZ77 Greedy Correctness | Greedy LZ77 matcher produces valid decomposition | Zip/Spec/LZ77NativeCorrect.lean |
lz77Greedy_resolves |
| 8 | LZ77 Lazy Correctness | Lazy LZ77 matcher produces valid decomposition | Zip/Spec/LZ77NativeCorrect.lean |
lz77Lazy_resolves |
We assume that the Lean kernel is sound, and that the Lean verification system correctly implements its verification logic based on sound reasoning principles.
As with any software, we trust that the hardware correctly executes the compiled machine code.
The zlib C library, C compiler (cc), and pkg-config are required for the unverified FFI path only. These system dependencies are trusted without formal proof.
Lean's standard axioms (propext, Quot.sound, Classical.choice; no custom axioms). lean-zip-common (Git @ 87480b0): shared utilities checked by the kernel.
Only the pure Lean native path (Zip/Native/) is formally verified. The C FFI path (wrapping system zlib), tar/ZIP archive support, and streaming APIs are tested for conformance but not formally proven.
RFC 1950 (Zlib), RFC 1951 (DEFLATE), RFC 1952 (GZIP), ISO 3309 / ITU-T V.42 (CRC-32).
Below are the formal verification results. Please check if the first test line says "VerificationSuccess": true.
{
"VerificationSuccess": true,
"branch": "master",
"build_arg_commit": "78e5bd6950afdda3ab88dbd567e54bc6adedf3ae",
"cert_readme_badge_alt": "VeriLib Certified",
"cert_readme_badge_image_url": "https://verilib.org/assets/img/verilib-certified-badge-wide.svg",
"cert_readme_page_url": "https://verilib.org/cert/5165",
"commit": "78e5bd6950afdda3ab88dbd567e54bc6adedf3ae",
"commit_date_utc": null,
"image": "verilib/probe-lean-repo-5165:1",
"image_build_date_utc": "2026-04-17T10:40:37Z",
"probe_extract_completed_at_utc": "2026-04-17T10:40:37Z",
"probe_lean_version": "0.6.2",
"repo": "https://github.com/kim-em/lean-zip.git",
"source_tree_sha256": "ce1e5ee20b158cb8ac9809e2a06bb34939d0ae3891d92853bab4cda2098986ee",
"to_be_verified": 773,
"unified_extract_json_path": "probe_extract.json",
"unified_extract_json_sha256": "8ca0933ce3961c6e3c6fc2dd2709c79561c21b84228e2e2081ba81f152ee4068",
"verification_source": "unified_extract_json",
"verified_functions": [
"probe:Adler32.Native.adler32",
"probe:Adler32.Native.updateBytes",
"probe:Adler32.Native.updateBytes_eq_updateList",
"probe:Adler32.Native.updateBytes_valid",
"probe:Adler32.Spec.MOD_ADLER",
"probe:Adler32.Spec.State",
"probe:Adler32.Spec.Valid",
"probe:Adler32.Spec.checksum",
"probe:Adler32.Spec.init",
"probe:Adler32.Spec.init_valid",
"probe:Adler32.Spec.pack",
"probe:Adler32.Spec.unpack",
"probe:Adler32.Spec.updateByte",
"probe:Adler32.Spec.updateByte_fst_lt",
"probe:Adler32.Spec.updateByte_snd_lt",
"probe:Adler32.Spec.updateByte_valid",
"probe:Adler32.Spec.updateList",
"probe:Adler32.Spec.updateList_append",
"probe:Adler32.Spec.updateList_cons",
"probe:Adler32.Spec.updateList_nil",
"probe:Adler32.Spec.updateList_valid",
"probe:Archive.Entry",
"probe:Archive.Entry.compressedSize",
"probe:Archive.Entry.crc32",
"probe:Archive.Entry.localOffset",
"probe:Archive.Entry.method",
"probe:Archive.Entry.path",
"probe:Archive.Entry.uncompressedSize",
"probe:Archive.create",
"probe:Archive.createFromDir",
"probe:Archive.extract",
"probe:Archive.extractFile",
"probe:Archive.instInhabitedEntry",
"probe:Archive.instInhabitedEntry.default",
"probe:Archive.instReprEntry",
"probe:Archive.instReprEntry.repr",
"probe:Archive.list",
"probe:Archive.readExactStream",
"probe:ByteArray.beq",
"probe:Checksum.adler32",
"probe:Checksum.crc32",
"probe:Crc32.Native.crc32",
"probe:Crc32.Native.crcBit_xor_high",
"probe:Crc32.Native.crcByteTable_eq_crcByte",
"probe:Crc32.Native.table",
"probe:Crc32.Native.table_size",
"probe:Crc32.Native.updateBytes",
"probe:Crc32.Native.updateBytes_eq_updateList",
"probe:Crc32.Spec.POLY",
"probe:Crc32.Spec.checksum",
"probe:Crc32.Spec.crcBit",
"probe:Crc32.Spec.crcByte",
"probe:Crc32.Spec.crcByteTable",
"probe:Crc32.Spec.mkTable",
"probe:Crc32.Spec.updateList",
"probe:Crc32.Spec.updateList_append",
"probe:Crc32.Spec.updateList_nil",
"probe:Deflate.Correctness.Deflate.Correctness.fixedDistLengths_eq",
"probe:Deflate.Correctness.Deflate.Correctness.fixedDistLengths_size",
"probe:Deflate.Correctness.Deflate.Correctness.fixedLitLengths_eq",
"probe:Deflate.Correctness.Deflate.Correctness.fixedLitLengths_size",
"probe:Deflate.Correctness.NoLeafOnPath",
"probe:Deflate.Correctness.TreeHasLeaf",
"probe:Deflate.Correctness.acc_or_shift_bound",
"probe:Deflate.Correctness.acc_or_shift_toNat",
"probe:Deflate.Correctness.alignToByte_data",
"probe:Deflate.Correctness.alignToByte_id_of_aligned",
"probe:Deflate.Correctness.alignToByte_toBits",
"probe:Deflate.Correctness.alignToByte_wf",
"probe:Deflate.Correctness.bfinal_beq_nat_false",
"probe:Deflate.Correctness.bfinal_beq_nat_true",
"probe:Deflate.Correctness.bytesToBits_bitsToBytes_aligned",
"probe:Deflate.Correctness.bytesToBits_bitsToBytes_take",
"probe:Deflate.Correctness.bytesToBits_drop_testBit",
"probe:Deflate.Correctness.canonicalCodes_correct_pos",
"probe:Deflate.Correctness.canonicalCodes_correct_zero",
"probe:Deflate.Correctness.canonicalCodes_go_size",
"probe:Deflate.Correctness.canonicalCodes_hasLeaf",
"probe:Deflate.Correctness.codeFor_some",
"probe:Deflate.Correctness.copyLoop_eq_ofFn",
"probe:Deflate.Correctness.count_foldl_take_le",
"probe:Deflate.Correctness.decodeBits",
"probe:Deflate.Correctness.decodeBits_of_hasLeaf",
"probe:Deflate.Correctness.decodeCLSymbols_complete",
"probe:Deflate.Correctness.decodeCLSymbols_inv",
"probe:Deflate.Correctness.decodeDynamicTables_rest_le",
"probe:Deflate.Correctness.decodeDynamicTrees_complete",
"probe:Deflate.Correctness.decodeDynamicTrees_correct",
"probe:Deflate.Correctness.decodeHuffman_complete",
"probe:Deflate.Correctness.decodeHuffman_correct",
"probe:Deflate.Correctness.decodeStored_complete",
"probe:Deflate.Correctness.decodeStored_correct",
"probe:Deflate.Correctness.decodeStored_invariants",
"probe:Deflate.Correctness.decodeStored_rest_le",
"probe:Deflate.Correctness.decodeSymbols_rest_le",
"probe:Deflate.Correctness.decode_go_complete",
"probe:Deflate.Correctness.decode_go_decodeBits",
"probe:Deflate.Correctness.decode_pos_inv",
"probe:Deflate.Correctness.decode_some_mem",
"probe:Deflate.Correctness.decode_wf",
"probe:Deflate.Correctness.distBase_eq",
"probe:Deflate.Correctness.distExtra_eq",
"probe:Deflate.Correctness.distExtra_le_32",
"probe:Deflate.Correctness.fillEntries_extract",
"probe:Deflate.Correctness.fillEntries_size",
"probe:Deflate.Correctness.fillEntries_snd",
"probe:Deflate.Correctness.fromLengths_complete",
"probe:Deflate.Correctness.fromLengths_hasLeaf",
"probe:Deflate.Correctness.fromLengths_leaf_spec",
"probe:Deflate.Correctness.fromLengths_valid",
"probe:Deflate.Correctness.hasLeaf_of_decodeBits",
"probe:Deflate.Correctness.huffTree_decode_complete",
"probe:Deflate.Correctness.huffTree_decode_correct",
"probe:Deflate.Correctness.inflateLoop_complete",
"probe:Deflate.Correctness.inflateLoop_correct",
"probe:Deflate.Correctness.inflateLoop_fuel_le",
"probe:Deflate.Correctness.inflate_correct",
"probe:Deflate.Correctness.inflate_correct'",
"probe:Deflate.Correctness.insert_go_complete'",
"probe:Deflate.Correctness.insert_go_hasLeaf",
"probe:Deflate.Correctness.insert_go_noLeafOnPath",
"probe:Deflate.Correctness.insert_go_preserves",
"probe:Deflate.Correctness.lengthBase_eq",
"probe:Deflate.Correctness.lengthExtra_eq",
"probe:Deflate.Correctness.lengthExtra_le_32",
"probe:Deflate.Correctness.nat_beq_to_uint32_false",
"probe:Deflate.Correctness.nat_beq_to_uint32_true",
"probe:Deflate.Correctness.readBit_complete",
"probe:Deflate.Correctness.readBit_toBits",
"probe:Deflate.Correctness.readBit_wf",
"probe:Deflate.Correctness.readBitsLSB_split",
"probe:Deflate.Correctness.readBitsLSB_writeBitsLSB",
"probe:Deflate.Correctness.readBits_complete",
"probe:Deflate.Correctness.readBits_go_complete",
"probe:Deflate.Correctness.readBits_pos_inv",
"probe:Deflate.Correctness.readBits_toBits",
"probe:Deflate.Correctness.readBits_wf",
"probe:Deflate.Correctness.readBytes_complete",
"probe:Deflate.Correctness.readBytes_toBits",
"probe:Deflate.Correctness.readBytes_wf",
"probe:Deflate.Correctness.readCLCodeLengths_complete",
"probe:Deflate.Correctness.readCLCodeLengths_size",
"probe:Deflate.Correctness.readNBytes_aligned",
"probe:Deflate.Correctness.readNBytes_output_length",
"probe:Deflate.Correctness.readNBytes_some_length",
"probe:Deflate.Correctness.readUInt16LE_complete",
"probe:Deflate.Correctness.readUInt16LE_data",
"probe:Deflate.Correctness.readUInt16LE_toBits",
"probe:Deflate.Correctness.readUInt16LE_wf",
"probe:Deflate.Correctness.specTable_cw_nonempty",
"probe:Deflate.Correctness.specTable_mem_codes",
"probe:Deflate.Correctness.symVal_of_beq",
"probe:Deflate.Correctness.toBits_length",
"probe:Deflate.Correctness.toBits_nonempty_pos",
"probe:Deflate.Correctness.toBits_readBitsLSB_byte",
"probe:Deflate.Correctness.uint32_bit_eq_testBit",
"probe:Deflate.Correctness.uint32_testBit",
"probe:Deflate.Correctness.validLengths_toUInt8_roundtrip",
"probe:Deflate.Correctness.writeBitsLSB_length",
"probe:Deflate.Spec.CLEntry",
"probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code16",
"probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code17",
"probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code18",
"probe:Deflate.Spec.Deflate.Spec.rlDecode_go_literal",
"probe:Deflate.Spec.LZ77Symbol",
"probe:Deflate.Spec.ValidSymbolList",
"probe:Deflate.Spec.alignToByte",
"probe:Deflate.Spec.bitsToByte",
"probe:Deflate.Spec.bitsToBytes",
"probe:Deflate.Spec.bitsToBytes.go",
"probe:Deflate.Spec.bitsToNat",
"probe:Deflate.Spec.bytesToBits",
"probe:Deflate.Spec.bytesToBits.byteToBits",
"probe:Deflate.Spec.bytesToBits.byteToBits_length",
"probe:Deflate.Spec.bytesToBits_length",
"probe:Deflate.Spec.clPermutation",
"probe:Deflate.Spec.clPermutation_length",
"probe:Deflate.Spec.clSymbolFreqs",
"probe:Deflate.Spec.clSymbolFreqs_length",
"probe:Deflate.Spec.clSymbolFreqs_pos",
"probe:Deflate.Spec.codeLengthOrder",
"probe:Deflate.Spec.computeHCLEN",
"probe:Deflate.Spec.computeHCLEN_ge_four",
"probe:Deflate.Spec.computeHCLEN_le_nineteen",
"probe:Deflate.Spec.countRun",
"probe:Deflate.Spec.countRun_le_length",
"probe:Deflate.Spec.countRun_take",
"probe:Deflate.Spec.decode",
"probe:Deflate.Spec.decode.go",
"probe:Deflate.Spec.decode.goR",
"probe:Deflate.Spec.decodeDynamicTables",
"probe:Deflate.Spec.decodeDynamicTables.decodeCLSymbols",
"probe:Deflate.Spec.decodeDynamicTables_append",
"probe:Deflate.Spec.decodeDynamicTables_valid_dist",
"probe:Deflate.Spec.decodeDynamicTables_valid_lit",
"probe:Deflate.Spec.decodeLitLen",
"probe:Deflate.Spec.decodeLitLen_append",
"probe:Deflate.Spec.decodeLitLen_of_endOfBlock",
"probe:Deflate.Spec.decodeLitLen_of_literal",
"probe:Deflate.Spec.decodeStored",
"probe:Deflate.Spec.decodeStored.readNBytes",
"probe:Deflate.Spec.decodeStored_append",
"probe:Deflate.Spec.decodeSymbols",
"probe:Deflate.Spec.decodeSymbols_append",
"probe:Deflate.Spec.decode_deterministic",
"probe:Deflate.Spec.decode_goR_exists",
"probe:Deflate.Spec.decode_goR_fst",
"probe:Deflate.Spec.decode_go_acc_prefix",
"probe:Deflate.Spec.decode_go_suffix",
"probe:Deflate.Spec.deflateLevel1_spec_roundtrip",
"probe:Deflate.Spec.deflateLevel1_spec_roundtrip'",
"probe:Deflate.Spec.deflateLevel2_spec_roundtrip",
"probe:Deflate.Spec.deflateStoredPure_goR",
"probe:Deflate.Spec.distBase",
"probe:Deflate.Spec.distExtra",
"probe:Deflate.Spec.encodeCLEntries",
"probe:Deflate.Spec.encodeCLEntries_isSome",
"probe:Deflate.Spec.encodeCLExtra",
"probe:Deflate.Spec.encodeDynamicTrees",
"probe:Deflate.Spec.encodeDynamicTrees_decodeDynamicTables",
"probe:Deflate.Spec.encodeDynamic_decode_append",
"probe:Deflate.Spec.encodeDynamic_goR_rest",
"probe:Deflate.Spec.encodeFixed",
"probe:Deflate.Spec.encodeFixed_decode",
"probe:Deflate.Spec.encodeFixed_decode_append",
"probe:Deflate.Spec.encodeFixed_goR_rest",
"probe:Deflate.Spec.encodeLitLen",
"probe:Deflate.Spec.encodeLitLen_decodeLitLen",
"probe:Deflate.Spec.encodeLitLen_endOfBlock_isSome",
"probe:Deflate.Spec.encodeLitLen_literal_isSome",
"probe:Deflate.Spec.encodeLitLen_nonempty",
"probe:Deflate.Spec.encodeLitLen_reference_isSome",
"probe:Deflate.Spec.encodeStored",
"probe:Deflate.Spec.encodeStored_decode",
"probe:Deflate.Spec.encodeStored_decode_goR",
"probe:Deflate.Spec.encodeSymbol",
"probe:Deflate.Spec.encodeSymbol_decode",
"probe:Deflate.Spec.encodeSymbol_fixed_isSome",
"probe:Deflate.Spec.encodeSymbol_isSome",
"probe:Deflate.Spec.encodeSymbol_mem",
"probe:Deflate.Spec.encodeSymbols",
"probe:Deflate.Spec.encodeSymbols_decodeSymbols",
"probe:Deflate.Spec.encodeSymbols_isSome_of_all",
"probe:Deflate.Spec.findDistCode",
"probe:Deflate.Spec.findDistCode.go",
"probe:Deflate.Spec.findDistCode_code_bound",
"probe:Deflate.Spec.findDistCode_isSome",
"probe:Deflate.Spec.findDistCode_spec",
"probe:Deflate.Spec.findDistCode_upper",
"probe:Deflate.Spec.findLengthCode",
"probe:Deflate.Spec.findLengthCode.go",
"probe:Deflate.Spec.findLengthCode_idx_bound",
"probe:Deflate.Spec.findLengthCode_isSome",
"probe:Deflate.Spec.findLengthCode_spec",
"probe:Deflate.Spec.findLengthCode_upper",
"probe:Deflate.Spec.findLongestMatch",
"probe:Deflate.Spec.findLongestMatch.go",
"probe:Deflate.Spec.findLongestMatch_dist_bounds",
"probe:Deflate.Spec.findLongestMatch_dist_le_windowSize",
"probe:Deflate.Spec.findLongestMatch_end_le",
"probe:Deflate.Spec.findLongestMatch_len_ge",
"probe:Deflate.Spec.findLongestMatch_matchLength",
"probe:Deflate.Spec.fixedDistCodes_prefix_free",
"probe:Deflate.Spec.fixedDistLengths",
"probe:Deflate.Spec.fixedDistLengths_entry_bounds",
"probe:Deflate.Spec.fixedDistLengths_getElem_le",
"probe:Deflate.Spec.fixedDistLengths_getElem_pos",
"probe:Deflate.Spec.fixedDistLengths_length",
"probe:Deflate.Spec.fixedDistLengths_valid",
"probe:Deflate.Spec.fixedLitCodes_prefix_free",
"probe:Deflate.Spec.fixedLitLengths",
"probe:Deflate.Spec.fixedLitLengths_entry_bounds",
"probe:Deflate.Spec.fixedLitLengths_getElem_le",
"probe:Deflate.Spec.fixedLitLengths_getElem_pos",
"probe:Deflate.Spec.fixedLitLengths_length",
"probe:Deflate.Spec.fixedLitLengths_valid",
"probe:Deflate.Spec.flipped_allCodes_prefix_free",
"probe:Deflate.Spec.instBEqLZ77Symbol",
"probe:Deflate.Spec.instBEqLZ77Symbol.beq",
"probe:Deflate.Spec.instReprLZ77Symbol",
"probe:Deflate.Spec.instReprLZ77Symbol.repr",
"probe:Deflate.Spec.lengthBase",
"probe:Deflate.Spec.lengthExtra",
"probe:Deflate.Spec.matchLZ77",
"probe:Deflate.Spec.matchLZ77.go",
"probe:Deflate.Spec.matchLZ77Lazy",
"probe:Deflate.Spec.matchLZ77Lazy.go",
"probe:Deflate.Spec.matchLZ77Lazy_encodable",
"probe:Deflate.Spec.matchLZ77Lazy_length_le",
"probe:Deflate.Spec.matchLZ77Lazy_validSymbolList",
"probe:Deflate.Spec.matchLZ77_encodable",
"probe:Deflate.Spec.matchLZ77_length_le",
"probe:Deflate.Spec.matchLZ77_validSymbolList",
"probe:Deflate.Spec.matchLength",
"probe:Deflate.Spec.matchLength.go",
"probe:Deflate.Spec.matchLength.go_bounds",
"probe:Deflate.Spec.matchLength.go_correct",
"probe:Deflate.Spec.matchLength.go_in_bounds",
"probe:Deflate.Spec.matchLength_correct",
"probe:Deflate.Spec.matchLength_in_bounds",
"probe:Deflate.Spec.matchLength_le_258",
"probe:Deflate.Spec.readBitsLSB",
"probe:Deflate.Spec.readBitsLSB_append",
"probe:Deflate.Spec.readBitsLSB_bound",
"probe:Deflate.Spec.readBitsLSB_some_length",
"probe:Deflate.Spec.readCLLengths",
"probe:Deflate.Spec.readCLLengths_writeCLLengths",
"probe:Deflate.Spec.resolveLZ77",
"probe:Deflate.Spec.resolveLZ77_endOfBlock",
"probe:Deflate.Spec.resolveLZ77_endOfBlock_empty",
"probe:Deflate.Spec.resolveLZ77_extends",
"probe:Deflate.Spec.resolveLZ77_literal",
"probe:Deflate.Spec.resolveLZ77_literal_cons",
"probe:Deflate.Spec.resolveLZ77_literals",
"probe:Deflate.Spec.resolveLZ77_matchLZ77",
"probe:Deflate.Spec.resolveLZ77_matchLZ77Lazy",
"probe:Deflate.Spec.resolveLZ77_nil",
"probe:Deflate.Spec.resolveLZ77_reference_dist_too_large",
"probe:Deflate.Spec.resolveLZ77_reference_dist_zero",
"probe:Deflate.Spec.resolveLZ77_reference_valid",
"probe:Deflate.Spec.rlDecodeLengths",
"probe:Deflate.Spec.rlDecodeLengths.go",
"probe:Deflate.Spec.rlDecodeLengths_go_rlEncodeLengths_go",
"probe:Deflate.Spec.rlDecodeLengths_rlEncodeLengths",
"probe:Deflate.Spec.rlEncodeLengths",
"probe:Deflate.Spec.rlEncodeLengths.go",
"probe:Deflate.Spec.rlEncodeLengths_go_valid",
"probe:Deflate.Spec.rlEncodeLengths_valid",
"probe:Deflate.Spec.take_countRun_eq_replicate",
"probe:Deflate.Spec.writeBitsLSB",
"probe:Deflate.Spec.writeCLLengths",
"probe:Gzip.DeflateState",
"probe:Gzip.DeflateState.finish",
"probe:Gzip.DeflateState.new",
"probe:Gzip.DeflateState.nonemptyType",
"probe:Gzip.DeflateState.push",
"probe:Gzip.InflateState",
"probe:Gzip.InflateState.finish",
"probe:Gzip.InflateState.new",
"probe:Gzip.InflateState.nonemptyType",
"probe:Gzip.InflateState.push",
"probe:Gzip.compress",
"probe:Gzip.compressFile",
"probe:Gzip.compressStream",
"probe:Gzip.decompress",
"probe:Gzip.decompressFile",
"probe:Gzip.decompressStream",
"probe:Gzip.instNonemptyDeflateState",
"probe:Gzip.instNonemptyInflateState",
"probe:Huffman.Spec.BuildTree",
"probe:Huffman.Spec.BuildTree.depths",
"probe:Huffman.Spec.BuildTree.depths_ge",
"probe:Huffman.Spec.BuildTree.depths_ne_nil",
"probe:Huffman.Spec.BuildTree.kraft_eq",
"probe:Huffman.Spec.BuildTree.weight",
"probe:Huffman.Spec.Codeword",
"probe:Huffman.Spec.IsPrefixFree",
"probe:Huffman.Spec.ValidLengths",
"probe:Huffman.Spec.allCodeWords_prefix_free",
"probe:Huffman.Spec.allCodes",
"probe:Huffman.Spec.allCodes_mem_iff",
"probe:Huffman.Spec.allCodes_nodup",
"probe:Huffman.Spec.allCodes_prefix_free_of_ne",
"probe:Huffman.Spec.assignLengths",
"probe:Huffman.Spec.assignLengths_bounded",
"probe:Huffman.Spec.assignLengths_length",
"probe:Huffman.Spec.assignLengths_pos",
"probe:Huffman.Spec.buildHuffmanTree",
"probe:Huffman.Spec.buildTree_depths_nonempty",
"probe:Huffman.Spec.canonical_prefix_free",
"probe:Huffman.Spec.codeFor",
"probe:Huffman.Spec.codeFor_injective",
"probe:Huffman.Spec.codeFor_len_bounds",
"probe:Huffman.Spec.codeFor_spec",
"probe:Huffman.Spec.code_value_bound",
"probe:Huffman.Spec.computeCodeLengths",
"probe:Huffman.Spec.computeCodeLengths_bounded",
"probe:Huffman.Spec.computeCodeLengths_length",
"probe:Huffman.Spec.computeCodeLengths_nonzero",
"probe:Huffman.Spec.computeCodeLengths_valid",
"probe:Huffman.Spec.countLengths",
"probe:Huffman.Spec.countLengths_eq",
"probe:Huffman.Spec.count_foldl_mono",
"probe:Huffman.Spec.count_le_pow_of_validLengths",
"probe:Huffman.Spec.decode",
"probe:Huffman.Spec.decode_deterministic",
"probe:Huffman.Spec.decode_prefix_free",
"probe:Huffman.Spec.decode_shorter",
"probe:Huffman.Spec.decode_some_append",
"probe:Huffman.Spec.decode_suffix",
"probe:Huffman.Spec.fixKraftList",
"probe:Huffman.Spec.fixKraftList_bounded",
"probe:Huffman.Spec.fixKraftList_kraft",
"probe:Huffman.Spec.fixKraftList_length",
"probe:Huffman.Spec.fixKraftList_nonzero",
"probe:Huffman.Spec.insertByWeight",
"probe:Huffman.Spec.insertByWeight_length",
"probe:Huffman.Spec.instDecidableValidLengths",
"probe:Huffman.Spec.instReprBuildTree",
"probe:Huffman.Spec.instReprBuildTree.repr",
"probe:Huffman.Spec.isPrefixOf",
"probe:Huffman.Spec.isPrefixOf_iff",
"probe:Huffman.Spec.kraftSum",
"probe:Huffman.Spec.natToBits",
"probe:Huffman.Spec.natToBits_eq_iff",
"probe:Huffman.Spec.natToBits_injective",
"probe:Huffman.Spec.natToBits_length",
"probe:Huffman.Spec.ncRec",
"probe:Huffman.Spec.ncRec_shift",
"probe:Huffman.Spec.nextCodes",
"probe:Huffman.Spec.nextCodes.go",
"probe:Huffman.Spec.nextCodes_eq_ncRec",
"probe:Huffman.Spec.nextCodes_plus_count_le",
"probe:Huffman.Spec.nextCodes_size",
"probe:Huffman.Spec.validLengths_cons",
"probe:RawDeflate.DeflateState.new",
"probe:RawDeflate.InflateState.new",
"probe:RawDeflate.compress",
"probe:RawDeflate.compressStream",
"probe:RawDeflate.decompress",
"probe:RawDeflate.decompressStream",
"probe:Tar.Entry",
"probe:Tar.Entry.gid",
"probe:Tar.Entry.gname",
"probe:Tar.Entry.linkname",
"probe:Tar.Entry.mode",
"probe:Tar.Entry.mtime",
"probe:Tar.Entry.path",
"probe:Tar.Entry.size",
"probe:Tar.Entry.typeflag",
"probe:Tar.Entry.uid",
"probe:Tar.Entry.uname",
"probe:Tar.applyPaxOverrides",
"probe:Tar.buildHeader",
"probe:Tar.buildPaxEntry",
"probe:Tar.buildPaxRecord",
"probe:Tar.computeChecksum",
"probe:Tar.create",
"probe:Tar.createFromDir",
"probe:Tar.createTarGz",
"probe:Tar.extract",
"probe:Tar.extractTarGz",
"probe:Tar.extractTarGzNative",
"probe:Tar.instInhabitedEntry",
"probe:Tar.instInhabitedEntry.default",
"probe:Tar.instReprEntry",
"probe:Tar.instReprEntry.repr",
"probe:Tar.list",
"probe:Tar.needsPaxHeader",
"probe:Tar.paddingFor",
"probe:Tar.parseHeader",
"probe:Tar.parsePaxRecords",
"probe:Tar.readNumeric",
"probe:Tar.splitPath",
"probe:Tar.typeDirectory",
"probe:Tar.typeGnuLongLink",
"probe:Tar.typeGnuLongName",
"probe:Tar.typePaxExtended",
"probe:Tar.typePaxGlobal",
"probe:Tar.typeRegular",
"probe:Tar.typeSymlink",
"probe:Tar.verifyChecksum",
"probe:Zip.Native.BitWriter",
"probe:Zip.Native.BitWriter.bitBuf",
"probe:Zip.Native.BitWriter.bitCount",
"probe:Zip.Native.BitWriter.data",
"probe:Zip.Native.BitWriter.empty",
"probe:Zip.Native.BitWriter.empty_toBits",
"probe:Zip.Native.BitWriter.empty_wf",
"probe:Zip.Native.BitWriter.flush",
"probe:Zip.Native.BitWriter.flush_toBits",
"probe:Zip.Native.BitWriter.toBits",
"probe:Zip.Native.BitWriter.wf",
"probe:Zip.Native.BitWriter.writeBits",
"probe:Zip.Native.BitWriter.writeBits.go",
"probe:Zip.Native.BitWriter.writeBits_toBits",
"probe:Zip.Native.BitWriter.writeBits_wf",
"probe:Zip.Native.BitWriter.writeHuffCode",
"probe:Zip.Native.BitWriter.writeHuffCode.go",
"probe:Zip.Native.BitWriter.writeHuffCode_toBits",
"probe:Zip.Native.BitWriter.writeHuffCode_wf",
"probe:Zip.Native.CompressFormat",
"probe:Zip.Native.Deflate.LZ77Token",
"probe:Zip.Native.Deflate.LZ77Token.toLZ77Symbol",
"probe:Zip.Native.Deflate.ValidDecomp",
"probe:Zip.Native.Deflate.array_get!Internal_eq",
"probe:Zip.Native.Deflate.canonicalCodes",
"probe:Zip.Native.Deflate.canonicalCodes.go",
"probe:Zip.Native.Deflate.canonicalCodes_size",
"probe:Zip.Native.Deflate.canonicalCodes_snd_le",
"probe:Zip.Native.Deflate.canonicalCodes_snd_le'",
"probe:Zip.Native.Deflate.deflateDynamic",
"probe:Zip.Native.Deflate.deflateDynamic_spec",
"probe:Zip.Native.Deflate.deflateFixed",
"probe:Zip.Native.Deflate.deflateFixedBlock",
"probe:Zip.Native.Deflate.deflateFixedBlock_spec",
"probe:Zip.Native.Deflate.deflateFixedIter",
"probe:Zip.Native.Deflate.deflateFixed_spec",
"probe:Zip.Native.Deflate.deflateLazy",
"probe:Zip.Native.Deflate.deflateLazyIter",
"probe:Zip.Native.Deflate.deflateLazyIter_eq_deflateLazy",
"probe:Zip.Native.Deflate.deflateLazy_spec",
"probe:Zip.Native.Deflate.deflateRaw",
"probe:Zip.Native.Deflate.deflateRaw_goR_pad",
"probe:Zip.Native.Deflate.deflateRaw_pad",
"probe:Zip.Native.Deflate.deflateStored",
"probe:Zip.Native.Deflate.distExtra_le_13",
"probe:Zip.Native.Deflate.emitTokens",
"probe:Zip.Native.Deflate.emitTokensWithCodes",
"probe:Zip.Native.Deflate.emitTokensWithCodes_spec",
"probe:Zip.Native.Deflate.emitTokensWithCodes_wf",
"probe:Zip.Native.Deflate.emitTokens_spec",
"probe:Zip.Native.Deflate.emitTokens_wf",
"probe:Zip.Native.Deflate.encodeSymbol_canonicalCodes_eq",
"probe:Zip.Native.Deflate.encodeSymbol_distTable_eq",
"probe:Zip.Native.Deflate.encodeSymbol_litTable_eq",
"probe:Zip.Native.Deflate.encodeSymbols_append",
"probe:Zip.Native.Deflate.encodeSymbols_append_inv",
"probe:Zip.Native.Deflate.encodeSymbols_cons_some",
"probe:Zip.Native.Deflate.encodeSymbols_tokensToSymbols_isSome",
"probe:Zip.Native.Deflate.encodeSymbols_tokensToSymbols_lazy_isSome",
"probe:Zip.Native.Deflate.findDistCode",
"probe:Zip.Native.Deflate.findDistCode_agree",
"probe:Zip.Native.Deflate.findLengthCode",
"probe:Zip.Native.Deflate.findLengthCode_agree",
"probe:Zip.Native.Deflate.findTableCode",
"probe:Zip.Native.Deflate.findTableCode.go",
"probe:Zip.Native.Deflate.findTableCode_go_extraN",
"probe:Zip.Native.Deflate.findTableCode_go_idx_bound",
"probe:Zip.Native.Deflate.fixedDistCodes",
"probe:Zip.Native.Deflate.fixedDistCodes_size",
"probe:Zip.Native.Deflate.fixedLitCodes",
"probe:Zip.Native.Deflate.fixedLitCodes_size",
"probe:Zip.Native.Deflate.freqPairs_witness",
"probe:Zip.Native.Deflate.inflate_complete",
"probe:Zip.Native.Deflate.inflate_deflateDynamic",
"probe:Zip.Native.Deflate.inflate_deflateFixed",
"probe:Zip.Native.Deflate.inflate_deflateFixedIter",
"probe:Zip.Native.Deflate.inflate_deflateLazy",
"probe:Zip.Native.Deflate.inflate_deflateLazyIter",
"probe:Zip.Native.Deflate.inflate_deflateRaw",
"probe:Zip.Native.Deflate.instBEqLZ77Token",
"probe:Zip.Native.Deflate.instBEqLZ77Token.beq",
"probe:Zip.Native.Deflate.instInhabitedLZ77Token",
"probe:Zip.Native.Deflate.instInhabitedLZ77Token.default",
"probe:Zip.Native.Deflate.lengthExtra_le_5",
"probe:Zip.Native.Deflate.lz77Greedy",
"probe:Zip.Native.Deflate.lz77Greedy.countMatch",
"probe:Zip.Native.Deflate.lz77Greedy.countMatch_matches",
"probe:Zip.Native.Deflate.lz77Greedy.go",
"probe:Zip.Native.Deflate.lz77Greedy.go_matches",
"probe:Zip.Native.Deflate.lz77Greedy.hash3",
"probe:Zip.Native.Deflate.lz77Greedy.mainLoop",
"probe:Zip.Native.Deflate.lz77Greedy.trailing",
"probe:Zip.Native.Deflate.lz77Greedy.updateHashes",
"probe:Zip.Native.Deflate.lz77GreedyIter",
"probe:Zip.Native.Deflate.lz77GreedyIter.countMatch",
"probe:Zip.Native.Deflate.lz77GreedyIter.go",
"probe:Zip.Native.Deflate.lz77GreedyIter.hash3",
"probe:Zip.Native.Deflate.lz77GreedyIter.mainLoop",
"probe:Zip.Native.Deflate.lz77GreedyIter.trailing",
"probe:Zip.Native.Deflate.lz77GreedyIter.updateHashes",
"probe:Zip.Native.Deflate.lz77GreedyIter_eq_lz77Greedy",
"probe:Zip.Native.Deflate.lz77Greedy_encodable",
"probe:Zip.Native.Deflate.lz77Greedy_resolves",
"probe:Zip.Native.Deflate.lz77Greedy_size_le",
"probe:Zip.Native.Deflate.lz77Greedy_spec_decode",
"probe:Zip.Native.Deflate.lz77Greedy_valid",
"probe:Zip.Native.Deflate.lz77Lazy",
"probe:Zip.Native.Deflate.lz77Lazy.countMatch",
"probe:Zip.Native.Deflate.lz77Lazy.countMatch_matches",
"probe:Zip.Native.Deflate.lz77Lazy.go",
"probe:Zip.Native.Deflate.lz77Lazy.go_matches",
"probe:Zip.Native.Deflate.lz77Lazy.hash3",
"probe:Zip.Native.Deflate.lz77Lazy.mainLoop",
"probe:Zip.Native.Deflate.lz77Lazy.mainLoop_encodable",
"probe:Zip.Native.Deflate.lz77Lazy.mainLoop_length",
"probe:Zip.Native.Deflate.lz77Lazy.mainLoop_valid",
"probe:Zip.Native.Deflate.lz77Lazy.trailing",
"probe:Zip.Native.Deflate.lz77Lazy.trailing_encodable",
"probe:Zip.Native.Deflate.lz77Lazy.trailing_length",
"probe:Zip.Native.Deflate.lz77Lazy.trailing_valid",
"probe:Zip.Native.Deflate.lz77Lazy.updateHashes",
"probe:Zip.Native.Deflate.lz77LazyIter",
"probe:Zip.Native.Deflate.lz77LazyIter.mainLoop",
"probe:Zip.Native.Deflate.lz77LazyIter.trailing",
"probe:Zip.Native.Deflate.lz77LazyIter_eq_lz77Lazy",
"probe:Zip.Native.Deflate.lz77Lazy_encodable",
"probe:Zip.Native.Deflate.lz77Lazy_resolves",
"probe:Zip.Native.Deflate.lz77Lazy_size_le",
"probe:Zip.Native.Deflate.lz77Lazy_spec_decode",
"probe:Zip.Native.Deflate.lz77Lazy_valid",
"probe:Zip.Native.Deflate.mainLoop_encodable",
"probe:Zip.Native.Deflate.mainLoop_length",
"probe:Zip.Native.Deflate.mainLoop_valid",
"probe:Zip.Native.Deflate.nativeFindDistCode_extraN_bound",
"probe:Zip.Native.Deflate.nativeFindDistCode_idx_bound",
"probe:Zip.Native.Deflate.nativeFindLengthCode_extraN_bound",
"probe:Zip.Native.Deflate.nativeFindLengthCode_idx_bound",
"probe:Zip.Native.Deflate.toUInt8Array_le",
"probe:Zip.Native.Deflate.tokenFreqs",
"probe:Zip.Native.Deflate.tokenFreqs.go",
"probe:Zip.Native.Deflate.tokenFreqs_distCode_pos",
"probe:Zip.Native.Deflate.tokenFreqs_eob_pos",
"probe:Zip.Native.Deflate.tokenFreqs_go_distCode_pos",
"probe:Zip.Native.Deflate.tokenFreqs_go_lengthCode_pos",
"probe:Zip.Native.Deflate.tokenFreqs_go_literal_pos",
"probe:Zip.Native.Deflate.tokenFreqs_go_mono",
"probe:Zip.Native.Deflate.tokenFreqs_go_sizes",
"probe:Zip.Native.Deflate.tokenFreqs_lengthCode_pos",
"probe:Zip.Native.Deflate.tokenFreqs_literal_pos",
"probe:Zip.Native.Deflate.tokenFreqs_sizes",
"probe:Zip.Native.Deflate.tokensToSymbols",
"probe:Zip.Native.Deflate.tokensToSymbols_encodable",
"probe:Zip.Native.Deflate.tokensToSymbols_lazy_encodable",
"probe:Zip.Native.Deflate.tokensToSymbols_length",
"probe:Zip.Native.Deflate.tokensToSymbols_validSymbolList",
"probe:Zip.Native.Deflate.trailing_encodable",
"probe:Zip.Native.Deflate.trailing_length",
"probe:Zip.Native.Deflate.trailing_valid",
"probe:Zip.Native.Deflate.validDecomp_resolves",
"probe:Zip.Native.Deflate.validDecomp_resolves_aux",
"probe:Zip.Native.Deflate.writeDynamicHeader",
"probe:Zip.Native.Deflate.writeDynamicHeader.writeCLEntries",
"probe:Zip.Native.Deflate.writeDynamicHeader.writeCLLengths",
"probe:Zip.Native.Deflate.writeDynamicHeader_spec",
"probe:Zip.Native.Deflate.writeDynamicHeader_wf",
"probe:Zip.Native.GzipDecode.decompress",
"probe:Zip.Native.GzipDecode.decompressSingle",
"probe:Zip.Native.GzipEncode.compress",
"probe:Zip.Native.GzipEncode.compress_crc32",
"probe:Zip.Native.GzipEncode.compress_eq",
"probe:Zip.Native.GzipEncode.compress_header_bytes",
"probe:Zip.Native.GzipEncode.compress_isize",
"probe:Zip.Native.GzipEncode.compress_size",
"probe:Zip.Native.HuffTree",
"probe:Zip.Native.HuffTree.decode",
"probe:Zip.Native.HuffTree.decode.go",
"probe:Zip.Native.HuffTree.fromLengths",
"probe:Zip.Native.HuffTree.fromLengthsTree",
"probe:Zip.Native.HuffTree.insert",
"probe:Zip.Native.HuffTree.insert.go",
"probe:Zip.Native.HuffTree.insertLoop",
"probe:Zip.Native.Inflate.codeLengthOrder",
"probe:Zip.Native.Inflate.codeLengthOrder_size",
"probe:Zip.Native.Inflate.copyLoop",
"probe:Zip.Native.Inflate.decodeCLSymbols",
"probe:Zip.Native.Inflate.decodeDynamicTrees",
"probe:Zip.Native.Inflate.decodeHuffman",
"probe:Zip.Native.Inflate.decodeHuffman.go",
"probe:Zip.Native.Inflate.decodeStored",
"probe:Zip.Native.Inflate.distBase",
"probe:Zip.Native.Inflate.distBase_size",
"probe:Zip.Native.Inflate.distExtra",
"probe:Zip.Native.Inflate.distExtra_size",
"probe:Zip.Native.Inflate.fillEntries",
"probe:Zip.Native.Inflate.fixedDistLengths",
"probe:Zip.Native.Inflate.fixedLitLengths",
"probe:Zip.Native.Inflate.inflate",
"probe:Zip.Native.Inflate.inflateLoop",
"probe:Zip.Native.Inflate.inflateRaw",
"probe:Zip.Native.Inflate.lengthBase",
"probe:Zip.Native.Inflate.lengthBase_size",
"probe:Zip.Native.Inflate.lengthExtra",
"probe:Zip.Native.Inflate.lengthExtra_size",
"probe:Zip.Native.Inflate.readCLCodeLengths",
"probe:Zip.Native.ZlibDecode.decompress",
"probe:Zip.Native.ZlibDecode.decompressSingle",
"probe:Zip.Native.ZlibEncode.compress",
"probe:Zip.Native.ZlibEncode.compress_adler32",
"probe:Zip.Native.ZlibEncode.compress_cinfo",
"probe:Zip.Native.ZlibEncode.compress_cm",
"probe:Zip.Native.ZlibEncode.compress_cmf",
"probe:Zip.Native.ZlibEncode.compress_eq",
"probe:Zip.Native.ZlibEncode.compress_header_check",
"probe:Zip.Native.ZlibEncode.compress_no_fdict",
"probe:Zip.Native.ZlibEncode.compress_size",
"probe:Zip.Native.bytesToBits_append",
"probe:Zip.Native.bytesToBits_drop_prefix_three",
"probe:Zip.Native.compressAuto",
"probe:Zip.Native.decodeCLSymbols_inv",
"probe:Zip.Native.decodeDynamicTrees_inv",
"probe:Zip.Native.decodeHuffman_go_inv",
"probe:Zip.Native.decodeHuffman_inv",
"probe:Zip.Native.decodeStored_inv",
"probe:Zip.Native.decode_inv",
"probe:Zip.Native.decompressAuto",
"probe:Zip.Native.detectFormat",
"probe:Zip.Native.gzip_decompressSingle_compress",
"probe:Zip.Native.inflateLoop_complete_ext",
"probe:Zip.Native.inflateLoop_endPos_le",
"probe:Zip.Native.inflateRaw_append_suffix",
"probe:Zip.Native.inflateRaw_complete",
"probe:Zip.Native.inflateRaw_endPos_eq",
"probe:Zip.Native.inflateRaw_endPos_ge",
"probe:Zip.Native.inflateRaw_endPos_le",
"probe:Zip.Native.inflate_to_spec_decode",
"probe:Zip.Native.readCLCodeLengths_inv",
"probe:Zip.Native.zlib_decompressSingle_compress",
"probe:Zip.Spec.DeflateStoredCorrect.decodeStored_align",
"probe:Zip.Spec.DeflateStoredCorrect.decodeStored_on_block",
"probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure",
"probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure_size",
"probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure_size_bound",
"probe:Zip.Spec.DeflateStoredCorrect.fromLengths_fixedDist_ok",
"probe:Zip.Spec.DeflateStoredCorrect.fromLengths_fixedLit_ok",
"probe:Zip.Spec.DeflateStoredCorrect.inflateLoop_final_stored",
"probe:Zip.Spec.DeflateStoredCorrect.inflateLoop_nonfinal_stored",
"probe:Zip.Spec.DeflateStoredCorrect.inflate_deflateStoredPure",
"probe:Zip.Spec.DeflateStoredCorrect.readBits_1_at_0",
"probe:Zip.Spec.DeflateStoredCorrect.readBits_2_at_1",
"probe:Zip.Spec.DeflateStoredCorrect.readBytes_at_aligned",
"probe:Zip.Spec.DeflateStoredCorrect.readUInt16LE_align",
"probe:Zip.Spec.DeflateStoredCorrect.readUInt16LE_at_aligned",
"probe:Zip.Spec.DeflateStoredCorrect.storedBlockHdr",
"probe:Zip.Spec.DeflateStoredCorrect.storedBlockHdr_size",
"probe:Zip.Spec.DeflateStoredCorrect.uint16_le_roundtrip",
"probe:Zip.Spec.DeflateStoredCorrect.uint16_xor_complement",
"probe:ZipCommon.BitReader.toBits",
"probe:ZipTest.Archive.tests",
"probe:ZipTest.Benchmark.tests",
"probe:ZipTest.Binary.tests",
"probe:ZipTest.Checksum.tests",
"probe:ZipTest.CompressFixtures.tests",
"probe:ZipTest.Gzip.tests",
"probe:ZipTest.NativeChecksum.tests",
"probe:ZipTest.NativeCompressBench.tests",
"probe:ZipTest.NativeDeflate.tests",
"probe:ZipTest.NativeGzip.tests",
"probe:ZipTest.NativeInflate.tests",
"probe:ZipTest.NativeIntegration.tests",
"probe:ZipTest.NativeScale.Pattern",
"probe:ZipTest.NativeScale.Pattern.generate",
"probe:ZipTest.NativeScale.Pattern.name",
"probe:ZipTest.NativeScale.TimingEntry",
"probe:ZipTest.NativeScale.TimingEntry.ns",
"probe:ZipTest.NativeScale.TimingEntry.op",
"probe:ZipTest.NativeScale.TimingEntry.pat",
"probe:ZipTest.NativeScale.TimingEntry.size",
"probe:ZipTest.NativeScale.levels",
"probe:ZipTest.NativeScale.matrixSizes",
"probe:ZipTest.NativeScale.patterns",
"probe:ZipTest.NativeScale.sweepSizes",
"probe:ZipTest.NativeScale.tests",
"probe:ZipTest.RawDeflate.tests",
"probe:ZipTest.Tar.tests",
"probe:ZipTest.TarFixtures.tests",
"probe:ZipTest.Utf8Fixtures.tests",
"probe:ZipTest.ZipFixtures.tests",
"probe:ZipTest.Zlib.tests",
"probe:Zlib.compress",
"probe:Zlib.decompress",
"probe:assertThrows",
"probe:byteArrayReadStream",
"probe:calibrateIters",
"probe:fmtMBps",
"probe:fmtMs",
"probe:fmtRatio",
"probe:forceEval",
"probe:fragmentingStream",
"probe:main",
"probe:mkConstantData",
"probe:mkCyclicData",
"probe:mkLargeData",
"probe:mkPrngData",
"probe:mkRandomData",
"probe:mkTestData",
"probe:mkTextData",
"probe:pad",
"probe:readFixture",
"probe:sizeName",
"probe:timeIO",
"probe:writeFixtureTmp"
],
"verified_functions_count": 773
}
We have designed our VeriLib verification certificates to meet three goals:
Here is how this works in detail. The green checkmark displayed (at the top of certificate pages such as this one) is not static, but dynamically generated if and only if three hashes stored on the Ethereum blockchain satisfy these properties:
a) The GitHub repo hash matches that of the linked repo (certifying that we’re verifying the right code)
b) The DockerHub container hash matches that of the linked container (certifying that we’re using the right verification tooling)
c) The manifest hash matches that of the displayed manifest (certifying that we’re showing the right verification result)
d) That the manifest shows VerificationSuccess = true
| Blockchain commit time | — (on-chain timestamp: Ethereum proof) |
|---|---|
| GitHub / repo hash | 78e5bd6950afdda3ab88dbd567e54bc6adedf3ae (browse tree) |
| DockerHub / container hash |
sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed
|
| Manifest hash | 0464c6bbd288ab6fbff75d240095cb3b340bb79d661ca67ac40d7d0a1eae8bcd (SHA-256 of published JSON file) |
Running the Verify it yourself script (instructions below) checks that applying the verification tooling (b) to the code (a) reproduces the manifest (c).
To save you time, VeriLib has already auto-run this same script, which produces both pedagogical output to the terminal and the result summary file manifest.json.
We encourage you to not only run this tooling, but also inspect it for correctness. You can build trust in this certificate page by checking the text in green against the manifest, and by noting that the manifest lists as successfully verified all functions in the Specifications section.
You do not need to clone any repository. Download the small bash script below using wget or curl. Running it pulls the prebuilt image from Docker Hub and writes the same manifests and lists this page publishes. A full run can take a long time and use significant disk space—plan for that before you start.
wget (saves as verify.sh in the current directory):
wget -O verify.sh https://verilib.org/cert/5165/verify-script
Same URL with curl: curl -fsSL -o verify.sh https://verilib.org/cert/5165/verify-script
bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/probe-lean-repo-5165@sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed' 'VERIFICATION_RESULTS'
Once you have finished running the script, the file VERIFICATION_RESULTS/manifest.json should match what is shown in the Results section above (downloadable here).
You need a working Docker install before you can pull the certificate image or run the verification script. For the canonical, up-to-date steps (including licensing and system requirements), use Docker’s official guide: Get Docker.
apt package without checking Docker’s repo instructions.
Detailed steps:
Install Docker Engine
(choose your distro: Ubuntu, Debian, Fedora, etc.).
Smoke test: In a terminal, run docker version. You should see both Client and Server sections. If you see docker: command not found, the CLI is not on your PATH yet—restart the terminal or finish Docker Desktop’s setup.
Latest certificate: v1
— /cert/5165 and /cert/5165?p=1&c=v1 pin the image below.
The Docker image verilib/probe-lean-repo-5165@sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed on Docker Hub matches this certificate’s published dockerHubImageDigest / manifest image.
Use Verify it yourself to pull and run—no clone required.