[
  "����[�\u0015�\u007f�Յ{�\f�",
  [
    [
      "EverCrypt.Poly1305.poly1305",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer",
        "equation_Spec.Poly1305.size_key",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Tm_refine_d4c7098650bd63ee7195c3ca69b31faa",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "1ac92169b37f65c5ce0cd8277845cc46"
    ],
    [
      "EverCrypt.Poly1305.poly1305",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "b059a67891901fb378451ae31e423f35"
    ],
    [
      "EverCrypt.Poly1305.poly1305",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "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.W128",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W128@tok",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
        "equation_FStar.Integers.width_of_sw",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "equation_FStar.Monotonic.HyperStack.is_stack_region",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Monotonic.HyperStack.pop",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.popped",
        "equation_FStar.Monotonic.HyperStack.remove_elt",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
        "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_Lib.Sequence.seq",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.disjoint",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.l_True", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key",
        "equation_X64.Poly1305.Util.readable_words",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_LowStar.Buffer.trivial_preorder",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int", "function_token_typing_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
        "lemma_FStar.Endianness.n_to_le_le_to_n",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomRestrict",
        "lemma_FStar.Map.lemma_InDomUpd2",
        "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
        "lemma_FStar.Map.lemma_UpdDomain",
        "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
        "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_intro",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
        "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
        "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
        "lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
        "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
        "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "lemma_LowStar.Monotonic.Buffer.len_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.live_gsub",
        "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "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_region_buffer_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "lemma_LowStar.Monotonic.Buffer.popped_modifies",
        "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
        "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_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "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",
        "refinement_interpretation_Tm_refine_1119d78abb1039fd7b8c03b6be0d4758",
        "refinement_interpretation_Tm_refine_1e6ddbb476472075a9c8b9eb852a225d",
        "refinement_interpretation_Tm_refine_232745ea17b84a4e93c949a9bff1d2b1",
        "refinement_interpretation_Tm_refine_2bc144de01d64d7e672e94682c459e88",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4e25a7905e98128bc6f88dd9d64b6204",
        "refinement_interpretation_Tm_refine_56ab909861a887a471ba68f10063795f",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5a9b07a98aac9ef86cf806048f3fefbd",
        "refinement_interpretation_Tm_refine_6a722253105466a793c8366b0d8b327c",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6e3f78b75dbac4079b8eec2087da6bff",
        "refinement_interpretation_Tm_refine_814770d986f06f66b84225be16b5517a",
        "refinement_interpretation_Tm_refine_81aa92b7573e33eeaa7a335b747501de",
        "refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_9e8bec944afe09933cb5aed7ee6e285c",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b61138e8766a0c817530cc12518c3b0a",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
        "refinement_interpretation_Tm_refine_cf51693b595960604bbe46bea87bbc32",
        "refinement_interpretation_Tm_refine_d3f87b68b4bf3e552b80bbb81c580058",
        "refinement_interpretation_Tm_refine_d4c7098650bd63ee7195c3ca69b31faa",
        "refinement_interpretation_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_Tm_refine_e3588258e1439e7bbe20158183cb2f8b",
        "refinement_interpretation_Tm_refine_e36e7fa194162fb94cb448be97de0361",
        "true_interp", "typing_Arch.BufferFriend.of_bytes",
        "typing_Arch.BufferFriend.to_bytes",
        "typing_FStar.Int.Cast.uint32_to_uint64",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Map.restrict", "typing_FStar.Map.upd",
        "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.mod_set",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.root",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_rid_ctr",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.is_stack_region",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_FStar.Monotonic.HyperStack.remove_elt",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Set.complement",
        "typing_FStar.Set.mem", "typing_FStar.Set.singleton",
        "typing_FStar.Set.union", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.add", "typing_FStar.UInt32.div",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.loc",
        "typing_Lib.ByteSequence.nat_to_bytes_le",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.as_addr",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_addresses",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
        "typing_LowStar.Monotonic.Buffer.loc_regions",
        "typing_LowStar.Monotonic.Buffer.loc_union",
        "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "173cb6034245b1bc69d456c49fc1c92e"
    ]
  ]
]