[
  "āŪZppAšKœ?¬ß'7a",
  [
    [
      "Spec.Poly1305.prime",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "da3b654b937bb6d79f8d4a8ef56211a5"
    ],
    [
      "Spec.Poly1305.fadd",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Poly1305.felem",
        "equation_Spec.Poly1305.prime", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Spec.Poly1305.prime"
      ],
      0,
      "c042db34391c9f9384f71258e8f8aa01"
    ],
    [
      "Spec.Poly1305.fmul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Poly1305.felem",
        "equation_Spec.Poly1305.prime", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Spec.Poly1305.prime"
      ],
      0,
      "3f6dca7c9a8682429ebfe497dce82be0"
    ],
    [
      "Spec.Poly1305.zero",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "equation_Spec.Poly1305.prime",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Spec.Poly1305.prime"
      ],
      0,
      "72d4feaf10be32ef8fb09f84f78cb2b2"
    ],
    [
      "Spec.Poly1305.size_block",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "62fc52b2ed00e43acef2b3449e88321b"
    ],
    [
      "Spec.Poly1305.size_key",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "57e1b348c84974876e4836f9a40d1a60"
    ],
    [
      "Spec.Poly1305.poly1305_encode_r",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_Spec.Poly1305.size_key",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "8976238c8d52bb9ead06a3b0a35482e8"
    ],
    [
      "Spec.Poly1305.poly1305_init",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
      ],
      0,
      "76ef93c03ece39af9714ee594fdd8e3f"
    ],
    [
      "Spec.Poly1305.encode",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Poly1305.size_block", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a7b50ae8c4d1ef81999174593660f8c",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "2411358cc8fdb0227a831422c8316c60"
    ],
    [
      "Spec.Poly1305.poly1305_finish",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.nonzero",
        "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key", "int_inversion",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5726018248762f1a50e71a8485d6d48d",
        "refinement_interpretation_Tm_refine_ca50ce86452a3257a9622c065c92c0e8",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
      ],
      0,
      "d94409355a8ea031cf163f06fb0f3225"
    ],
    [
      "Spec.Poly1305.poly1305_update_last",
      1,
      0,
      0,
      [ "@query", "equation_Spec.Poly1305.size_block" ],
      0,
      "f76e6c72bf3a9b4cfcf4d0a59e2a6cb3"
    ],
    [
      "Spec.Poly1305.poly1305_update",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "typing_Spec.Poly1305.size_key"
      ],
      0,
      "1ce509b2285dbf2dcd27c0ee413e15c0"
    ]
  ]
]