[
  "\b\r ˜ÁþYÑÐCÔpS1Š(",
  [
    [
      "Vale.Poly1305.X64.va_req_Poly1305",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "2919507af3a11a997a5ee942e75e9fa6"
    ],
    [
      "Vale.Poly1305.X64.va_ens_Poly1305",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "unit_typing"
      ],
      0,
      "7faf62828ba945fc4cb392450ff20f79"
    ],
    [
      "Vale.Poly1305.X64.va_lemma_Poly1305",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Poly1305.Util.readable_words",
        "equation_Vale.Poly1305.Util.validSrcAddrs64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6688d8d4d0a4ee4e5fc12d9bf7990aa3",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "81cb1e6c7eb909de48d945ad3a90bd2a"
    ],
    [
      "Vale.Poly1305.X64.va_wp_Poly1305",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "4a6cf7cb6c7fd4ba13ef7653b16502a2"
    ],
    [
      "Vale.Poly1305.X64.va_quick_Poly1305",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "158833b38ccfc912f047cb42fea0c820"
    ]
  ]
]