[
  "æ1%Žlªjw<Y‰I\u0018\u001dOý",
  [
    [
      "Hacl.Impl.Poly1305.Field64.as_nat",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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_847e96a1feedc748e1951d8c6bc1015e",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2"
      ],
      0,
      "fb6edd5b4ed35ca86b2ad8ee1d5991dd"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.wide_as_nat",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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_8ca277f814d2a7f57ae12602242376a4",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2"
      ],
      0,
      "8c5125db6ce38bf65cfa6688ec0fa85b"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.create_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "c6bd55286d3ba5ca68d4c8552370be38"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.create_felem",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperStack.is_stack_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6b7f09e7622f68539f4655489f095bfa",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b5ed10fe6cdb264ee69337fcedb9da96",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "31fbf6194aa798745691d9e7c5ac1f25"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.create_wide",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "53f0efcb859b7b29f56034f2dda2e776"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.create_wide",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperStack.is_stack_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6b7f09e7622f68539f4655489f095bfa",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b5ed10fe6cdb264ee69337fcedb9da96",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "797dd360c3962cbbd2b2e1759f43b268"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.mask44",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "2ae0e1094a222d012da8edd3c402c73f"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.mask42",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "9d4d84e2335eb27335ae22573a7db598"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.load_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.mask44",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_fd7a6b02730b17637ac7a29f1f38874c",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Poly1305.Field64.mask44",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "dcec32e1c0f5a458bfcfd237b3e385a1"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.store_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d87f9f8caca91612a04e4527918b9238"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.set_bit",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Percent_Dot",
        "equation_Lib.IntTypes.op_Slash_Dot",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.div_lemma",
        "lemma_Lib.IntTypes.mod_lemma", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4a34935eeba50b27dccb698391a74562",
        "refinement_interpretation_Tm_refine_96882651b42b971f097bcdca8bbde91b",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "token_correspondence_Lib.IntTypes.div",
        "token_correspondence_Lib.IntTypes.mod",
        "token_correspondence_Lib.IntTypes.op_Percent_Dot",
        "token_correspondence_Lib.IntTypes.op_Slash_Dot",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.Buffer.MUT@tok",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "ade36d24ccb20da311515584fc7b6caa"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.set_bit128",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "9c9252f41ec0ddc3e0d705c069d590ff"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.set_zero",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "0c59a5dbdcf2472ee7059dad031a39d6"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.copy_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_3167e2cb65f6f5f927c17d6009e974fd",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "90783abd02eceb1ee9bddd2826758aca"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.load_precompute_r",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.precomp_r",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.l_True",
        "equation_Prims.logical", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.Buffer.modifies_sub", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "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.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.uint",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "de675f9547f597ee1283929d1120dce2"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.fadd",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "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.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "75037dcb5ec2138bdc88235a6c15391b"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.fadd",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_49f388450e5cfc91da46292c2a5d5b7b",
        "Lib.IntTypes_interpretation_Tm_arrow_64d9bcf6dc13bcbde626455717781a82",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.as_nat",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.op_Plus_Dot",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "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",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b4656f91da78ff16a953d7830084e524",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_f17ce12623fb5401c9c6496441382e03",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Prims.op_Multiply",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_Hacl.Impl.Poly1305.Field64.as_nat",
        "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.upd", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "72acd12df887e621ad33344d5054ddaf"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.smul_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.as_nat",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.felem_wide",
        "equation_Hacl.Impl.Poly1305.Field64.wide_as_nat",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.mul64_wide_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f17ce12623fb5401c9c6496441382e03",
        "token_correspondence_Prims.op_Multiply",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Poly1305.Field64.wide_as_nat",
        "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mul64_wide",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.Sequence.upd", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "55e3a13345ff4ff30c38b74c89a8f17c"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.smul_add_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "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.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "98df889db030ee422af656de8ec0a84f"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.mul_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "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.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.felem_wide",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
        "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies1",
        "equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_6b7f09e7622f68539f4655489f095bfa",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.root",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0466864b35896242414e6536c69d83d4"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry44",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_lemma",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4d098827d6c922bbd67478ce60a8436a"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry42",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_lemma",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "fa5372a73c6cc4ccf3171fce0ad5a54e"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry44_wide",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_lemma",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c533f40365875c9fe547187607f6f1b0"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry42_wide",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_lemma",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "98625ad8f7c009e8503cdf2d984171c9"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry_wide",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.felem_wide",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "aba70d963cd7716c00c5b8d147e5dd85"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e8650a2ba8f9d4be02bee859383258ee"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.carry_top_felem",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "521bac38ea306a7c984d3d24504606a8"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.fmul_r",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "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.mem",
        "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.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.precomp_r",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.root",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.is_stack_region",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "66ca141008b0da43fb688a8455b51109"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.fadd_mul_r",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "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.mem",
        "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.Impl.Poly1305.Field64.felem",
        "equation_Hacl.Impl.Poly1305.Field64.precomp_r",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.Heap.emp",
        "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.root",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.is_stack_region",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_none",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "45ed3f97714a507fc4b7462d0368f0bd"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.fmul_rn_normalize",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Lib.IntTypes.uint64",
        "refinement_interpretation_Tm_refine_3167e2cb65f6f5f927c17d6009e974fd",
        "refinement_interpretation_Tm_refine_f2f4e706d925538de401265323388171"
      ],
      0,
      "ff6e36ed35d4737b90c47d7dac1219e3"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.subtract_p",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "7c2c853fdbf56a33385a482b72675e8d"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.reduce_felem",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint64",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "83bfbfb6d5fd6e2a16626ecbd00b2ed8"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.load_felem_le",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "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.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_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_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_Lib.Buffer.length",
        "typing_Lib.IntTypes.numbytes",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "20db03f75398669589bdae2a2ffd9695"
    ],
    [
      "Hacl.Impl.Poly1305.Field64.store_felem_le",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "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.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Poly1305.Field64.felem",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.union",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.l_True",
        "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.Buffer.modifies_sub", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.size_v_size_lemma",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_19c9d892d71b94689f60811ae83ba708",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_7d28454cc602c65d0baeea87f419a4fa",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
        "refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperHeap.root",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.Buffer.union", "typing_Lib.IntTypes.numbytes",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "3d58c079090b523adb56bd009e19f708"
    ]
  ]
]