[
  "¤·J9S\u001aÀ\u001b)\u0014\u001aE­­Á‰",
  [
    [
      "Hacl.Spec.FFDHE.Lemmas.ffdhe_p_lemma_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Lib.Sequence.lseq",
        "equation_Spec.FFDHE.ffdhe_params_2048",
        "equation_Spec.FFDHE.ffdhe_params_3072",
        "equation_Spec.FFDHE.ffdhe_params_4096",
        "equation_Spec.FFDHE.ffdhe_params_6144",
        "equation_Spec.FFDHE.ffdhe_params_8192",
        "equation_Spec.FFDHE.get_ffdhe_params",
        "fuel_guarded_inversion_Spec.FFDHE.ffdhe_params_t",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p",
        "typing_Spec.FFDHE.get_ffdhe_params"
      ],
      0,
      "be90b30309ab6b5f4a317f953717830c"
    ],
    [
      "Hacl.Spec.FFDHE.Lemmas.ffdhe_p_lemma_len",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Spec.FFDHE.FFDHE2048",
        "constructor_distinct_Spec.FFDHE.FFDHE3072",
        "constructor_distinct_Spec.FFDHE.FFDHE4096",
        "constructor_distinct_Spec.FFDHE.FFDHE6144",
        "constructor_distinct_Spec.FFDHE.FFDHE8192",
        "disc_equation_Spec.FFDHE.FFDHE2048",
        "disc_equation_Spec.FFDHE.FFDHE3072",
        "disc_equation_Spec.FFDHE.FFDHE4096",
        "disc_equation_Spec.FFDHE.FFDHE6144",
        "disc_equation_Spec.FFDHE.FFDHE8192",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.FFDHE.FFDHE2048@tok",
        "equality_tok_Spec.FFDHE.FFDHE3072@tok",
        "equality_tok_Spec.FFDHE.FFDHE4096@tok",
        "equality_tok_Spec.FFDHE.FFDHE6144@tok",
        "equality_tok_Spec.FFDHE.FFDHE8192@tok",
        "equation_FStar.List.Tot.Properties.llist",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Spec.FFDHE.ffdhe_p2048", "equation_Spec.FFDHE.ffdhe_p3072",
        "equation_Spec.FFDHE.ffdhe_p4096", "equation_Spec.FFDHE.ffdhe_p6144",
        "equation_Spec.FFDHE.ffdhe_p8192",
        "equation_Spec.FFDHE.ffdhe_params_2048",
        "equation_Spec.FFDHE.ffdhe_params_3072",
        "equation_Spec.FFDHE.ffdhe_params_4096",
        "equation_Spec.FFDHE.ffdhe_params_6144",
        "equation_Spec.FFDHE.ffdhe_params_8192",
        "equation_Spec.FFDHE.get_ffdhe_params",
        "fuel_guarded_inversion_Spec.FFDHE.ffdhe_alg",
        "function_token_typing_Lib.IntTypes.byte_t", "int_typing",
        "inversion-interp",
        "lemma_FStar.Seq.Properties.lemma_seq_of_list_index",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p",
        "projection_inverse_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "refinement_interpretation_Tm_refine_0794011d44001b1fec89e9552f792160",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_841e96a5a013474304a287d636ebc350",
        "refinement_interpretation_Tm_refine_bc9f290f5345422bd1514cc244788d51",
        "refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e",
        "refinement_interpretation_Tm_refine_c1845bbdf525b18324aa6d5e25176918",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e3af2d5d78d277f78a448ebd4e018881",
        "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
        "typing_Lib.IntTypes.bits",
        "typing_Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p_len",
        "typing_Spec.FFDHE.get_ffdhe_params",
        "typing_Spec.FFDHE.list_ffdhe_p2048",
        "typing_Spec.FFDHE.list_ffdhe_p3072",
        "typing_Spec.FFDHE.list_ffdhe_p4096",
        "typing_Spec.FFDHE.list_ffdhe_p6144",
        "typing_Spec.FFDHE.list_ffdhe_p8192",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.FFDHE.FFDHE2048@tok",
        "typing_tok_Spec.FFDHE.FFDHE3072@tok",
        "typing_tok_Spec.FFDHE.FFDHE4096@tok"
      ],
      0,
      "7c4f39b309003cb62756ec3b46044b32"
    ],
    [
      "Hacl.Spec.FFDHE.Lemmas.pow2_lt_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "38602757b015907118015154aab515a8"
    ],
    [
      "Hacl.Spec.FFDHE.Lemmas.pow2_lt_len",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "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_Minus", "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_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Prims.pow2"
      ],
      0,
      "ba64a50120d3f3d383db8c2e2854f31c"
    ],
    [
      "Hacl.Spec.FFDHE.Lemmas.ffdhe_p_bits_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.FFDHE.ffdhe_len", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ca2354151d9f95e5892dc0437ed6052b",
        "typing_Spec.FFDHE.ffdhe_len"
      ],
      0,
      "2d277350635051b24f3f9b0da9351cef"
    ],
    [
      "Hacl.Spec.FFDHE.Lemmas.ffdhe_p_bits_lemma",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.ByteSequence.nat_from_bytes_be",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.slice", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.FFDHE.ffdhe_len",
        "equation_Spec.FFDHE.ffdhe_params_2048",
        "equation_Spec.FFDHE.ffdhe_params_3072",
        "equation_Spec.FFDHE.ffdhe_params_4096",
        "equation_Spec.FFDHE.ffdhe_params_6144",
        "equation_Spec.FFDHE.ffdhe_params_8192",
        "equation_Spec.FFDHE.get_ffdhe_params",
        "fuel_guarded_inversion_Spec.FFDHE.ffdhe_params_t",
        "function_token_typing_Lib.IntTypes.byte_t", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt8.vu_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p",
        "proj_equation_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.FFDHE.Mk_ffdhe_params_ffdhe_p_len",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "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_9e7b7ec534a2a9a23ec52880cc32ece2",
        "refinement_interpretation_Tm_refine_a769cf2126378855a0f7a809f308c2b7",
        "refinement_interpretation_Tm_refine_ac361b132c26d906d5997e1372d2a888",
        "refinement_interpretation_Tm_refine_b72bccd166def05aa28bd2e7acbc5f74",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_fedc659840bef2cd5b60437a973e1bda",
        "typing_FStar.UInt.fits", "typing_FStar.UInt8.v",
        "typing_Lib.IntTypes.maxint", "typing_Lib.Sequence.slice",
        "typing_Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p",
        "typing_Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p_len",
        "typing_Spec.FFDHE.ffdhe_len", "typing_Spec.FFDHE.get_ffdhe_params",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "d893a183cd7267c09764e0944e783cf0"
    ]
  ]
]