[
  "_%¥Íù‰Ê\u0019Ýú\u0004×Ã8âä",
  [
    [
      "Hacl.Spec.Bignum.Convert.bn_from_uint",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "214470c63c05b39416a347f14d53b182"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_uint",
      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_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", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "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"
      ],
      0,
      "5ab31c1455bb90f61d5d73a0ada7386b"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_uint_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "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.unsigned", "equation_Prims.pos",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "1656fa31bcde86b5a43b05023e6114f9"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_uint_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.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_uint",
        "equation_Hacl.Spec.Bignum.Definitions.bn_v",
        "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.uint64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.slice", "equation_Lib.Sequence.to_seq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_upd",
        "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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_01496a0cce63db36a137834bd6ec548b",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_348ce2a9b3a78cc1ebfb25f7b09df72a",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9bbf73467679375f43a0fe35bf576903",
        "refinement_interpretation_Tm_refine_a38b95dfec73eec9642ad5f2020d0cec",
        "refinement_interpretation_Tm_refine_a550f73e495a7bb5066bd3f10fa2f9fb",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d159fe5e58af2d5c150976d4684f3dc1",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d599c9bc2af511ab86ad43cbfdec5a92",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Lib.Sequence.index", "typing_Lib.Sequence.sub",
        "typing_Lib.Sequence.to_seq", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "8e499a68c4693d9f3fd3f41bdbaca378"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
      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.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "8575c5306ba0824f37f735f17fa79213"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "81feb46934368bdb9511e278dfaab421"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
      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",
        "disc_equation_Lib.IntTypes.U1", "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.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "47777e69b9ed9787ded693480fd10e99"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_",
      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.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "e910c62d84fbdb1f0f0dabfb91515535"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "5ccb0c7b4762c2f0e7a155fec6f69533"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "54caedf72926ba207864ff13159731ab"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "302c41c90d3d086ae192a5f0385e8a44"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_acd1484e3c6952e815159dcef873e23d",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d86144496814462c66a9358c7e148d74",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b92e2738ff73e8bb5bc32e4cc6dc85d8"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "23be83954252b6ab0f1b7388345187df"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "2ce7f019e807cff125a580e166121aa0"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a182e4b0356ed5104fcafdb8de0e5bc1",
        "refinement_interpretation_Tm_refine_a947d69c8ac83f2023f9c09849ee20e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d86144496814462c66a9358c7e148d74",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b406ec7df9ea7e2c0445d2efa7cffe43"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_f",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e8a06f9c88bd428da75ec2d2fae4eff6"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_f",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "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_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "16ad5df8fcaff9c8e66c1fb23422785a"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
      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.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "93c6f80ecc8e9a2cf28b79f5d61763f5"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
        "unit_typing"
      ],
      0,
      "32990ed4d417ff3af19f00d6a7287ee1"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f029aa92e7df29ca6d5bb14ad931b315"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "92a5b14029914a5730a639501956d0c1"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be",
      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.U16",
        "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.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c1c4eefab9148144b64824ab3360437e"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0f95961c1f4219b7e0715ad229a18d23"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "fa66a8e2e14160c4da2220c6ecaa2924"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a64028372aa1750805f94cfac8e63615"
    ],
    [
      "Hacl.Spec.Bignum.Convert.reverse",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "7d531a7941c74bcc2713950344839121"
    ],
    [
      "Hacl.Spec.Bignum.Convert.twice_reverse",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Hacl.Spec.Bignum.Convert_interpretation_Tm_arrow_eed71c227c77bdf6585b933fd7492ec5",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Convert.reverse",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Hacl.Spec.Bignum.Convert.reverse",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.Sequence.createi",
        "typing_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae"
      ],
      0,
      "ddeac676892012df8bdcc8efc49dbe0e"
    ],
    [
      "Hacl.Spec.Bignum.Convert.reverse_slice1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "457d5b22fd07a7992e099a26a296a278"
    ],
    [
      "Hacl.Spec.Bignum.Convert.reverse_slice1",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "1bb4e1a3c28a72241b3cb50ff9cd806c"
    ],
    [
      "Hacl.Spec.Bignum.Convert.reverse_slice1",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Hacl.Spec.Bignum.Convert_interpretation_Tm_arrow_eed71c227c77bdf6585b933fd7492ec5",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Convert.reverse",
        "equation_Hacl.Spec.Bignum.Definitions.lbignum",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06fe3070c602c55a1b3c1d362c165c0e",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_348ce2a9b3a78cc1ebfb25f7b09df72a",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
        "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Convert.reverse",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.Sequence.createi", "typing_Lib.Sequence.slice",
        "typing_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae"
      ],
      0,
      "8fa183c8639fb324564a176196c32366"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be_reverse",
      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",
        "disc_equation_Lib.IntTypes.U1", "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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "efe48c932443024b8d5c60925622f677"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be_reverse",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "ae3c85eb01d5c1ff1f2eaa67837bc087"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be_reverse",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Hacl.Spec.Bignum.Convert_interpretation_Tm_arrow_e9a9e4b7995a56cf320f05bdc2544c87",
        "Hacl.Spec.Bignum.Convert_interpretation_Tm_arrow_eed71c227c77bdf6585b933fd7492ec5",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
        "equation_Hacl.Spec.Bignum.Convert.reverse",
        "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.int_t",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "function_token_typing_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "token_correspondence_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_f",
        "typing_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.createi",
        "typing_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4c82bacceff51d489521305776c9b5e9"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_be_lemma",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "748cac5924021295613509da255b195e"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_be_lemma",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "26a299d0833ceb7b5954bf77c212651c"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_be_lemma",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Hacl.Spec.Bignum.Convert_interpretation_Tm_arrow_eed71c227c77bdf6585b933fd7492ec5",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_1",
        "binder_x_7e285ce37f54294648c0f7c99b9b7949_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.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Convert.reverse",
        "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.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.slice", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "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_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_1a9a556bf89e9fdd7f225a12a2db8186",
        "refinement_interpretation_Tm_refine_31f84d00e7d4b9b012962a7991e6a750",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_808130b1acb6c50ab7e7538fc44a7a2b",
        "refinement_interpretation_Tm_refine_a79dbc2755cff0c8930dc875f6899f72",
        "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
        "refinement_interpretation_Tm_refine_cd545b316516e7d3d96e036bd1a6f35b",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d1164283ccfcd64e5c4a03e57404f80c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Convert.reverse",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.ByteSequence.nat_from_intseq_be",
        "typing_Lib.Sequence.createi", "typing_Lib.Sequence.slice",
        "typing_Prims.pow2",
        "typing_Tm_abs_e9aa29b82b6f0dc989de47cc8f54bbae",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "e6973e90541e7aa7c18d1ad9c04910fb"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_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.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "2240b603078a737207c73f57687ffd7f"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_lemma_",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "d1ee165e93d9e35ed4584350fc4a0e0f"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_lemma_",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@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",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Convert.bn_from_bytes_be_",
        "typing_Hacl.Spec.Bignum.Convert.reverse",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f1a4c22c8b8099ac8530fd58566934e8"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_be_zeroes",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "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_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "70b71b780b764d4b8a10133d81fb6a1f"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_be_zeroes",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "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_5b7b02b472fd499c1d21e7dd96dd29b2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b248b2f38923f042ae3cf029427fb30c"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_be_zeroes",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_0",
        "binder_x_4087f3fe1be39a5c31013c62f06056e3_1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.slice", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8bafef160cbde7bbe7741fa9d7e95cc6",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_9e7b7ec534a2a9a23ec52880cc32ece2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.ByteSequence.nat_from_intseq_be",
        "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.sub", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U8@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "721d026cd206eb91dab7d06c6be91499"
    ],
    [
      "Hacl.Spec.Bignum.Convert.nat_from_bytes_be_eq_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Addition", "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_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e7cd5cdf4bff745818002e164455a7fe",
        "refinement_interpretation_Tm_refine_f3beb7d4cc0af0f21fb0073806e21865",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "28167f90bc31ef4dd99f7366989ee6e5"
    ],
    [
      "Hacl.Spec.Bignum.Convert.nat_from_bytes_be_eq_lemma",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.slice", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual", "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6f358e7b3448597ac8fda6ccad1ffbbd",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_bafcbd17cff205f275aeea14cd667bb2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e23532ddf6e6720ef7b5f88299cb5db0",
        "refinement_interpretation_Tm_refine_e715abb391c6e60e3492f2ceaa45146e",
        "refinement_interpretation_Tm_refine_e7cd5cdf4bff745818002e164455a7fe",
        "refinement_interpretation_Tm_refine_ef46de995d5b44bf8d6ffaeac5309411",
        "refinement_interpretation_Tm_refine_f3beb7d4cc0af0f21fb0073806e21865",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Lib.Sequence.slice", "typing_Lib.Sequence.sub",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "6b0ce1b6b6ed76f7a96341ea2be90585"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_lemma",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c52d47279c1481b191c3dd65c1d18114"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "686fe4cadb9c73909ddbfd156ca74def"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_lemma",
      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.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_bytes_be",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.ByteSequence.nat_from_bytes_be",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_acd1484e3c6952e815159dcef873e23d",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d86144496814462c66a9358c7e148d74",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "7eaf96141dd48401c72d4530578952a8"
    ],
    [
      "Hacl.Spec.Bignum.Convert.index_bn_to_bytes_be_",
      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",
        "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.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_311b12f7a3afbaea4c57b860c2e07c6f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "60b9894e2b4403bf60a830417177cc97"
    ],
    [
      "Hacl.Spec.Bignum.Convert.index_bn_to_bytes_be_",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
        "equation_Hacl.Spec.Bignum.Convert.bn_to_bytes_be_f",
        "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.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_08c36fa2492101a8fdef50ab40807141",
        "refinement_interpretation_Tm_refine_0906d1dba46b62e3be3cff2a84c635a0",
        "refinement_interpretation_Tm_refine_13b46e58046928c9b0446977a0e8ad2e",
        "refinement_interpretation_Tm_refine_311b12f7a3afbaea4c57b860c2e07c6f",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6995b0f4000fa0c5e6436e1dd45f3269",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b07203f29840a020412ed1886975c161",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
        "typing_Lib.ByteSequence.uint_to_bytes_be",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "6953505ec5df7cb57688ea2d4ae7a887"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_aux",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_311b12f7a3afbaea4c57b860c2e07c6f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0228fd41ec6a74e858265a520d166c13"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_aux",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "0433ababcbda85c22ed16102b06e726a"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_aux",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_311b12f7a3afbaea4c57b860c2e07c6f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "9f6efdd9d87d38f7d0403f5d59059930"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4bbefd38ef1a9da1a498242ba98c9109",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "61f9cf398f6d0307866a3bc2a48a024c"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_",
      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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92"
      ],
      0,
      "bc648b0ae3adbbc7953593fd121c40c9"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma_",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_to_bytes_be_",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_296d49113526e4fc6bdaf262a385572a",
        "refinement_interpretation_Tm_refine_311b12f7a3afbaea4c57b860c2e07c6f",
        "refinement_interpretation_Tm_refine_32a7d823fc1e44d6f86f842a17182e57",
        "refinement_interpretation_Tm_refine_4bbefd38ef1a9da1a498242ba98c9109",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a3c2ca184063999da0d4361288c72e7b",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_c4db1a5e792081301f1c5eb4ed90971e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "5222da5adb1d82c21bfa53975b3c2d7e"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "refinement_interpretation_Tm_refine_ec2f0d9a9b311ef993ed9a9872822f28",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c11fd4082d4c071e3c36534968adebb3"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "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", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "22ad01c6d9b4dbe42397e454977b91ab"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_be_lemma",
      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.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_to_bytes_be",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "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.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0b535b8a3ed409a556a37e9d8df09da4",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_3e4031b9fc47bcb302a7d1ea6536e9f4",
        "refinement_interpretation_Tm_refine_450c5fab5899e44e63db869bd0c9eec0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_85398722b10b20c2cf4b6eaeb54ec9a8",
        "refinement_interpretation_Tm_refine_8c0e9cb74ff385e290037f6464732ec2",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_be9f3762ef829e4292fadae5bee9b36d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_ce9e89c38e60c2d05a21867d34d2a76a",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "refinement_interpretation_Tm_refine_ec2f0d9a9b311ef993ed9a9872822f28",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.ByteSequence.nat_to_intseq_be",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b6654a555851ab82b6ecc340385c5c5d"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "165c350982ccec06486d48d3705a72b7"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9c22255db31e0d833d312e8ba3f7b895"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_1",
        "binder_x_7e285ce37f54294648c0f7c99b9b7949_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.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.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "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_11fa0c41a6e2f11d06ba88a42e633e11",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_1a9a556bf89e9fdd7f225a12a2db8186",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_31f84d00e7d4b9b012962a7991e6a750",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_808130b1acb6c50ab7e7538fc44a7a2b",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d1164283ccfcd64e5c4a03e57404f80c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.nat_from_intseq_le",
        "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "0c275ee4c9767df712da16a7187f6b2b"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_le_zeroes",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "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_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "db7fca3629de9ad1f84853635ae4bbaf"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_le_zeroes",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "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_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b8fca6e3a2d99cec05db464193eec66f",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "3db3f62363ad40a0aa07f22f2735308d"
    ],
    [
      "Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_le_zeroes",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_0",
        "binder_x_4087f3fe1be39a5c31013c62f06056e3_1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.slice", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8bafef160cbde7bbe7741fa9d7e95cc6",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_9e7b7ec534a2a9a23ec52880cc32ece2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.ByteSequence.nat_from_intseq_le",
        "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.sub", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U8@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "7157fac43da7f2ea54adbfc6f3620e10"
    ],
    [
      "Hacl.Spec.Bignum.Convert.nat_from_bytes_le_eq_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Addition", "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_681a5ef0c96e958fbba4137a5fd38818",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f3beb7d4cc0af0f21fb0073806e21865",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "f3b9e72f617903fa679a910739412e58"
    ],
    [
      "Hacl.Spec.Bignum.Convert.nat_from_bytes_le_eq_lemma",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.slice",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_2057733be200c152a41705bd9fd424a6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_681a5ef0c96e958fbba4137a5fd38818",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_79427c29def4ecc8bbe088cdf2c4b729",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_dd83838b7d08260c0e5559d3737ba703",
        "refinement_interpretation_Tm_refine_eda4c60bfc6ed54661bae4c687abf48b",
        "refinement_interpretation_Tm_refine_ee8afbb4a53ba47763b3b9e2af44f2cb",
        "refinement_interpretation_Tm_refine_ef46de995d5b44bf8d6ffaeac5309411",
        "refinement_interpretation_Tm_refine_f3beb7d4cc0af0f21fb0073806e21865",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.slice",
        "typing_Lib.Sequence.sub", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "06972c2b9ba32d4396813e79da305f72"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_lemma",
      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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b1e5c9824b2bfdcce8b6cd97908ea6cb"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b0a5c7ea1a68ffbaa9dcfed82a6ea29b"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_lemma",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_bytes_le",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a182e4b0356ed5104fcafdb8de0e5bc1",
        "refinement_interpretation_Tm_refine_a947d69c8ac83f2023f9c09849ee20e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d86144496814462c66a9358c7e148d74",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "89f7bb460afd7646d53c8f5b32f32be2"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le_lemma",
      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",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "refinement_interpretation_Tm_refine_ec2f0d9a9b311ef993ed9a9872822f28",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "8fd7c281e57923837078f9e6ef8c4103"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le_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.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "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", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "9deccab1449d5f9fc7f35fc66cc8623f"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_to_bytes_le_lemma",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_to_bytes_le",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "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.ByteSequence.nat_to_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_16af63ffd2c44e2ad56d8a6f61747579",
        "refinement_interpretation_Tm_refine_2196484e7ee5e6900b19fbaf8536cbec",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_be9f3762ef829e4292fadae5bee9b36d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e282b29344537850ca65fa1e83db32c1",
        "refinement_interpretation_Tm_refine_ec2f0d9a9b311ef993ed9a9872822f28",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "refinement_interpretation_Tm_refine_fddad6074c6981c4381d05c86ab29274",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.blocks",
        "typing_Hacl.Spec.Bignum.Definitions.bn_v",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "fbb1b7bb221c9bcffebeb1da875bd008"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_is_uints_from_bytes_le",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7001c85ff932b362e4f84d0aa016ae20",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c17e4c3cf1366351feb9c547f55f5a62"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_is_uints_from_bytes_le",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a746eff463a44a5593f7758c6c7e3026"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_le_is_uints_from_bytes_le",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Convert.bn_from_bytes_le",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "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.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7001c85ff932b362e4f84d0aa016ae20",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Definitions.blocks",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.IntTypes.numbytes", "typing_Lib.Sequence.create",
        "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "4b4ec5e97a67181513d188a3e282a128"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "equation_Hacl.Spec.Bignum.Definitions.limb_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_48109e3830d3ffed3ab6a6ee83783955",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7001c85ff932b362e4f84d0aa016ae20",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.create",
        "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "14ee31948b376af570e23dbc3cbb7bcc"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be",
      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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "52bbdba4479ff650be629024123ae62e"
    ],
    [
      "Hacl.Spec.Bignum.Convert.bn_from_bytes_be_is_uints_from_bytes_be",
      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",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Spec.Bignum.Definitions.blocks",
        "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.int_t",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7001c85ff932b362e4f84d0aa016ae20",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
        "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Spec.Bignum.Convert.reverse",
        "typing_Hacl.Spec.Bignum.Definitions.blocks",
        "typing_Hacl.Spec.Bignum.Definitions.limb",
        "typing_Lib.ByteSequence.uints_from_bytes_be",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "4aa18fde870a9489a7944c228c691547"
    ]
  ]
]