[
  "”'£_\nŽÆIDœ»Þ/JÎÛ",
  [
    [
      "Hacl.Spec.P256.bCoordinateP256",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "e45ccaf5e189d5da1209e11e58217e87"
    ],
    [
      "Hacl.Spec.P256.basePoint",
      1,
      0,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "b001e940e571a8df92d5cca8b1df9ab6"
    ],
    [
      "Hacl.Spec.P256._point_double",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.P256.Definitions.point_nat_prime",
        "equation_Hacl.Spec.P256.Definitions.prime256", "equation_Prims.nat",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_782879f3a1b84057df9d0b4b9925bdeb"
      ],
      0,
      "574c72a7c111a02ad9d36597e350665a"
    ],
    [
      "Hacl.Spec.P256._point_add",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.P256.Definitions.point_nat_prime",
        "equation_Hacl.Spec.P256.Definitions.prime256", "equation_Prims.nat",
        "int_typing", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_782879f3a1b84057df9d0b4b9925bdeb",
        "true_interp"
      ],
      0,
      "789fe4120a93e35eb2c354c71b083ec2"
    ],
    [
      "Hacl.Spec.P256._norm",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Hacl.Spec.P256.Definitions.prime256",
        "equation_Hacl.Spec.P256.Lemmas.modp_inv2_pow",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "4ec3c8443aafbbab167dc07e5195872a"
    ],
    [
      "Hacl.Spec.P256.scalar",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "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.U32@tok"
      ],
      0,
      "d1366bf57c6cab10457b7546bcb82eb1"
    ],
    [
      "Hacl.Spec.P256.ith_bit",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "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.U32@tok"
      ],
      0,
      "b62dc1abdd80f2bbf5585717c0151b9b"
    ],
    [
      "Hacl.Spec.P256.ith_bit",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "57819ee941f77b8e660cd818230d18fa"
    ],
    [
      "Hacl.Spec.P256._ml_step",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "687d30030ac585987dbc47ce45a79ef9"
    ],
    [
      "Hacl.Spec.P256.scalar_multiplication",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.P256.Definitions.prime256", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "typing_Hacl.Spec.P256.Definitions.prime256"
      ],
      0,
      "b012c3549094839f11efb2c2c1f11e1f"
    ],
    [
      "Hacl.Spec.P256.secret_to_public",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.P256.Definitions.prime256", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "typing_Hacl.Spec.P256.Definitions.prime256"
      ],
      0,
      "f406f8e8fdcd6ca8260cfb0069846b7c"
    ],
    [
      "Hacl.Spec.P256.isPointOnCurve",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "7bc476b62aa1db1d034531daffccb8fb"
    ],
    [
      "Hacl.Spec.P256.point_prime_to_coordinates",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "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.U32@tok"
      ],
      0,
      "f8b952e69f386e79f0a72168ba3ab677"
    ]
  ]
]