Revision - cef6a8e - Merge pull request #298 from project-everest/vdum_ocaml_nits

Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC

Merge pull request #298 from project-everest/vdum_ocaml_nits

OCaml API: Don't run unit tests which require unsupported features

2 parent s 760addb + 28f416c

Files
Changes

Permalinks

MerkleTree.Low.Serialization.fst.hints

[
  "\b�~4��\\��p�|F��_",
  [
    [
      "MerkleTree.Low.Serialization.serialize_bool",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint8_t",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gte", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_LowStar.Buffer.trivial_preorder",
        "int_inversion",
        "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_8f35a30b5723496a838bcc2be6799465",
        "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "true_interp", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "122481c14e74976f604153864c47ed45"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_uint8_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint8_t",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gte", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_LowStar.Buffer.trivial_preorder",
        "int_inversion",
        "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4",
        "refinement_interpretation_Tm_refine_e633d96da2f5ad1e125b09ef53e4c4f2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "true_interp", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "82267d80b4e126b21c32427241416304"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_uint16_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "65f19ab435021c786223af00961470ec"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_uint32_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "9dd00626eac661df6b8ae7ecd7d30493"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_uint64_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "974d50e9fce139483d09dcd580410655"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash_i",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc",
        "refinement_interpretation_Tm_refine_cf65d243580d5162516eff3756abceb2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "c0087f12c0a92feec646f0dfe694ea38"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t", "int_inversion",
        "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "377414d7bd858350a01245135c75471b"
    ],
    [
      "MerkleTree.Low.Serialization.u64_add_fits",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt64.gte",
        "equation_MerkleTree.Low.Serialization.uint64_t",
        "equation_MerkleTree.Low.uint64_max", "equation_Prims.nat",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt64.vu_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4db8ba22c4504a66577a2159dcc603cd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
        "typing_FStar.UInt64.sub", "typing_FStar.UInt64.v",
        "typing_MerkleTree.Low.uint64_max"
      ],
      0,
      "6c77b76783683cfbd024c9f516778e40"
    ],
    [
      "MerkleTree.Low.Serialization.hash_vec_bytes",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.Int.Cast.uint32_to_uint64",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Serialization.uint64_t",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt64.vu_inv",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c",
        "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.uint_to_t",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Serialization.u64_add_fits"
      ],
      0,
      "4523db176f4eb8818190d77f4cf903d9"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash_vec_i",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Signed",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.elems_inv",
        "equation_LowStar.RVector.rs_elems_inv",
        "equation_LowStar.RVector.rv_elems_inv",
        "equation_LowStar.RVector.rv_inv",
        "equation_LowStar.RVector.rv_itself_inv",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq",
        "equation_LowStar.Vector.forall_seq",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_r_inv",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hreg",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "lemma_LowStar.RVector.rv_inv_preserved",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_LowStar.Regional.Rgl_r_inv",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_r_inv",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_3e7d6d9effbbeae5539c0cb324d2cadb",
        "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12",
        "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b",
        "refinement_interpretation_Tm_refine_ac09e169622915d2fb30eeed97b3a2b2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "token_correspondence_LowStar.Regional.rg_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hreg"
      ],
      0,
      "550d67cc81c0107d0fbb3f7a93670189"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash_vec",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.lt", "equation_FStar.UInt32.gt",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.loc_rvector",
        "equation_LowStar.RVector.rv_inv",
        "equation_LowStar.RVector.rv_itself_inv",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "equation_MerkleTree.Low.Datastructures.hreg",
        "equation_MerkleTree.Low.Datastructures.hvreg",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "lemma_FStar.Ghost.reveal_hide",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.freeable_length",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Negation",
        "proj_equation_LowStar.Regional.Rgl_region_of",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_region_of",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_ac09e169622915d2fb30eeed97b3a2b2",
        "refinement_interpretation_Tm_refine_d96c0978ac30e5f0fd109eead55c3101",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "typing_FStar.Monotonic.HyperHeap.includes",
        "typing_FStar.Monotonic.HyperHeap.mod_set",
        "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty",
        "typing_FStar.Set.intersect", "typing_FStar.Set.singleton",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_regions",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.RVector.loc_rvector",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "typing_MerkleTree.Low.Datastructures.hreg"
      ],
      0,
      "a3804a63e63570e0ca4677a40346c0c3"
    ],
    [
      "MerkleTree.Low.Serialization.hash_vv_bytes_i",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W64",
        "equality_tok_FStar.Integers.W64@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte",
        "equation_FStar.UInt32.lt", "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vv",
        "equation_MerkleTree.Low.Serialization.hash_vec_bytes",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint64_t",
        "equation_Prims.nat",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
        "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_LowStar.Vector.Vec_sz",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe",
        "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c",
        "refinement_interpretation_Tm_refine_dd6b31fbf6cc990de2d6442415284c3b",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_LowStar.Vector.__proj__Vec__item__sz",
        "typing_LowStar.Vector.as_seq",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.Serialization.hash_vec_bytes",
        "typing_MerkleTree.Low.Serialization.u64_add_fits"
      ],
      0,
      "41f2e7ff33ca6dd6d49b8bd6fc2827af"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash_vv_i",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada",
        "MerkleTree.Low.Datastructures_interpretation_Tm_ghost_arrow_c55a67b27f4ea444400878ed4572b7c7",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Signed",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.elems_inv",
        "equation_LowStar.RVector.elems_reg",
        "equation_LowStar.RVector.loc_rvector",
        "equation_LowStar.RVector.rs_elems_inv",
        "equation_LowStar.RVector.rs_elems_reg",
        "equation_LowStar.RVector.rv_elems_inv",
        "equation_LowStar.RVector.rv_elems_reg",
        "equation_LowStar.RVector.rv_inv",
        "equation_LowStar.RVector.rv_itself_inv",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Regional.Instances.vector_region_of",
        "equation_LowStar.Regional.Instances.vector_regional",
        "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq",
        "equation_LowStar.Vector.forall_seq",
        "equation_LowStar.Vector.freeable",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv",
        "equation_MerkleTree.Low.Datastructures.hash_vv",
        "equation_MerkleTree.Low.Datastructures.hvreg",
        "equation_MerkleTree.Low.Datastructures.hvvreg",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_LowStar.Regional.Instances.vector_region_of",
        "function_token_typing_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "int_inversion",
        "interpretation_Tm_abs_8af5505247aa684e407d3b8992667aef",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperHeap.lemma_disjoint_includes",
        "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.freeable_length",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
        "proj_equation_LowStar.Regional.Rgl_r_inv",
        "proj_equation_LowStar.Regional.Rgl_region_of",
        "proj_equation_LowStar.Vector.Vec_vs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_r_inv",
        "projection_inverse_LowStar.Regional.Rgl_region_of",
        "refinement_interpretation_Tm_refine_26862678c89ff3fc205c8b94520ae4f0",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12",
        "refinement_interpretation_Tm_refine_446bf10afa9e2c979cbc68d89c3e36ad",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "token_correspondence_LowStar.Regional.Instances.vector_region_of",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of",
        "token_correspondence_LowStar.Regional.rg_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv",
        "typing_FStar.Monotonic.HyperHeap.includes",
        "typing_FStar.Monotonic.HyperHeap.mod_set",
        "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty",
        "typing_FStar.Set.intersect", "typing_FStar.Set.singleton",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_regions",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.RVector.loc_rvector",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.Datastructures.hvreg"
      ],
      0,
      "1f31838308b9ed31defa8ab98c672199"
    ],
    [
      "MerkleTree.Low.Serialization.serialize_hash_vv",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.lt", "equation_FStar.UInt32.gt",
        "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.loc_rvector",
        "equation_LowStar.RVector.rv_inv",
        "equation_LowStar.RVector.rv_itself_inv",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Regional.Instances.vector_dummy",
        "equation_LowStar.Regional.Instances.vector_region_of",
        "equation_LowStar.Regional.Instances.vector_regional",
        "equation_LowStar.Vector.freeable",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vv",
        "equation_MerkleTree.Low.Datastructures.hvreg",
        "equation_MerkleTree.Low.Datastructures.hvvreg",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_LowStar.Regional.Instances.vector_region_of",
        "kinding_LowStar.Regional.regional@tok",
        "lemma_FStar.Ghost.reveal_hide",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.freeable_length",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Negation",
        "proj_equation_LowStar.Regional.Rgl_region_of",
        "proj_equation_LowStar.Vector.Vec_vs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_region_of",
        "refinement_interpretation_Tm_refine_26862678c89ff3fc205c8b94520ae4f0",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "token_correspondence_LowStar.Regional.Instances.vector_region_of",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of",
        "typing_FStar.Ghost.hide",
        "typing_FStar.Monotonic.HyperHeap.includes",
        "typing_FStar.Monotonic.HyperHeap.mod_set",
        "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty",
        "typing_FStar.Set.intersect", "typing_FStar.Set.singleton",
        "typing_FStar.UInt32.lt", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_regions",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.RVector.loc_rvector",
        "typing_LowStar.Regional.Instances.vector_dummy",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.Datastructures.hvreg"
      ],
      0,
      "059604a4cdb68ee9797d697452c5188e"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_bool",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "95557803d47a3f8aadde2eacad44b685"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_bool",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gte",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v"
      ],
      0,
      "01d23dd60bbf52547dfd99d64502d2a5"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint8_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "95d498be3997186fcff9440c1bfc9627"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint8_t",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gte",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v"
      ],
      0,
      "9672329ed270cc1c2ca3a3978150f459"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint16_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "94b8d6599029340e5e6f14b30845abdf"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint16_t",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Int.Cast.uint8_to_uint16",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_left_value_lemma",
        "lemma_Lib.IntTypes.pow2_4",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_541d06ed6731928026bc39b1981eb00a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Int.Cast.uint8_to_uint16", "typing_FStar.UInt.fits",
        "typing_FStar.UInt16.v", "typing_FStar.UInt32.v",
        "typing_FStar.UInt8.v", "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre"
      ],
      0,
      "5d70df3a01c6bc6313eb6e8d5eef5ff4"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint32_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "98c8046aa28355a42556c017537c88ff"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint32_t",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Int.Cast.uint16_to_uint32",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint16_t",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_left_value_lemma",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_88c857def71d9b11ced5e5e041edc24e",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Int.Cast.uint16_to_uint32", "typing_FStar.UInt.fits",
        "typing_FStar.UInt16.v", "typing_FStar.UInt32.v",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre"
      ],
      0,
      "4f4d704219a8dbb75aff105906d64770"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint64_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "d684f1a09313ef8763c77afb31605d00"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint64_t",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W64",
        "equality_tok_FStar.Integers.W64@tok",
        "equation_FStar.BitVector.bv_t", "equation_FStar.BitVector.zero_vec",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Int.Cast.uint32_to_uint64",
        "equation_FStar.Integers.int_t",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat",
        "equation_Prims.pos", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_left_value_lemma",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.BitVector.zero_vec",
        "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v"
      ],
      0,
      "9788f3408cd56879e43c2a408237d5bf"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "137d04331706b8a9af988ff6e40c8692"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.subset", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.gt", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt",
        "equation_FStar.UInt32.gte", "equation_FStar.UInt32.lt",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_LowStar.Monotonic.Buffer.disjoint",
        "equation_LowStar.Monotonic.Buffer.fresh_loc",
        "equation_LowStar.Regional.rg_dummy",
        "equation_LowStar.Regional.rg_inv",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_r_inv",
        "equation_MerkleTree.Low.Datastructures.hash_r_repr",
        "equation_MerkleTree.Low.Datastructures.hash_repr",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hreg",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.New.High.hash", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_LowStar.Regional.__proj__Rgl__item__r_inv",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
        "lemma_LowStar.Monotonic.Buffer.loc_buffer_null",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs",
        "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.Regional.Rgl_dummy",
        "proj_equation_LowStar.Regional.Rgl_loc_of",
        "proj_equation_LowStar.Regional.Rgl_r_inv",
        "proj_equation_LowStar.Regional.Rgl_r_repr",
        "proj_equation_LowStar.Regional.Rgl_repr",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_LowStar.Regional.Rgl_dummy",
        "projection_inverse_LowStar.Regional.Rgl_loc_of",
        "projection_inverse_LowStar.Regional.Rgl_r_inv",
        "projection_inverse_LowStar.Regional.Rgl_r_repr",
        "projection_inverse_LowStar.Regional.Rgl_repr",
        "refinement_interpretation_Tm_refine_0585ee3c240775258e9efb20961f9395",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_aa4b3d268075d84252df525db1f85524",
        "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_bcef36c9fe2b6458c3fdda81179b025f",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "token_correspondence_LowStar.Monotonic.Buffer.loc_buffer",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__loc_of",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_repr",
        "token_correspondence_LowStar.Regional.rg_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_r_repr",
        "typing_FStar.Ghost.reveal",
        "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.Set.singleton", "typing_FStar.UInt32.sub",
        "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.cast",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.as_addr",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.loc_addresses",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Regional.__proj__Rgl__item__irepr",
        "typing_LowStar.Regional.__proj__Rgl__item__repr",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hreg"
      ],
      0,
      "932fdea777e5632bd94e94371f19288e"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec_i",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b0df249b3f5894f8a7622074272b626d"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec_i",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_LowStar.Vector.loc_vector_within.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "b2t_def", "bool_inversion",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
        "equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt",
        "equation_FStar.UInt32.lte", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.live",
        "equation_LowStar.Vector.loc_vector",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Negation", "proj_equation_LowStar.Vector.Vec_vs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3e7d6d9effbbeae5539c0cb324d2cadb",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_7028972db935cf1f2ecc12fc7857552a",
        "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_a43b4918a11b234508ae97d267788230",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_c11ee48277084f734442582a62372ec4",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.UInt32.add", "typing_FStar.UInt32.lte",
        "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_LowStar.Vector.loc_vector",
        "typing_LowStar.Vector.loc_vector_within",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash"
      ],
      0,
      "da8d6f01b04cc21cd12ad6231be18554"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "3407cb0f22f2040a9f8f61ee873cf29e"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.Vector.loc_vector",
        "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_a43b4918a11b234508ae97d267788230",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.UInt32.gt", "typing_FStar.UInt32.lt",
        "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.loc_vector",
        "typing_MerkleTree.Low.Datastructures.hash"
      ],
      0,
      "cc644ac2507c0655445762f06f0bb552"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv_i",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "2a0470e12ef657d77001c97410f7e619"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv_i",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_LowStar.Vector.loc_vector_within.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "b2t_def", "bool_inversion",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.lte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gte", "equation_FStar.UInt32.lt",
        "equation_FStar.UInt32.lte", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.as_seq",
        "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_repr",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vec_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_vec_repr",
        "equation_MerkleTree.Low.Datastructures.hash_vv",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.Ghost.reveal_hide",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.Vector.Vec_vs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3396f1d518ffeb2163c25c13fcb1de13",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_446bf10afa9e2c979cbc68d89c3e36ad",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_7028972db935cf1f2ecc12fc7857552a",
        "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd",
        "refinement_interpretation_Tm_refine_80922429ffacb2b807b93c3173eb2f07",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_d1ad46dabfb91f0d027c88b59cc5fd9b",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "typing_FStar.Ghost.hide", "typing_FStar.Map.domain",
        "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt32.add", "typing_FStar.UInt32.lt",
        "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.__proj__Vec__item__cap",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.as_seq",
        "typing_LowStar.Vector.loc_vector",
        "typing_LowStar.Vector.loc_vector_within",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hash_repr",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.Datastructures.hash_vec_dummy"
      ],
      0,
      "b21f65b42dd2e6ddef25ff2f817f6e92"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "3781f95bd99499b40b84457882c5f854"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.loc_buffer",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.fresh_loc",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.loc_vector",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vec_dummy",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "fuel_guarded_inversion_LowStar.Vector.vector_str",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.Ghost.reveal_hide",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs",
        "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_80922429ffacb2b807b93c3173eb2f07",
        "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "typing_FStar.Ghost.hide", "typing_FStar.Map.domain",
        "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.Set.singleton", "typing_FStar.UInt32.gt",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.loc_buffer",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.as_addr",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_addresses",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.alloc_empty",
        "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.Datastructures.hash_vec_dummy"
      ],
      0,
      "c0474133f5154125ccb89788585987d4"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize_size",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_MerkleTree.Low.const_mt_p",
        "equation_MerkleTree.Low.const_pointer",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3"
      ],
      0,
      "cf0c417a42dac0ce898b72ef3cc06f64"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize_size",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W64",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_FStar.Integers.W64@tok",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.Int.Cast.uint32_to_uint64",
        "equation_FStar.Integers.int_t",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gte",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.gte",
        "equation_FStar.UInt64.lt", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_LowStar.Monotonic.Buffer.get",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rv_inv",
        "equation_LowStar.RVector.rv_itself_inv",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_r_inv",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hreg",
        "equation_MerkleTree.Low.Datastructures.hvreg",
        "equation_MerkleTree.Low.Serialization.hash_vec_bytes",
        "equation_MerkleTree.Low.Serialization.u64_add_fits",
        "equation_MerkleTree.Low.Serialization.uint64_t",
        "equation_MerkleTree.Low.const_mt_p",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.Low.merkle_tree_size_lg",
        "equation_MerkleTree.Low.mt_safe",
        "equation_MerkleTree.Low.uint32_max",
        "equation_MerkleTree.Low.uint64_max", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "lemma_FStar.UInt64.vu_inv",
        "lemma_LowStar.Monotonic.Buffer.freeable_length",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.Regional.Rgl_r_inv",
        "proj_equation_MerkleTree.Low.MT_hash_size",
        "proj_equation_MerkleTree.Low.MT_hs",
        "proj_equation_MerkleTree.Low.MT_mroot",
        "proj_equation_MerkleTree.Low.MT_rhs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_r_inv",
        "refinement_interpretation_Tm_refine_02a311be716ab03201b91cc11abde92c",
        "refinement_interpretation_Tm_refine_2ac8bed7a6398f84bccb91bd4fed7136",
        "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4",
        "refinement_interpretation_Tm_refine_4db8ba22c4504a66577a2159dcc603cd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c",
        "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_b7508c8246dd025aecf4ee8c56206add",
        "refinement_interpretation_Tm_refine_bc552b2c624e2add758b3ac761c0c563",
        "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
        "refinement_interpretation_Tm_refine_e07051c88e3784a2480ae13a521fed4d",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv",
        "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.add",
        "typing_FStar.UInt64.mul", "typing_FStar.UInt64.sub",
        "typing_FStar.UInt64.uint_to_t", "typing_FStar.UInt64.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.q_preorder",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.ConstBuffer.qbuf_qual",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Vector.__proj__Vec__item__sz",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Serialization.hash_vec_bytes",
        "typing_MerkleTree.Low.Serialization.u64_add_fits",
        "typing_MerkleTree.Low.__proj__MT__item__hash_size",
        "typing_MerkleTree.Low.__proj__MT__item__hs",
        "typing_MerkleTree.Low.__proj__MT__item__mroot",
        "typing_MerkleTree.Low.__proj__MT__item__rhs",
        "typing_MerkleTree.Low.uint64_max"
      ],
      0,
      "288f94b9887a2f300175f88613acb884"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_MerkleTree.Low.const_mt_p",
        "equation_MerkleTree.Low.const_pointer",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3"
      ],
      0,
      "3fdefc0c7369774a0a1db6cb668aa455"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c",
        "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Int.Cast.uint64_to_uint32",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_LowStar.Monotonic.Buffer.get",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Regional.Instances.vector_region_of",
        "equation_LowStar.Regional.Instances.vector_regional",
        "equation_LowStar.Vector.vector",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_dummy",
        "equation_MerkleTree.Low.Datastructures.hash_r_inv",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "equation_MerkleTree.Low.Datastructures.hash_vv",
        "equation_MerkleTree.Low.Datastructures.hreg",
        "equation_MerkleTree.Low.Datastructures.hvreg",
        "equation_MerkleTree.Low.Datastructures.hvvreg",
        "equation_MerkleTree.Low.Serialization.uint64_t",
        "equation_MerkleTree.Low.Serialization.uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_mt_p",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.Low.mt_loc", "equation_MerkleTree.Low.mt_p",
        "equation_MerkleTree.Low.mt_safe", "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Monotonic.HyperHeap.lemma_disjoint_includes",
        "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
        "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.freeable_length",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.Regional.Rgl_r_inv",
        "proj_equation_LowStar.Regional.Rgl_region_of",
        "proj_equation_LowStar.Vector.Vec_vs",
        "proj_equation_MerkleTree.Low.MT_hash_size",
        "proj_equation_MerkleTree.Low.MT_hs",
        "proj_equation_MerkleTree.Low.MT_mroot",
        "proj_equation_MerkleTree.Low.MT_rhs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_LowStar.Regional.Rgl_r_inv",
        "projection_inverse_LowStar.Regional.Rgl_region_of",
        "refinement_interpretation_Tm_refine_02a311be716ab03201b91cc11abde92c",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
        "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7",
        "refinement_interpretation_Tm_refine_a2cc6d46f3d2c5d64a91203b6155bab3",
        "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_b7508c8246dd025aecf4ee8c56206add",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_LowStar.Regional.Instances.vector_region_of",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv",
        "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv",
        "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of",
        "typing_FStar.Monotonic.HyperHeap.disjoint",
        "typing_FStar.Monotonic.HyperHeap.includes",
        "typing_FStar.Monotonic.HyperHeap.mod_set",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Set.empty", "typing_FStar.Set.intersect",
        "typing_FStar.Set.singleton", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.q_preorder",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.ConstBuffer.qbuf_qual",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.get",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_regions",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.__proj__Vec__item__vs",
        "typing_MerkleTree.Low.Datastructures.hash",
        "typing_MerkleTree.Low.Datastructures.hash_vec",
        "typing_MerkleTree.Low.__proj__MT__item__hash_size",
        "typing_MerkleTree.Low.__proj__MT__item__hs",
        "typing_MerkleTree.Low.__proj__MT__item__mroot",
        "typing_MerkleTree.Low.__proj__MT__item__rhs",
        "typing_MerkleTree.Low.mt_loc"
      ],
      0,
      "b3f51d4ff1fb58d9885b3d68117bdf74"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Monotonic.HyperStack.is_heap_color",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.pointer_or_null",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype",
        "function_token_typing_Lib.IntTypes.byte_t",
        "haseqTm_refine_56b4e6db87090880a4837304bb2a2909", "int_typing",
        "kinding_MerkleTree.Low.merkle_tree@tok",
        "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "typing_FStar.Ghost.reveal",
        "typing_FStar.Monotonic.HyperHeap.color",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.is_heap_color",
        "typing_FStar.UInt32.t", "typing_FStar.UInt32.v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len"
      ],
      0,
      "af6f76bd9156aec8326c7b9271ab21a4"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "function_token_typing_FStar.Integers.uint_8", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "typing_FStar.Ghost.reveal", "typing_FStar.UInt32.v",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.len"
      ],
      0,
      "d5210830f9236f5b4c26a487ade855f6"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Pervasives.Native.None",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "data_typing_intro_FStar.Pervasives.Native.None@tok",
        "disc_equation_FStar.Pervasives.Native.None",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid",
        "equation_FStar.HyperStack.ST.is_eternal_region",
        "equation_FStar.Int.Cast.uint32_to_uint64",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.fresh_region",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.gte", "equation_FStar.UInt.lte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_FStar.UInt32.gte",
        "equation_FStar.UInt32.lte", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.get",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_LowStar.RVector.rvector",
        "equation_LowStar.Vector.size_of",
        "equation_LowStar.Vector.uint32_t",
        "equation_MerkleTree.Low.Datastructures.hash",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.Datastructures.hash_vec",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.Low.merkle_tree_conditions",
        "equation_MerkleTree.Low.merkle_tree_size_lg",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Prims.int", "int_inversion", "int_typing",
        "kinding_MerkleTree.Low.merkle_tree@tok",
        "lemma_FStar.Ghost.hide_reveal", "lemma_FStar.Ghost.reveal_hide",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd2",
        "lemma_FStar.Monotonic.HyperHeap.lemma_extends_only_parent",
        "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
        "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.new_region_modifies",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.Vector.Vec_sz",
        "proj_equation_MerkleTree.Low.MT_hash_size",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_FStar.Pervasives.Native.None_a",
        "projection_inverse_MerkleTree.Low.MT_hash_size",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c",
        "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95",
        "refinement_interpretation_Tm_refine_30494f3fd2c285e7cecf228074ade467",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_799df84338c1e83b596e1d04d8c7433c",
        "refinement_interpretation_Tm_refine_a3e91433acc705e2c7f5ab6f610b2493",
        "refinement_interpretation_Tm_refine_aac145f146e34cea91c3fd512c5b7261",
        "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cbd24d5334c6bfffa6fd8a84fb787f7a",
        "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
        "typing_FStar.Int.Cast.uint32_to_uint64",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.lte",
        "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.length",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.mnull",
        "typing_LowStar.Vector.size_of",
        "typing_MerkleTree.Low.Datastructures.hash"
      ],
      0,
      "a21f2e3b88747f7d9b008716ad455539"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize_path",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_EverCrypt.Helpers.uint32_t",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_MerkleTree.Low.Datastructures.hash_size_t",
        "equation_MerkleTree.Low.const_path_p",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype",
        "haseqTm_refine_56b4e6db87090880a4837304bb2a2909",
        "kinding_MerkleTree.Low.path@tok",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_bcef36c9fe2b6458c3fdda81179b025f",
        "typing_FStar.UInt32.t", "typing_LowStar.ConstBuffer.cast"
      ],
      0,
      "c955cefce631af6e1f958d26b8f02e97"
    ],
    [
      "MerkleTree.Low.Serialization.mt_serialize_path",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
        "equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_LowStar.ConstBuffer.q_preorder",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.ConstBuffer.qbuf_qual",
        "equation_LowStar.ConstBuffer.qual_of",
        "equation_MerkleTree.Low.const_path_p",
        "equation_MerkleTree.Low.const_pointer",
        "equation_MerkleTree.Low.path_safe",
        "kinding_MerkleTree.Low.path@tok",
        "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.frameOf"
      ],
      0,
      "56ecccce7ad1e62bd4d8c0bc35584578"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize_path",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "9f7d9c8ac0cee758f09a92d2f75a59bc"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize_path",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "1a954943025db4580de127769162f002"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize_path",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Pervasives.Native.None",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "data_typing_intro_FStar.Pervasives.Native.None@tok",
        "disc_equation_FStar.Pervasives.Native.None",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.HyperStack.ST.erid", "equation_FStar.Integers.int_t",
        "equation_FStar.Integers.uint_8",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.disjoint",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.fresh_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.gt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.gt", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.ConstBuffer.as_mbuf",
        "equation_LowStar.ConstBuffer.length",
        "equation_LowStar.ConstBuffer.live",
        "equation_LowStar.ConstBuffer.qbuf_pre",
        "equation_LowStar.Monotonic.Buffer.length",
        "equation_MerkleTree.Low.Serialization.const_uint8_p",
        "equation_MerkleTree.Low.Serialization.uint32_t",
        "equation_MerkleTree.Low.Serialization.uint8_t",
        "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_FStar.Integers.uint_8",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Prims.int", "int_inversion", "int_typing",
        "kinding_MerkleTree.Low.path@tok",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd2",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "lemma_LowStar.Monotonic.Buffer.new_region_modifies",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.None_a",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c",
        "refinement_interpretation_Tm_refine_0bf64d9ba30241c6c2ada0c32b378b8c",
        "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95",
        "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df",
        "refinement_interpretation_Tm_refine_a3e91433acc705e2c7f5ab6f610b2493",
        "refinement_interpretation_Tm_refine_aac145f146e34cea91c3fd512c5b7261",
        "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3",
        "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.ConstBuffer.as_mbuf",
        "typing_LowStar.ConstBuffer.as_qbuf",
        "typing_LowStar.ConstBuffer.qbuf_pre",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.mnull"
      ],
      0,
      "1f424cfadb96fd98c0fe87d7437d9309"
    ]
  ]
]

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...