[
  "\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,
      "097c63d7339ad1bb8bd11acfefb6c7b5"
    ],
    [
      "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,
      "2ba3692b5d7b47f392f801819b0c70dd"
    ],
    [
      "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,
      "8a13167daaabff10f342d11455300406"
    ],
    [
      "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,
      "24a1ca13131719460b68904a53097c6d"
    ],
    [
      "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,
      "5cdf7e5aab078d783c719bd4ccaded6e"
    ],
    [
      "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,
      "b3fe1cfc3fed3412ac347c9b6733ceb3"
    ],
    [
      "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,
      "87058536e3f71e7cc8975fcb5b34fb1e"
    ],
    [
      "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,
      "43204d5fa4d432b2f59546a6e1654355"
    ],
    [
      "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,
      "e9d3706ccfbab37ea97438a4d7ec4e8b"
    ],
    [
      "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,
      "2e854d0e65e6bcabd4a5973b4f7b47dc"
    ],
    [
      "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,
      "acab870abf2e993c328e8e439fb820fc"
    ],
    [
      "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,
      "444abb037695d088c7f1d312596cdfd9"
    ],
    [
      "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.U1@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",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf",
        "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",
        "proj_equation_Spec.GaloisField.GF_t",
        "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",
        "projection_inverse_Spec.GaloisField.GF_t",
        "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_de8080fdc4bd6678af723874a7d70466",
        "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", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "9d23730e5a14f989bf9039a8078194ff"
    ],
    [
      "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,
      "59d63ceb3398a62948651f9365a06d22"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_bool",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "e6bb15c6808eeb267d8026b7e85b72aa"
    ],
    [
      "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,
      "8b3686116c44a64fbc23944cbab6983a"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint8_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "7cefaa9238fed1f3c80811d2dc57be64"
    ],
    [
      "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,
      "b830642edfa9380fc6a68cc85eee40e1"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint16_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "ceb4baa9fb179acd4e34e0499ff610e5"
    ],
    [
      "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,
      "e72e2cbf211026117134f46835e12c03"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint32_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b7d095ef081e6af2b24548bc4d2b330f"
    ],
    [
      "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,
      "fb5226489e053698acbca3801d3251b8"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_uint64_t",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "c1e25d230348b592722b9a10513bebf5"
    ],
    [
      "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,
      "2fbf9c95898cee07651650e723c5e10e"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "83901a9ea3a7be1f9069763c3f552be1"
    ],
    [
      "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,
      "f89351fced41ad9b4b3f80adda16349d"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec_i",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "2954b25258e1ea5bd91775d29d32ae33"
    ],
    [
      "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,
      "cf8cced4844547880ba1be5fdb691a3d"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vec",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "0cf777d7abd0d51682aad75c60dfe8b0"
    ],
    [
      "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.U1@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.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_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq",
        "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", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "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",
        "function_token_typing_Spec.AES.elem", "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",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "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_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.UInt32.gt", "typing_FStar.UInt32.lt",
        "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned",
        "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", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "95997aff949f8891ceeb9e84c1528dc8"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv_i",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "ebc7f8c216aa58e89fae4a5f84f660eb"
    ],
    [
      "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,
      "94a6f2219b641fabdae6bd961f6e75a0"
    ],
    [
      "MerkleTree.Low.Serialization.deserialize_hash_vv",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "269c22dbaa56190af1dcc5b63dd3cf4f"
    ],
    [
      "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.U1@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.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.unsigned",
        "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", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "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",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "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_de8080fdc4bd6678af723874a7d70466",
        "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.rid",
        "typing_FStar.Monotonic.HyperHeap.rid_freeable",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Set.singleton", "typing_FStar.UInt32.gt",
        "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v",
        "typing_Lib.IntTypes.unsigned",
        "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",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b614f80516dbb6d9a5574d6b650bee38"
    ],
    [
      "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,
      "3093d4bccb731bb4aabb24dbf1b1b1c2"
    ],
    [
      "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,
      "e56d6c15599db3b904d8e35fafe6473c"
    ],
    [
      "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,
      "6ff12944e879061ce39e557b4c33391d"
    ],
    [
      "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,
      "ad6de9ea0db38aa3ca46e39600bf157b"
    ],
    [
      "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,
      "4a97c2761cea1d7e67008cd24108a854"
    ],
    [
      "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,
      "64cd24ab27715fcd74679c8a0a71db90"
    ],
    [
      "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.buffer",
        "equation_LowStar.Buffer.pointer_or_null",
        "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.__cache_version_number__",
        "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_33818f36d361a5f8bc0487fdff0c49fc",
        "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_cd18e9962a0d204005dcfcda04529ffc",
        "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,
      "1aae2730c6b1b21af940e7215f72cd22"
    ],
    [
      "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,
      "60e0f1c011e151ba49061cc0ee4d9334"
    ],
    [
      "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,
      "934f0c691041ca4397028cf999ee375e"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize_path",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5f3663b9a21ca8bbb079d86ad8bab8d5"
    ],
    [
      "MerkleTree.Low.Serialization.mt_deserialize_path",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "ac2c1d16e54cb493fae82f0e1a07ab92"
    ],
    [
      "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",
        "MerkleTree.Low_pretyping_7e119b85ec1bddfeba5c5e23b7ab201f",
        "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.buffer",
        "equation_LowStar.Buffer.pointer_or_null",
        "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.__cache_version_number__",
        "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_cd18e9962a0d204005dcfcda04529ffc",
        "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,
      "033c5eea6d266c845f219feace7925f5"
    ]
  ]
]