[
  "*t��t�U�5ab\\\u0001Ρ9",
  [
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c773e4967c768f6c1d8286aaa157853a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp"
      ],
      0,
      "bfa828777a9b682320f4463a54539b9a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "ae8eb27fd75c1e04091b3ffe2e7f06d7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_typing", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "380016ec8a8f9d70a6fb8c2098f5df4b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_typing", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "9f542ea94b5b443dd198aeacdd6d9ec3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "5a342902482ae8c7ea4c1d075d97ddb8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr2",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7c1969c95aeee006b8c6880cfa73e246"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "499962af72527b25558a8b579aff5523"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp"
      ],
      0,
      "ad367011db07caf115e8c60550c86e0a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "7e70c9020e6ba0dfd9b477e0dd662446"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "c25aea7de941f2a8781ea224a36caa71"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "cb49bc0fb07a4c77fc8a601f8daca7d2"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "adcdb63dfd8ae1ec9fe1e388d9d08b32"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_shr4",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "480fc245025c75f845e004c950e3b801"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits"
      ],
      0,
      "15694485dc3a71c7efbcc4d96c241688"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "d21e0536e10742d87a8919ad7bee2786"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "e02f7fd871125e6c4d42adf8b23f4388"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "4160ad21e0e89bc3cfa94cc662f0a471"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "06923d90f65edc96b91fe2060f098cb1"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "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_045feaff96c939e73ccd5d7de8e4a488",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.UInt.fits",
        "typing_FStar.UInt.to_vec"
      ],
      0,
      "a2cc654e64bfa1fed7dc9d54c895b572"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      7,
      1,
      0,
      [ "@query" ],
      0,
      "1d708eca82c904883e209f1f92e8d72f"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      8,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "6eabddeed5b3d9b143d8c22560f5eca6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      9,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "62f2eec1f9c81954fa1294809245df32"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_mod_n",
      10,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1",
        "refinement_interpretation_Tm_refine_ae088b609204e032b97ba5aef2efdb95"
      ],
      0,
      "948dcddc5a0dc2275d7ad425f2aa0e34"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits"
      ],
      0,
      "1fc3c058e42a6c47af1d50deb4637ed3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "2a3027534e5835547656de64acc61023"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "768a45ff904bbdd5ded2a71827eccc9c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "e6f8158a0df3f75e68d05503e0a66f59"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "cd253e8dc2a19122138fc1b916d8ed4e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "dfe8e813388581b6d8698511b4100341"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "31ff00eef37d2e5fa7527e60f7960cef"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
      8,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9c12fb09160ff7a001213e7f87934303"
      ],
      0,
      "fd485ff60df5c7aedfee3453b1c08da0"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "749cb220d2be24b1a5318892dff00bdf"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp"
      ],
      0,
      "400cb42bc8884fbed3f01baa01ce99b7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "ea5c07e6afc43997b5ff6d40d6e86078"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      4,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "71e1a6cabe65be90b7f99c7d95115b57"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      5,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "b6575c5d73f4caa17bcd53a45e6dce7e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      6,
      1,
      0,
      [ "@query" ],
      0,
      "270cd2ac17e4e5d95f91cdf5c49e5c4b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_constants",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_2058df7f678abb27e3e3b80b6c07d514",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "6e00cf433a0bce9ebf779dd28daa0fe7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "be0cd4a13e3780541cd914aed811475b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "c83f85abdc203b3b26e5bee45b7adf7a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "8f2e6bca5bd4198ea4ab9b6749d69f7d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      4,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_cd0ab3cd862bf71d820fca2a2683eb4e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "64f8349a8d534e9d55d24c293c0fdeb3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      5,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "4f0bf4181a5d9b565219483c3d418c53"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      6,
      1,
      0,
      [ "@query" ],
      0,
      "ad14518b8f047468f04c1133ccc796c7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      7,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_7a38babb012d4430b4bf955e1ec34561",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "965316ce7deec5253b9e6bdd2b25e8e4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      8,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "f7ad2e8e2e0fc7bd29568249a116d3e9"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      9,
      1,
      0,
      [ "@query" ],
      0,
      "e9a0aaaafffe876583856a354b656623"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_7a38babb012d4430b4bf955e1ec34561",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "4b7ae39e22080d18dc3ddc8b043842e7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "9bfe1b38ed36127142cd35dd855c424c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      12,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "d7efe8d2a421ce6094b653827a5aa921"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_poly_constants",
      13,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_64b0aa59998320440bf5be332fb7a4f2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "b8da42da2c781f937825708d909900ef"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_commutes",
      1,
      1,
      0,
      [ "@query", "true_interp" ],
      0,
      "696889ac8597f01691e41ece3a9633d4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_and_commutes",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "6be9bc79ffb5dc59b605e5eca3aa63dd"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bv128_64_64_and_helper'",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "6c8aa64e1df2b8e636057a059311b30b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bv128_64_64_and_helper",
      1,
      1,
      0,
      [ "@query", "true_interp" ],
      0,
      "cd26ccbd162e345e4223ef4534069e28"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bv128_64_64_and_helper",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "projection_inverse_BoxBitVec128_proj_0",
        "projection_inverse_BoxBitVec64_proj_0",
        "refinement_interpretation_Tm_refine_c56804022554b54425861cac611cccb4",
        "refinement_interpretation_Tm_refine_ec5c8ae42eac80d2d1b6d904c9523e69"
      ],
      0,
      "869531c10e8bbdd34ae369eb31db28e0"
    ],
    [
      "Vale.Poly1305.Bitvectors.uint_to_nat",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "34eabeb22f5231ff00f514700ed5c8a9"
    ],
    [
      "Vale.Poly1305.Bitvectors.uint_ext",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.to_uint_t", "equation_FStar.UInt.uint_t",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits"
      ],
      0,
      "8e0e8e98c84d31c7639334d18459ccd6"
    ],
    [
      "Vale.Poly1305.Bitvectors.mul_bvshl",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.nat", "equation_Vale.Poly1305.Bitvectors.uint_ext",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_3053c8e9fa8bcd8df8e3179077055b61",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_Vale.Poly1305.Bitvectors.uint_ext"
      ],
      0,
      "f54c7ecae00856364f3fdef9eda9905c"
    ],
    [
      "Vale.Poly1305.Bitvectors.mul_bvshl",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f8b5b242d96e8ce0bd565c48ec641966",
        "typing_Prims.pow2"
      ],
      0,
      "c46d5a3a29cd1e2004c31ea03defe074"
    ],
    [
      "Vale.Poly1305.Bitvectors.plus_bvor",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "25b75cc5430c0178427f2f88fe6aaf91"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bv128_64_64_and",
      1,
      1,
      0,
      [ "@query", "true_interp" ],
      0,
      "ba0648486572cc2424960b9f1495e480"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bv128_64_64_and",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Poly1305.Bitvectors.bv128_64_64",
        "projection_inverse_BoxBitVec128_proj_0",
        "projection_inverse_BoxBitVec64_proj_0",
        "refinement_interpretation_Tm_refine_e86593445f6419d21e77060f88d51853",
        "refinement_interpretation_Tm_refine_ec5c8ae42eac80d2d1b6d904c9523e69"
      ],
      0,
      "9fc792204bf3cf1c4dd2a38afb045ad9"
    ],
    [
      "Vale.Poly1305.Bitvectors.lowerUpper128u",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "eda521ec4ff049f5c5a2434390b1cad0"
    ],
    [
      "Vale.Poly1305.Bitvectors.int2bv_uext_64_128",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.squash", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "acb2b713b29a0d07f9af3f66834f7c90"
    ],
    [
      "Vale.Poly1305.Bitvectors.int2bv_uext_64_128",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1a6b6e376eef1cd28182da451df7925"
      ],
      0,
      "c78d64baf3716ae975d8ad947cb06265"
    ],
    [
      "Vale.Poly1305.Bitvectors.lowerUpper128m",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Math.Bits.uext",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6b0eda4eb5978ef303fd4d2a10033f86",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.max_int", "typing_Vale.Math.Bits.uext"
      ],
      0,
      "8cb7f4488ac2be9b7e74c2fa6ce60988"
    ],
    [
      "Vale.Poly1305.Bitvectors.lowerUpper128b",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "75bae479326baf5b31cefdd8a82f26e2"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_lowerUpper128_andu",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
        "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Math.Bits.lemmas_i2b_all",
        "equation_Vale.Math.Bits.uext",
        "equation_Vale.Poly1305.Bitvectors.lowerUpper128b",
        "equation_Vale.Poly1305.Bitvectors.lowerUpper128m",
        "equation_Vale.Poly1305.Bitvectors.lowerUpper128u",
        "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c91e66c97ed3054dc88c856ecfaebc1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c6a5ae056cb5a72f4660066bbd48d8bd",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.BitVector.logand_vec", "typing_FStar.UInt.to_vec",
        "typing_Vale.Math.Bits.add_hide", "typing_Vale.Math.Bits.mul_hide",
        "typing_Vale.Poly1305.Bitvectors.lowerUpper128m"
      ],
      0,
      "23d145f845c51d608d24b39f867af658"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "6f271d62d3566d3be129e646e0fafe2d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_Prims.pow2"
      ],
      0,
      "6bb37561e07099d91891eb4258ad7bf4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "3ef92d19e9ec1f207d900e0ca14cb38d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
        "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
        "equation_FStar.BitVector.shift_left_vec",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_left",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
        "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0d2be3818ed499a11a1a02c7a3629ed",
        "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.BitVector.shift_left_vec",
        "typing_FStar.Seq.Base.create", "typing_FStar.UInt.to_vec",
        "typing_Prims.pow2"
      ],
      0,
      "ce72bc8cc625dcde67c73731802fb9a1"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      5,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "e5985e70fb7023fa68f1d49d24674d89"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
        "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
        "equation_FStar.BitVector.shift_left_vec",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_left",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
        "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0d2be3818ed499a11a1a02c7a3629ed",
        "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.BitVector.shift_left_vec",
        "typing_FStar.Seq.Base.create", "typing_FStar.UInt.to_vec",
        "typing_Prims.pow2"
      ],
      0,
      "608be049dd633da331adcdfec0158091"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      7,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "e15cfcd29ce433c996f22b0c25b5b4af"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "78bb93997d2218351caa5597bae9e343"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_5d4499fa92e44a19dc1f1ea90c5ac6f6",
        "refinement_interpretation_Tm_refine_a0d2be3818ed499a11a1a02c7a3629ed",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "08904db21609d1918e9636ea70f70e6d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      10,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "716862b6b6bbebe8ab0f5abed5267990"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_5d4499fa92e44a19dc1f1ea90c5ac6f6",
        "refinement_interpretation_Tm_refine_a0d2be3818ed499a11a1a02c7a3629ed",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "d257cc15e4153b6535d8ca2954794ebb"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants0",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_4bb8998fe69acc99b21e814adae749a3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "ac6f28c61ac5bb8fa74792cfd28e153b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "77c13bc91997a023c6f46c7568bf8378"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.UInt.fits"
      ],
      0,
      "dd7a5aee3b78e046cee2a1fa64192dea"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "54adf094220ebb58d286a5e48c7fabc8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "57c00cc461afb0dd7470e10e259c069c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "1aa538facee9e4a7b87fcc074a38e7a6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "2d8e90c4b731a7112aa2b9376502bdd6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8836626372248741cc7d6582bd93782",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "0421539fefe10850b45a3d8fef4394b4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "6d32440728dc8cf1df8e9c79fb4afe92"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_6e4b6a3bc62a81e54556d05317a88bb7",
        "refinement_interpretation_Tm_refine_c0be3d2c292eb10672724315a42ff4ed",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "eb0afeb3411febc6ed82c830a0441ec0"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6e4b6a3bc62a81e54556d05317a88bb7",
        "refinement_interpretation_Tm_refine_c0be3d2c292eb10672724315a42ff4ed",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "60030c8107d3a96b1da323bd127af109"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_6e4b6a3bc62a81e54556d05317a88bb7",
        "refinement_interpretation_Tm_refine_c0be3d2c292eb10672724315a42ff4ed",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "5ca0d622085f7666d2a56acb146713a5"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants1",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_2bd847f7dedd5f8c0ccfa10349b2470b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8836626372248741cc7d6582bd93782",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "c9d567167b5f96b527f7ff5e2fb25b41"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "81e045746f03110ec81dc5d54c02a504"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "de10fac5bed6ad82027d1b3889a7deb8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "326701694039517b645ec1ef08ae514c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "e223f489fa8f8f6692e26e68bac607a2"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1",
        "refinement_interpretation_Tm_refine_a7a18b3d2bbe32ad1d7773e62663094f"
      ],
      0,
      "8c1116b5b30d1592f071cee9c358c6f3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "29fb216bb043cd9aef2f1a4af88375d6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1"
      ],
      0,
      "c1134c20748985cf8b091dcc58868634"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "25f6492019bf4d5afc99be8885d3212e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_30414f165f634d1d5242aa07d66adbc8",
        "refinement_interpretation_Tm_refine_e491d4c19c2c46d0915df57189ee1dad",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "616ec0083ff89d73df8aa4e85e4c4a76"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_30414f165f634d1d5242aa07d66adbc8",
        "refinement_interpretation_Tm_refine_e491d4c19c2c46d0915df57189ee1dad",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "75d7026dd20e74b173dbe5dee62524e5"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_30414f165f634d1d5242aa07d66adbc8",
        "refinement_interpretation_Tm_refine_e491d4c19c2c46d0915df57189ee1dad",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "980d98a3cdfa5b40af94a12963df6f2e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants2",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_986b3d1bb94bf57fa4d40e63127dc5c1",
        "refinement_interpretation_Tm_refine_a7a18b3d2bbe32ad1d7773e62663094f",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_ed24a72559e6d95bc4aa8f08c105ba2f",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "5eb6c07c6c2e9b9bccdf123f4d4521cb"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "70588dca1a12d6fdfaf95e873eef6f93"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "127f5b6d66b5a4fb58e93dd9e1d86119"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "45e99aa4fbb3cbc40263289a2f577c77"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_045feaff96c939e73ccd5d7de8e4a488",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "f37bb1b061f4220cb48f7ad39d324da3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_045feaff96c939e73ccd5d7de8e4a488",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "9df6242fdec4e499d6781826874cdef8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_045feaff96c939e73ccd5d7de8e4a488",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "06785c95681fda97b086c6b199ab17d6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_63c0cf93c4d449b5b9d1b12e355a0400"
      ],
      0,
      "c7a1c02a18cb3d7910b82ef089abfb27"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "cfaaa1645d6334e0f0c3674ad243a8b6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_2ae30301407ba3dc93e49e645c32177c",
        "refinement_interpretation_Tm_refine_d730384adee79cebfeadaabbf7839af7",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "5b24f431d369764e4e1de99bd4bf0212"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ae30301407ba3dc93e49e645c32177c",
        "refinement_interpretation_Tm_refine_d730384adee79cebfeadaabbf7839af7",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "cf6a71b6299e6587f22ce7969db883c9"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_2ae30301407ba3dc93e49e645c32177c",
        "refinement_interpretation_Tm_refine_d730384adee79cebfeadaabbf7839af7",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "ad09068f5bc180e1a9e83603eead3caf"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants3",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bca658aa64bc5735e3ededc363500da8",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "fbadb521e7124ef58cf47c30a546dfcd"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d781d7ad2e8e8d7b8a906de4dd9345d3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "3acbe364f2bfb24ef088c0a4510c5e06"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "a7e9be42dbea3beb8254066040ac7d4e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_1e77b5c9709b25329ec1e9a6a79fa90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "31e94cbf40306a0524e8e0e031f561bc"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_1e77b5c9709b25329ec1e9a6a79fa90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8e275cfa492c73f52b5f32fd4e8a7155"
      ],
      0,
      "0380b76180f92a623b12007edce703b1"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_1e77b5c9709b25329ec1e9a6a79fa90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "a1f2068a2b6fdb6e9b5a8a419e44a154"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_1e77b5c9709b25329ec1e9a6a79fa90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7319df5c149eacf9683df78f9600e5ad"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "285ec01663e082255d36ba53c5f6ad02"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_33e1fddbba764f57973fbe50740dbead",
        "refinement_interpretation_Tm_refine_c8fe22df2550385ad8288573cfaa0358",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "47d6e180770e74ae91a7f71acd019017"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_33e1fddbba764f57973fbe50740dbead",
        "refinement_interpretation_Tm_refine_c8fe22df2550385ad8288573cfaa0358",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "86bcaec53f0484fe3502e35f48631d80"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_33e1fddbba764f57973fbe50740dbead",
        "refinement_interpretation_Tm_refine_c8fe22df2550385ad8288573cfaa0358",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "ea0be9b76e918b7670826e13b25eba5a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants4",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_1e77b5c9709b25329ec1e9a6a79fa90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bd89f601c4e1e2a25c87dfc424c60a21",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "817d47d06b33d37283435d3440c9abb1"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "05cc473627e637248c4687da09ac4369"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "61789528a4355a8ae29fcb5e5cc2fe42"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "9a86749d120c1fa174b38ed7a8fca10c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "cc361028b740adbf11850605dc5a247b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_17842b692fc36ec40a803769d235f928",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "98427ef271d88555c5031e4421aa5f09"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7388f698bb51c3e3ab11ae5b397afa5e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_3625590d087d0d10f3cdcea079eeb351",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "29581e4b7dbd87d4bd0f95f5351dbdc4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "2764ec414a92f897770324c72b4d4457"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_757cfaaee9b88057ff842254440ce8ba",
        "refinement_interpretation_Tm_refine_c73fc168ae40a96ad31f7aea550b6103",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "fe61380cf90de2af27d4ef0f9bbe4f0e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_757cfaaee9b88057ff842254440ce8ba",
        "refinement_interpretation_Tm_refine_c73fc168ae40a96ad31f7aea550b6103",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "853aff39d094cdf0a5219e4ca50d0919"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_757cfaaee9b88057ff842254440ce8ba",
        "refinement_interpretation_Tm_refine_c73fc168ae40a96ad31f7aea550b6103",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "b6161f51155ef501cc36ef51f35fbd44"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants5",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8a5f244d53592fb3a63de62cfcbccfec",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "55cd7ad2dd060a72766ad0cd86d72157"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "1d743101e42bbbcca7bfe522ea175fd9"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "cce47eb7bbf83caf1682687959e51d67"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "eb2bc4426f301a439f96b077eeb12749"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "9be3e3f8905074f724692a4224708ea7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bcb4c74dd9c0210c7a566434f6c21fa1"
      ],
      0,
      "2cb4e668d3e0e1476c3fa0f49f4b8cee"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "40cf79de3f1e448e649795b0f5924da2"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_01b887a5163539618c830389659390df",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "bd20bfab889e9e94b758a4eb06667f9b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "8880cbf9d917289235ea81df4516638a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_01b86c072fdc8bcb686a3b9012e5f190",
        "refinement_interpretation_Tm_refine_d969f1aa1274e0da999b26974295e887",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "e5c21e0d203fd0023201ef9c4a01e28e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_01b86c072fdc8bcb686a3b9012e5f190",
        "refinement_interpretation_Tm_refine_d969f1aa1274e0da999b26974295e887",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "7b1c298a48c3e78f967297e4cc0332e8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_01b86c072fdc8bcb686a3b9012e5f190",
        "refinement_interpretation_Tm_refine_d969f1aa1274e0da999b26974295e887",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "81b25f95958ec95b6fd209908756d660"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants6",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_599e43830bbbaacbaa5e9e7bc0734208",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "0d739502f3557ca847499fc19bf4061f"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "14260c1c146dd5e037487209e91a0b00"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "308b4147719f89e162a05b3d1bacc668"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "7d5c0d5914bf6c337ca28013bf4a08c0"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d125fc007f7686166210ae6ea7d65d50"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_63951cf891d05f4c4ee21aee034efca6"
      ],
      0,
      "73a2d4b305cac099c5bf4b9a0a0c2b45"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      6,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "854776764c5e8acf2d1e9ea7a922f180"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      7,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e8d8996a0520d799b82919241f7a58d4"
      ],
      0,
      "7cf337b5f39a58749c6c0fe7283c900a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "1df3e81cb1ca4eb924f13d22bf2076d3"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_2f0b6555080cb45835e9907794515b7e",
        "refinement_interpretation_Tm_refine_c13973d5e8bb99c2b02d9d47d55e22b6",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "d1c923685aa1a4fbc1b97b783660fdc7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      10,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2f0b6555080cb45835e9907794515b7e",
        "refinement_interpretation_Tm_refine_c13973d5e8bb99c2b02d9d47d55e22b6",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "a241fee07e07d0de9d41e1438f741e00"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      11,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_2f0b6555080cb45835e9907794515b7e",
        "refinement_interpretation_Tm_refine_c13973d5e8bb99c2b02d9d47d55e22b6",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "e5fbdaadcc96868a9426205376528d92"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_constants7",
      12,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96eb0b30da4f22e2bae813e96cac2e82",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15"
      ],
      0,
      "f693c88d39f941aafb86615d1cd509db"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "fb4b6325e5c96ce831a505d77397d79d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp"
      ],
      0,
      "2c0bd347ef31e9f7979dfb31dd93f101"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "9881429bc7ea0640148b5e92744fb77c"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "b8bb668d4dc5e588de88269c952272ea"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e9fd75cceaaeb3c4516e200cfb4bee15",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "4c6e29cce0094689a08a16b71f2645b7"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod0",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_0cc3b8bc4390a8152398abb544530a43",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "734a3ed10fc70a6170613594124bebce"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "dd53446d10643ee6ab89d9786d87e093"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "d6bf28778fa5afa7a05046d578192235"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "498e6dd84406939c38f44e16216f8d88"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_2bd847f7dedd5f8c0ccfa10349b2470b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "3eaa6f6c2415502da6b25cef6765c968"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_2bd847f7dedd5f8c0ccfa10349b2470b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c2360b7e46e6ee3c856abca5ae7b5173"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_1e912a01f562d84e2decab9945d4c6ea",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "75f638fac0b117626d41e1c5876254d0"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "fc5c934f3fe9b5bc7efe963805718c0d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "a166e0880d05d167a3fa679aa3407a6a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "412ca786303bf44346c3e02832198c61"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ed24a72559e6d95bc4aa8f08c105ba2f"
      ],
      0,
      "3d28132b4cd733fa44f888ff238dd8c8"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ed24a72559e6d95bc4aa8f08c105ba2f"
      ],
      0,
      "9bcb4605a2749127416c92b257e2fe0f"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod2",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_7b6b83afd9733f0a04b5718436f8d408",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "f6cb6bd24a6f458063f56716786c1e89"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "1138f815659f63a1a3c2f18abba3bdc6"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "865c3e9f03fbce38cdec684f50de4cbf"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "9e96f81dd208a50a26ec9037b3b29cf4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bca658aa64bc5735e3ededc363500da8"
      ],
      0,
      "f9b169540e39729f51035226b5810f02"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bca658aa64bc5735e3ededc363500da8"
      ],
      0,
      "ff17e8ca2d17877b9031bd623c24b35a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod3",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_7823c69564b57033bac02ce7c906711d",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "5a4c792eff04214b4550690a45456981"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "8bbae39e64aa2f95503c71ee0af1c784"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "ff6033d3181093d7ab638f61e8b0343d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "14133c790d418c42f8b1474ead44143b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bd89f601c4e1e2a25c87dfc424c60a21"
      ],
      0,
      "5d61e4fd454cc10a628e4033f85f1699"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bd89f601c4e1e2a25c87dfc424c60a21"
      ],
      0,
      "830295c0eb2027426b073cacab3e64b4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod4",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_cd6c3d2b07f6023bdcef4ac62fa5d79c",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "27e4371392c4f332c76f35176fb09e59"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "9ba090be7170151bebb5970d8569505b"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "ffda9d211e3f7ef1fd123d73719ac361"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "54643f83dcb7af405a317c729227e204"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8a5f244d53592fb3a63de62cfcbccfec"
      ],
      0,
      "d5f0f9ea162baae033539f751ee94929"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8a5f244d53592fb3a63de62cfcbccfec"
      ],
      0,
      "6a06a7b2d32e55b8843227a87950f288"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod5",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_b8dfb09524b7641835f2d255bd6cc0df",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "8ad0e88ed0d09af093764be8d2186bbf"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "3366e94600fbceb9a0369631822c410a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "3e4d401422b4fcafc0965cacc58e86f5"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "f940dadf94dbabf8fb37c10b26467486"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_599e43830bbbaacbaa5e9e7bc0734208"
      ],
      0,
      "bcaaecf50b90f52e067cb2048206e81d"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_599e43830bbbaacbaa5e9e7bc0734208"
      ],
      0,
      "4ee10244805db1ae1d9135c522b9e784"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod6",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_220e22fbd32bdc7b457063c0ef41d1cd",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "2fa04648dc16c8e459361e42f03c46fd"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "f98c7f16a01cdf40aed26b1ffca13165"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "true_interp", "typing_FStar.UInt.fits"
      ],
      0,
      "71438552ca03303f6e4b56bb2ad04a26"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "3b9f9a71369c677b5ede40e337439023"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      4,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96eb0b30da4f22e2bae813e96cac2e82"
      ],
      0,
      "a82cad6e044a7a9077a5ca5909754937"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      5,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96eb0b30da4f22e2bae813e96cac2e82"
      ],
      0,
      "7226ec115a42283e0146b7a95f7b56ce"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod7",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "refinement_interpretation_Tm_refine_2428ed024039b8855430c0fa9deb412a",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "709fe54f71101c18e9eb83512bd27c07"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_left",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.shift_left"
      ],
      0,
      "1cd3dc38eb9c547ab4967f02362d67f4"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_and_mod",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "2657e2fc0057a25fb748b6e76a7e669e"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_power2",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8130f04884ed893ec6484aa91242725a"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_power2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_FStar.BitVector.shift_left_vec",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_left",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.BitVector.shift_left_vec", "typing_FStar.UInt.to_vec"
      ],
      0,
      "3e97ffc517fe043f2ed765f59650a786"
    ],
    [
      "Vale.Poly1305.Bitvectors.lemma_bytes_shift_power2",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "c6d81e482cd7a1dccc0105823cf601ce"
    ]
  ]
]