[
  "6³¤ —ð±\u0016\u0019\r¬:läè¼",
  [
    [
      "Vale.Curve25519.X64.FastSqr.va_lemma_Fast_sqr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "34e82e759f6a24ea2b1bb0ec24af574c"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_wp_Fast_sqr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c7cdb4adc8b68b4b7f37febd634ae5b8"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_quick_Fast_sqr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "266860161f9ed792542c8d6eeb6dacb2"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_lemma_Fast_sqr_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_083efce99383e0ba0f00342643a9ae85",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "f3192f3fdf11177e25f6fdae587c97e6"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_wp_Fast_sqr_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,
      "94ff5fdbcffde9e0b09e68964196b923"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_quick_Fast_sqr_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "331ed9685290d9e3a4528404f6dd5c39"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_lemma_Sqr2_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_448d78f6e32281845737f788a930b91a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "86f5f8d1abef2f3adc24702526aa4cbf"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_wp_Sqr2_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,
      "9534c9641121b88e32cea0cb99fbb3eb"
    ],
    [
      "Vale.Curve25519.X64.FastSqr.va_quick_Sqr2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "fb20a62a5cf7cc9ac6b87c344173aaf0"
    ]
  ]
]