[
  "Èâ+\u000e¡»1)®§äìNš=‹",
  [
    [
      "Vale.Curve25519.X64.FastMul.va_lemma_Fast_multiply",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "dbb2e96844a3a5bf8ba00118d67e66a8"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_wp_Fast_multiply",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "cbb9fdfdc6047a40b72dafbd3efe6993"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_quick_Fast_multiply",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "fde42886fad3aba948ad2b9165077578"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_lemma_Fast_mul_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2111fb9198de365561cfa31855f8c970",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "4b0baa05298e7c082aa0bd141d1e3b42"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_wp_Fast_mul_stdcall",
      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,
      "14f262a6a6a08ecc4f90118d60a295f6"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_quick_Fast_mul_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "d33a5522c4469755704953cc41bd7c6a"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_lemma_Fast_mul2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "refinement_interpretation_Tm_refine_12858e97eec0ea4a967ef81772c81ae1"
      ],
      0,
      "b77f2e989df04bd9556d7c50ed6f6c98"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_wp_Fast_mul2_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d29d4f69658d1aaa35dc68316eda5afc"
    ],
    [
      "Vale.Curve25519.X64.FastMul.va_quick_Fast_mul2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "473a178f61ad5391b3339806e5a28894"
    ]
  ]
]