[
  "{ð½qÄû&KÌ%wÃw/\"Å",
  [
    [
      "Hacl.Spec.Curve25519.Field51.Definition.s64x5",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64",
        "refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923"
      ],
      0,
      "4c6d63b98d5b60dd357ad1b709c2ebe5"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.s128x5",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale128",
        "refinement_interpretation_Tm_refine_53e76104623db325c3ccc5c7426058ab"
      ],
      0,
      "933ff5d73ff83f7fff7dd436fe62f7c2"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.op_Plus_Star",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d3da3706507e66b178681f94a2370dcf"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.op_Star_Star",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7a043aebaeb843296eb998eb481f528f"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.lemma_mul_le_scale64",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "b8fd9ba0ca397d61c60f94b2ecf7b19a"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.op_Star_Hat",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64_5",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_663c12b322f48469426a5b8197cd0ebb",
        "refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923"
      ],
      0,
      "43af9a9d5394ab4ee4f1ace7ae2a9c47"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.pow51",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "6983cfb6d2af73ba6d97a09e9bfca918"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.mask51",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "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.U64@tok"
      ],
      0,
      "b4250dc42bf1cee4cacfea2bd83d7d04"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "e3693315d93d72b4af4b76c88e8240f6"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.felem_wide_fits1",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "53532ea1555228e143343ac7dd7a6dbc"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64_5",
        "equation_Prims.nat",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_663c12b322f48469426a5b8197cd0ebb"
      ],
      0,
      "4ea0b79486debc5c6b596122f0b54cdc"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.felem_wide_fits5",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale128_5",
        "equation_Prims.nat",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_3781545d89a72c1167cd3e7b244dbf3c"
      ],
      0,
      "65824be65746e13cffdd4c1eb34ee277"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.as_nat5",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@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_with_fuel_Prims.pow2.fuel_instrumented", "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_4ae12848fac0601da6605bac9d6872f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "846e20be6a336999e30454a9d2705340"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.wide_as_nat5",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4b944ca09ad96bece941715cac814505",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51"
      ],
      0,
      "aeb016b42891925e80f883a862011795"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.feval",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "cc714d670cf1c161cca0c9db9deb1012"
    ],
    [
      "Hacl.Spec.Curve25519.Field51.Definition.feval_wide",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "589f15422adff58b4886548131182b6a"
    ]
  ]
]