[
  "ãA½YD¸¯rvtýD¡º\u0014\t",
  [
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_add_distr_twice",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "61372690f02c8a97a4315ee023945b47"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_add_distr_twice",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "9d708084df6e3bc3dfa5949529796076"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_mul_distr_twice",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "843d82d8fb54e1e85813a916a6867d5b"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_mul_distr_twice",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b19016dadaff6de678dad54e5ee2faf4"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_add_mul_distr",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "3d61282cfc2ec37ec872b9007b92980f"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_mod_add_mul_distr",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "ff6045cd56d47dca6eba5549361ab49f"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify_lp",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "6c72235a850cfe79f2f878e3bd239e7f"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify_lp",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_65a74e6a36b6e5b6f006649316571ebe",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "275ef07ce655f6c5da19db8663eb4fc3"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify_rp",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "001b4e30e469389ed8300d84c5631136"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify_rp",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_65a74e6a36b6e5b6f006649316571ebe",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "e389310bff6bc7163e5a6fe786e5eca1"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "978ac706ff196573dcaffaa3bc462148"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "9cd6ddf996561144273f2a8f3c36f636"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "850c2f0148b9cc49466c0e04c126d686"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "2abc3d8629b1455ec53c78fe925a7e73"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "ec0d06f4a27fdc58f891bb1f0bf91f09"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_paren_mul_4",
      1,
      0,
      0,
      [
        "@query", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "f6f4303f3b76c09cc36c33c60ff1397c"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod4",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "5ea4c8343451dad46a26db43d1f25090"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod4",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "04a7e8751b1a5db85865204c0fe5cbb2"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod3",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "3f5113ad5014891f74c6da18d5a19a43"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod3",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Prims.nat",
        "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "59f07df4a3c3a73d0efff6a8dcdd78bc"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "8bcb7966b1f995d21a1408064460cdf0"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_remove_mod2",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Prims.nat",
        "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "049ae157667579137f2b7271a458723b"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "a6ec882f45b4150e0d60093026e724f7"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp1",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7f268c3987500a0b2d8132aef89ff22c",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_bef96b376eac7597d3b66f969135f633",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "b67e689f642ef317c8c07db5e7021779"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.paren_mul_right4",
      1,
      0,
      0,
      [
        "@query", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "e64bbafccaf77a5533b69394295f1cbd"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "5569ec0475a4f02cf202bb32814a7d42"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_lp2",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7f268c3987500a0b2d8132aef89ff22c",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_bef96b376eac7597d3b66f969135f633",
        "typing_Hacl.Spec.Poly1305.Vec.prime"
      ],
      0,
      "0313d256073a030359aacd4508bbb29b"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.paren_mul_right5",
      1,
      0,
      0,
      [
        "@query", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "69e13bb96ae6770af59662f53462d691"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "be289778b2d13461540ab2448ce8ede2"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp2",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "f2855d970d800af8e90aa42e6fe45bd7"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp1",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "df6bf8f690488c788561fa980af60374"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify_rp1",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "3ee633b5bbdd4cd57351785bf78414d6"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify",
      1,
      1,
      1,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul"
      ],
      0,
      "a27735b666376a3b5dd8098f5e298010"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2_simplify_lp",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "e2b8c6e931a2a46b53e1d68fe0fcecd9"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2_simplify_lp",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "e02a3e1ffe83a80664f1336071beda8d"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2_simplify_rp",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "7681360a5203fd1ef51bc163429d1970"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2_simplify_rp",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "228b4e809a16556ee25a85ab2a6dc697"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2_simplify",
      1,
      1,
      1,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul"
      ],
      0,
      "b0b937b7019a9e975b246159931d2009"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4_simplify_lp",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "1ad9dd55b6df01e52a3d4d4b366b602a"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4_simplify_lp",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "801634b7e0a9be3d638bc85914c59693"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.mul_distr_a_r_lemma",
      1,
      1,
      1,
      [
        "@query", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "0673ef736dc87e28de9930944fefd684"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4_simplify_rp",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "db56aafb3f2fa5de45d538b733d447da"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4_simplify_rp",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052"
      ],
      0,
      "d2bac2d227476f8ccad767fc3bda179b"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4_simplify",
      1,
      1,
      1,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfmul"
      ],
      0,
      "4f5052f23e5ca69c4191a37ebb0be585"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma1",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "f1cee4949ab2416c04348401d42672c7"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma1",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "945a57bf6cd0e13506e84dd16f17277f"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma1",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.compute_r1",
        "equation_Hacl.Spec.Poly1305.Vec.compute_rw",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem1",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_1",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Hacl.Spec.Poly1305.Vec.updaten",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_29886ea9d8a4b5deaee5f4e4824cfa0e",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d8d40ee35640d1efdf87cb52a275ab1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.updaten",
        "token_correspondence_Lib.Sequence.repeat_blocks_f",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Hacl.Spec.Poly1305.Vec.compute_r1",
        "typing_Hacl.Spec.Poly1305.Vec.compute_rw",
        "typing_Hacl.Spec.Poly1305.Vec.fmul",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.Sequence.create", "typing_Lib.Sequence.length",
        "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2",
        "typing_Prims.pow2", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "dffd4c4d84d5a7b9ff7aed37fabf09d8"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_7c273b71dc523e9869a90ca67dbe27f9",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "3c35c76a312868ece5e707c209b80a1d"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "73c849915bc5d655a0923462174f74bf"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma2",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.compute_r2",
        "equation_Hacl.Spec.Poly1305.Vec.compute_rw",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem2",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_2",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Hacl.Spec.Poly1305.Vec.updaten",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_11b3cf03e38e155f1eed89d08f3782c0",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7c273b71dc523e9869a90ca67dbe27f9",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a0f83ae4ab1305808612ac8e6ba3244d",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d75d61b582b9f5d9864c874910a7e7d0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f28f93ce590dd14a5cb9f67d5e00470f",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.updaten",
        "token_correspondence_Lib.Sequence.repeat_blocks_f",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.fmul",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.ByteSequence.nat_from_intseq_le",
        "typing_Lib.IntVector.create2", "typing_Lib.Sequence.create",
        "typing_Lib.Sequence.length", "typing_Lib.Sequence.map",
        "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub",
        "typing_Lib.Sequence.to_seq", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "b9297005607a4c2c2558504502ec2567"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ce23dd14fd756279ff8acff4b62d0e0c",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "29fdb0051a2ea0a9bbd4dadd0518360c"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.lemma_div_nat_is_nat",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "primitive_Prims.op_Division",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "176cc8ad079b5afe0c45964ba28c392e"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "0f18e090d622f9cf9a44b3df1bc31cc9"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_repeat_blocks_multi_lemma4",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.compute_r4",
        "equation_Hacl.Spec.Poly1305.Vec.compute_rw",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem4",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_4",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Hacl.Spec.Poly1305.Vec.updaten",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "interpretation_Tm_abs_222099de51c418a80a6c8a1acaa5a33c",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "lemma_Lib.IntTypes.pow2_2", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_45aa679e2920dae80de332edb44a5f88",
        "refinement_interpretation_Tm_refine_54186ae54e4390dc0622b822c9c26dfa",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5ac6ea56e3f7b7badd5e3c05da656d0d",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8a5abea94ad2813f2777736f2debe1bf",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_ce23dd14fd756279ff8acff4b62d0e0c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.updaten",
        "token_correspondence_Lib.Sequence.repeat_blocks_f",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Hacl.Spec.Poly1305.Vec.fmul",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.IntVector.create4", "typing_Lib.Sequence.create",
        "typing_Lib.Sequence.length", "typing_Lib.Sequence.map",
        "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "well-founded-ordering-on-nat"
      ],
      0,
      "2182b56e51d825c301d8511f1bd22c24"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.normalize_4_lemma",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "typing_Hacl.Spec.Poly1305.Vec.size_key"
      ],
      0,
      "7af335481d050f47803629677de1c83f"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.normalize_4_lemma",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "typing_Hacl.Spec.Poly1305.Vec.size_block"
      ],
      0,
      "fbd91ef31a99af8b8095e2221358130e"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.normalize_4_lemma",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_4",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "int_typing",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5ac6ea56e3f7b7badd5e3c05da656d0d",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v",
        "typing_Lib.IntVector.create4", "typing_Lib.Sequence.map2",
        "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "16676466512bc8f31fa432ce9ba9b515"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load1",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0715d2e4233dbcf29d6352f137ac893d",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "160553e79f8930b55d74dcba370ef008"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load1",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "3869b163fa00e1714547233ccc28d811"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load1",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc1",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem1",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_1",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0715d2e4233dbcf29d6352f137ac893d",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.Sequence.create", "typing_Lib.Sequence.map",
        "typing_Lib.Sequence.map2", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "9634b204cb4a5adc3a3a8cf8ba40bd7d"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Spec.AES.elem",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_81e45fceb6dc0c75f6d59946aa686c81",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v",
        "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "8f5c6826c1dd002be2429cfb8befa419"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf", "primitive_Prims.op_Multiply",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "174b1df14c28db84fd3429ca91ffb01a"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load2",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc2",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem2",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_2",
        "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.prime",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_81e45fceb6dc0c75f6d59946aa686c81",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a0f83ae4ab1305808612ac8e6ba3244d",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.IntVector.create2", "typing_Lib.Sequence.map",
        "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "759928c616103be2a1ef79de96b0229b"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_09630c7d170f75d893f43322b29ffb46",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_c1853d4b6fabf6b9c3640a456beaa249",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v",
        "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "837333c678cc579551864b68f0650fe6"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf", "primitive_Prims.op_Multiply",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "d44988469c404dfdff7f527329ec7073"
    ],
    [
      "Hacl.Spec.Poly1305.Equiv.Lemmas.poly_update_multi_lemma_load4",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Poly1305.Vec.elem",
        "equation_Hacl.Spec.Poly1305.Vec.fadd",
        "equation_Hacl.Spec.Poly1305.Vec.fmul",
        "equation_Hacl.Spec.Poly1305.Vec.lanes",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc",
        "equation_Hacl.Spec.Poly1305.Vec.load_acc4",
        "equation_Hacl.Spec.Poly1305.Vec.load_blocks",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem",
        "equation_Hacl.Spec.Poly1305.Vec.load_elem4",
        "equation_Hacl.Spec.Poly1305.Vec.normalize_4",
        "equation_Hacl.Spec.Poly1305.Vec.pfadd",
        "equation_Hacl.Spec.Poly1305.Vec.pfelem",
        "equation_Hacl.Spec.Poly1305.Vec.prime",
        "equation_Hacl.Spec.Poly1305.Vec.size_block",
        "equation_Hacl.Spec.Poly1305.Vec.size_key",
        "equation_Hacl.Spec.Poly1305.Vec.update1",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd",
        "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
        "lemma_Lib.IntTypes.pow2_2", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_09630c7d170f75d893f43322b29ffb46",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5ac6ea56e3f7b7badd5e3c05da656d0d",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
        "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
        "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
        "refinement_interpretation_Tm_refine_b0903b8d87e86a2787255a592ed4633c",
        "refinement_interpretation_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_c1853d4b6fabf6b9c3640a456beaa249",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd",
        "token_correspondence_Hacl.Spec.Poly1305.Vec.update1",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Hacl.Spec.Poly1305.Vec.load_blocks",
        "typing_Hacl.Spec.Poly1305.Vec.load_elem",
        "typing_Hacl.Spec.Poly1305.Vec.pfmul",
        "typing_Hacl.Spec.Poly1305.Vec.size_block",
        "typing_Hacl.Spec.Poly1305.Vec.size_key",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.ByteSequence.nat_from_intseq_le",
        "typing_Lib.IntVector.create4", "typing_Lib.Sequence.map",
        "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "c74041df12a40e0ae2c70ddbae013b39"
    ]
  ]
]