[
  "\u0000}!‘ƒ’‡0NM κߑʏ",
  [
    [
      "Hacl.Spec.P256.Normalisation.lemma_norm_as_specification",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Hacl.Spec.P256.Definitions.prime256",
        "equation_Hacl.Spec.P256.Normalisation.prime",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ae5bc5e47bcfeee1c1f1d89b14e02c69",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "6a680ad2a0a5213c3c164c0309f4aedb"
    ],
    [
      "Hacl.Spec.P256.Normalisation.lemma_norm_as_specification",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Hacl.Spec.P256.Definitions.prime256",
        "equation_Hacl.Spec.P256.Normalisation.prime",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ae5bc5e47bcfeee1c1f1d89b14e02c69",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "4587cdc09ce03fbe499a059b70b7615e"
    ],
    [
      "Hacl.Spec.P256.Normalisation.lemma_norm_as_specification",
      3,
      2,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Hacl.Spec.P256.Definitions.prime256",
        "equation_Hacl.Spec.P256.Lemmas.modp_inv2_pow",
        "equation_Hacl.Spec.P256.Normalisation.prime",
        "equation_Hacl.Spec.P256._norm",
        "equation_Hacl.Spec.P256.isPointAtInfinity",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_319ba7ad18b1e5c23f23d7c0009d178a",
        "refinement_interpretation_Tm_refine_3d1a5257640cdda8bf4067dc3d0753a2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ae5bc5e47bcfeee1c1f1d89b14e02c69",
        "refinement_interpretation_Tm_refine_bfc14a90c86084df96cf5d91e1a25040",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "b140a7624d7d87e93d5eea6b8ee851ef"
    ]
  ]
]