[
  "��ޤ���4��\u0010�%lQ",
  [
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "34aaabb1305089ea01985312096f505f"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a"
      ],
      0,
      "b3cac69484d9606f40e0f168e6593ef2"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a"
      ],
      0,
      "3224262566b42b187bf6015cf20fefc1"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__n",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "3f45fff40eced52ec4e5c2fda6544778"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__n",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len"
      ],
      0,
      "b9921bba94dd1ecd7c4539a58c1d567b"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__r2",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "bdf97e5c69f1092d48678e15e121fb56"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__r2",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len"
      ],
      0,
      "27c81d2c0d5b1b1ad1592d0af2ba9714"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.n",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "961d247b9e4341a47448fb979c345ab9"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.r2",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "632ab91e5e332813108102ac635f9d0d"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "data_elim_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "904d51346ea29719bae431867fdf645e"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "data_elim_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a"
      ],
      0,
      "4de38a7dddfac276998b89a16a868e07"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.mul_zero_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_62f21a2aa1a4ff46f503d4f6e27f44d2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "ffa97471c4ab6f11bfbf41ae74dfc5cb"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.mul_zero_lemma",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Math.Euclid.is_prime", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_62f21a2aa1a4ff46f503d4f6e27f44d2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "unit_inversion", "unit_typing"
      ],
      0,
      "4d7dcfc1eca2958062df82799f79cc3e"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.mul_nonzero_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_62f21a2aa1a4ff46f503d4f6e27f44d2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b0e54c4143de27918ff4de50b9f2c0f0"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.mul_nonzero_lemma",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "05497a7e11dc72494ef1792026b9be31"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.from_mont_lemma_nonzero",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b7e02982f0240b7dc3c4118cb320c96f"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.from_mont_lemma_nonzero",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Hacl.Spec.Montgomery.Lemmas.eea_pow2_odd_k.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Hacl.Spec.Montgomery.Lemmas.eea_pow2_odd",
        "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_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_4199ebae5488a1dfeef0878899049fb4",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Montgomery.Lemmas.eea_pow2_odd_k"
      ],
      0,
      "86f3d5c35ae1286c9a858ef8fbcc87f2"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_check_modulus",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b2eac54def372883a8849af3f005622b"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_check_modulus",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "db0ff2afd2a215c251c42bb72f7611d5"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_check_modulus",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.ones_v",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa",
        "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8f37d884d4222999b1ab57971267e3b4",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones",
        "typing_Lib.IntTypes.zeros", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "4056c0f1c8cf88a32810485eaa732eeb"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_init",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "cbc50ab730053413aed5eb776fbe5688"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_init",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "58d3b878c46830929df0f7cfed374cc6"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_init",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.Lib.bn_low_bound_bits",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_r2",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_r2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_85cd141032cfb24d8edfc54276e6af71",
        "refinement_interpretation_Tm_refine_8bfea23f1ac4519cc5286ee2c6bbe35a",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.Lib.bn_low_bound_bits",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "978d84fad821ed7832cbbd19e8dab196"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_to_field",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "0643e8a36fd30ce617296ca97c733565"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_to_field",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "a9aadd93cba86dff4f95f7697408c451"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_to_field",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1e04f03855bf169fd65abc6851182e30",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5a0f96da135e898a5c754cbda1ef84b8"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "b741b22b7bd5c65ab7487307699c1c0a"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1e04f03855bf169fd65abc6851182e30",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a433cf4830e5f5d1ca454fa0be52c6d5"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_from_to_field_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "37efb3967e0ee1c29500685d557da57d"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_from_to_field_lemma",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "606271fcd821e3ffe7e7bbd4344d0a91"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_from_to_field_lemma",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_to_field",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d63570a11c86d56384fb53501f78a2a4",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_to_field",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "c516395e9c18b38f9ada77d8367930d5"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_add",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "3c9c9621d3979eab2a1a45b9f81af4cf"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_add",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "primitive_Prims.op_Modulus",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "6e31f1b89bef1f3d088e4d30e8f1b227"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_sub",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "c5f1bceda28891222a3e9d2d7b90e6bc"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_sub",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "primitive_Prims.op_Modulus",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "19f70b4bc6b82384bbd86143deadb8d6"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_mul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "54618abe50a959b248b2b4d382a5dd87"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_mul",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_1e04f03855bf169fd65abc6851182e30",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "bbb4ddb8f27c751d7d68d55c3913169c"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_sqr",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "003fe50509e564f1c202f1ba5a57f100"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_sqr",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_1e04f03855bf169fd65abc6851182e30",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a6a30dbcf68ef958926975b0968c8a9e"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_one",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "1b40f9dcf4cf842f7a5a10560fe0355d"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_one",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.r2",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "interpretation_Tm_abs_5645c8794d28408b0c6572d64fec56ad",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_1e04f03855bf169fd65abc6851182e30",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "token_correspondence_Hacl.Spec.Bignum.MontArithmetic.r2",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "44a971f1268a16941382c914fabf1459"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_exp_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5a03c3b1eee50e9ccb63de23b5c0a957"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_exp_consttime",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a43f7a842966c805fcd804b83f9744d7"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_exp_consttime",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "cd76d157d8f334982d9405a8f798d41e"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_exp_vartime",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "df1193f5be17dae58888e3ff7b610d26"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_exp_vartime",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_mu",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_1cfe508ae739b6f52646dce85c33d61f",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Hacl.Spec.Bignum.MontArithmetic.bn_from_field",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4c0ea35d9cc3e10d974579f2007031a7"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_inv",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len"
      ],
      0,
      "76089f9c486c9de043dddbc5300bc03b"
    ],
    [
      "Hacl.Spec.Bignum.MontArithmetic.bn_field_inv",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Math.Euclid.is_prime",
        "equation_Hacl.Spec.Bignum.Definitions.blocks0",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre",
        "equation_Hacl.Spec.Bignum.MontArithmetic.bn_mont_nat",
        "equation_Hacl.Spec.Bignum.bn_len",
        "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_len",
        "proj_equation_Hacl.Spec.Bignum.MontArithmetic.Mkbn_mont_ctx_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0444e7862174b14c2a104f9d9c872350",
        "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_4fe9a5df27ca5859eef8add9fc6819fb",
        "refinement_interpretation_Tm_refine_51c595810418f4c2471ec34a247be192",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Hacl.Spec.Bignum.Definitions.blocks0",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__len",
        "typing_Hacl.Spec.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx__item__mu",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "dbd847bc8c2657a4bd1851d4bb399d59"
    ]
  ]
]