[
  "@�\"\u0014��&m<\u0017�5\u0010��S",
  [
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "typing_Spec.P256.Definitions.prime256"
      ],
      0,
      "29daca9507bdd627c525aa82f9ba2d17"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "da28f6dd1e6ed70a952ac83e8dd9f12a"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double",
        "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_8807a8a6db5cf1a86cc29f7b64a93885",
        "refinement_interpretation_Tm_refine_93e2420a1bc2654a04bc10881f331e3b",
        "refinement_interpretation_Tm_refine_a92851949b382679e8dc999df60d181e"
      ],
      0,
      "e1ef097de3e55c2cca36fa654d0eb4b3"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "7bb6654e41690119d3f164f1846ea4ad"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "dc9471f7cbdcd16dc427c7173af0d490"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double", "int_typing",
        "lemma_Spec.P256.MontgomeryMultiplication.lemmaToDomainAndBackIsTheSame",
        "primitive_Prims.op_Modulus", "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_a92851949b382679e8dc999df60d181e",
        "refinement_interpretation_Tm_refine_a9a8ee103221296ed130a43a8be51fb9",
        "refinement_interpretation_Tm_refine_ac652f9023b70de96af3f923ebf68db3",
        "refinement_interpretation_Tm_refine_cf60fc7ec5c165f556fc4bba108ab85b",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "9f68781c33c06495f8a88c80c3555ea3"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "ca9dda96abd8a50d3b4802c117e61192"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "bda35c403a628ead06a4e9881f51ec7b"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_4429a03440a4f885fdd4b2268b6cb06f"
      ],
      0,
      "812add578385ab64ec33b1d7e63850ee"
    ]
  ]
]