[
  "ËŠ°Ê¡}k±M»\u001d\u0018¡—@$",
  [
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1",
      1,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "1b012e59ce4ee8140cd7fe85113c90e1"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place",
      1,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "10d706d3b739152bc1d3c0ce9169a1f7"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lshift_add",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f0c1b717dfabcacea22f6db20f96ff8e"
      ],
      0,
      "ae87fd57015abeef979867f45aa5fd46"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "1e16aafe171b84609329c4d64679a102"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "7f133ae93c7d3a4d656c6a9389044547"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "2bbe3a263542d635793a25e577d0bb54"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "9f921f4d3c58caa21be87441824fb536"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul",
      2,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "04dcee706ca4fb3c39b068932c182e21"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop_step",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.Sequence.length",
        "equation_Prims.pos", "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_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4514f4fdf60106c55d2be5c3943f2ee7",
        "refinement_interpretation_Tm_refine_584ed023d00656e213ffb78ffdf829f6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "e0159ca224918961c93a856f5983043d"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop_step",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "2c2cdb5991aecf7b0a363914259bad4f"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop_step",
      3,
      0,
      0,
      [
        "@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.Multiplication.bn_mul1_f",
        "equation_Hacl.Spec.Lib.generate_elem_f",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "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_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4514f4fdf60106c55d2be5c3943f2ee7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_584ed023d00656e213ffb78ffdf829f6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "token_correspondence_Hacl.Spec.Bignum.Multiplication.bn_mul1_f",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "be81882a95cb7f71b9ff92ad3a07fb5d"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop",
      1,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_663ea0dfb2f44ae8d955d7deb432232c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "6e543fd3758c08eeb59325486bc305ef"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop",
      2,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_663ea0dfb2f44ae8d955d7deb432232c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a302be5c5c9af771174f2f6e572a51dc",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "beb31b880e14e7061b935ee5b05cc7b1"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma_loop",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_1",
        "binder_x_42b72a46b729884521de5402f51cda8a_4",
        "binder_x_841b4d802a58cc8b28cf8b35864b4d5d_0",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals",
        "equation_Prims.pos",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "refinement_interpretation_Tm_refine_004f8090c545047f856b534616ae8c79",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9f4007ee28fa89eb3ed7cd65ab92f56a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d9c68450036cfcd30491648c836062e7",
        "refinement_interpretation_Tm_refine_e3ffbb6d51068408d3995caf3ac2bc05",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U64@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "fec798f64f6c0a6f50ae834b33cc74b5"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "ef3895d0fba521344b1879d0a86f4326"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma",
      2,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Multiplication.bn_mul1"
      ],
      0,
      "9e460ec3534dd3ae7328bfd8d88179a0"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop_step",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.Sequence.length",
        "equation_Prims.pos", "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_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4514f4fdf60106c55d2be5c3943f2ee7",
        "refinement_interpretation_Tm_refine_584ed023d00656e213ffb78ffdf829f6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "7c52369884e426b215cca85679f7ddd4"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop_step",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "4698c50a4d77b42887bbda01e05074e7"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop_step",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Hacl.Spec.Bignum.Definitions.eval_.fuel_instrumented",
        "@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.Multiplication.bn_mul1_add_in_place_f",
        "equation_Hacl.Spec.Lib.generate_elem_f",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "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_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4514f4fdf60106c55d2be5c3943f2ee7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_584ed023d00656e213ffb78ffdf829f6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "token_correspondence_Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_f",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "224211fc301080c8f86788853c97db28"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop",
      1,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_663ea0dfb2f44ae8d955d7deb432232c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "6378c5b6009b03610eb6026c0e831b0a"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop",
      2,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_663ea0dfb2f44ae8d955d7deb432232c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_ea8209f65df1288bfc53fe85f187a3fb",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "0e02966d77597bf070540359ee19a22d"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma_loop",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_1",
        "binder_x_42b72a46b729884521de5402f51cda8a_5",
        "binder_x_69ada7bcf4dba8a70008ac2bf509ddb3_3",
        "binder_x_841b4d802a58cc8b28cf8b35864b4d5d_0",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "refinement_interpretation_Tm_refine_004f8090c545047f856b534616ae8c79",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4d95e1b0ca9124f6c7f0e5718aeb3d16",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9f4007ee28fa89eb3ed7cd65ab92f56a",
        "refinement_interpretation_Tm_refine_ac1e44c425d1973c0da36658a73ff529",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "a521da50f625490ffded31fc3093e43b"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "88cebbcd76ea71f447590a5ec9d9bfda"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place_lemma",
      2,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Multiplication.bn_mul1_add_in_place"
      ],
      0,
      "2a5848c57db448383c0bb114aa0dd2c4"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lshift_add_lemma",
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c32b5d96e64f338ccf7fe51701c1a8da",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f0c1b717dfabcacea22f6db20f96ff8e",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "dfdd3db891314a57af68a4bcdb291ad8"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul1_lshift_add_lemma",
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@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.Multiplication.bn_mul1_lshift_add",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.slice",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_1737a1740ceb05f475db45cf0fa7f5c1",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_66b55347eadd8366d826283c3e00cf22",
        "refinement_interpretation_Tm_refine_6a3903a652e3dfee4e5c61bea7ea284a",
        "refinement_interpretation_Tm_refine_715b076d848c5595796a961e6d95e0cc",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_837bca83cb16efa663cc2f96712f7df8",
        "refinement_interpretation_Tm_refine_92a82301be21e35f901951b25f6d260a",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f0c1b717dfabcacea22f6db20f96ff8e",
        "refinement_interpretation_Tm_refine_f201e7203460cea479218a2cb8e8f122",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "refinement_interpretation_Tm_refine_fa438d772cecc8ffd789a21cf0813c57",
        "refinement_interpretation_Tm_refine_fb72e214ecde26316ea317d73133c626",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.slice",
        "typing_Lib.Sequence.sub", "typing_Lib.Sequence.to_seq",
        "typing_Lib.Sequence.update_sub", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d031eda574df41031619ad3c91af2c81"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_lemma_",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "43d4e498938c2cb8130b820b5cd71caf"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_lemma_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "57fec37c0068d509eaf3d7ffa012f5cf"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_lemma_",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Multiplication.bn_mul_",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Properties.slice_upd",
        "primitive_Prims.op_Addition", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d2ca91f0561922dd196ac248dd665a0",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "6ca88c38072f2dae4e4406565bb38152"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma_step",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "bc2e627ef214a04d80e2e9a6f320e59e"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma_step",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "8c4764ce86de9a7cb716e74c5399a785"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma_step",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Hacl.Spec.Bignum.Definitions.eval_.fuel_instrumented",
        "@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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@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_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", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_07295705544891065e7a01d318c0ba51",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.Spec.Bignum.Definitions.bn_v",
        "typing_Hacl.Spec.Bignum.Definitions.eval_",
        "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.v",
        "typing_Lib.Sequence.index", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "a57368822488bc3c6019c5e2724a229b"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma",
      1,
      0,
      0,
      [
        "@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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "c79ea79e001e067491d7d26118b11052"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma",
      2,
      0,
      0,
      [
        "@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.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5901beb867a9e2e15326f3d8167d3b30",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "8d1c8627089f86ff157b36958a85f0ca"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_loop_lemma",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_0f1bb649b46bc5a3984d220fa96c604e_5",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_1",
        "binder_x_16801ebb32b1e68147451c80e7546dad_2",
        "binder_x_841b4d802a58cc8b28cf8b35864b4d5d_0",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_12cdd001288db6dd02d7cb55eb77c087",
        "refinement_interpretation_Tm_refine_44f85982d07bfcb740bf51044d331658",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U64@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "bd0d3b8eef61db6ca851f4223ac59df8"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
      ],
      0,
      "4d459be1f13b9d55b94618b6c0399795"
    ],
    [
      "Hacl.Spec.Bignum.Multiplication.bn_mul_lemma",
      2,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "equation_Hacl.Spec.Bignum.Multiplication.bn_mul",
        "primitive_Prims.op_Addition"
      ],
      0,
      "e787301ac7631dc2ff977f1c5cbe29ec"
    ]
  ]
]