[
  "@d]���-��w���fn�",
  [
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_reduction",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b71e52f06a7beb3c8539952a8b2eb571"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "f4a24ac8181f09b9f58b21e13d06eb56"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_sqr",
      1,
      0,
      0,
      [
        "@query", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "53f3eb975a4504ba18cc33427241b6a0"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.lemma_fits_c_lt_rr",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "fc53a776aa4f781f36b934ecf49040b7"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.lemma_fits_c_lt_rr",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b32d00e531b361bf4a06e11c7c42c948"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_reduction_lemma",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "f2e922e952eda11df9a7b2e85d34214a"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_reduction_lemma",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_reduction",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1b0bf9a33998bf6b68d869d3a41516d5"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul_lemma",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "6a9b5f2e6b902d4175762fedf072d174"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul_lemma",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "5ccf59674a9fa982030f06c93ce55e8d"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul_is_mont_mul_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "80da607c99efb588e117df593208cd55"
    ],
    [
      "Hacl.Spec.AlmostMontgomery.Lemmas.almost_mont_mul_is_mont_mul_lemma",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "e6436af94e92d9a01006c65e2831a7f9"
    ]
  ]
]