[
  "\u0006�D��@NO� �� \u0003��",
  [
    [
      "Hacl.GenericField64.field_modulus_check",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Hacl.Spec.Bignum.Definitions.limb",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "8c3be6421d1ed0fcaea537a54939ace3"
    ],
    [
      "Hacl.GenericField64.field_init",
      1,
      0,
      0,
      [
        "@query", "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "8e3fa48ea745d0c7ded76f208b3b3d1f"
    ],
    [
      "Hacl.GenericField64.to_field",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_9509bf3bc0ef95ab26d2deef3178a6bf",
        "refinement_interpretation_Tm_refine_955e684da9470ec36ae4a7ab0b6c3de6",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "8f1c6c8ec3c32d808c6e15715c253f4d"
    ],
    [
      "Hacl.GenericField64.from_field",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_006817e69d7826ffee6a8d38339eae32",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_c50ffba077112288eace58db3621fa39",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "51faca97501c06e3c167eecbd0775a11"
    ],
    [
      "Hacl.GenericField64.add",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ac5a0d7c1535726b6b58566ff42fe21a",
        "refinement_interpretation_Tm_refine_b384fe79280d66db6177d77c41c59792",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "fcfc88835c398b2024035d145812f71a"
    ],
    [
      "Hacl.GenericField64.sub",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ac5a0d7c1535726b6b58566ff42fe21a",
        "refinement_interpretation_Tm_refine_b384fe79280d66db6177d77c41c59792",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "6a4d5abd7a7f7de86d7352ef98d33713"
    ],
    [
      "Hacl.GenericField64.mul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ac5a0d7c1535726b6b58566ff42fe21a",
        "refinement_interpretation_Tm_refine_b384fe79280d66db6177d77c41c59792",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "0da0ee655a32f6ebb93680ca857e5a1d"
    ],
    [
      "Hacl.GenericField64.sqr",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_878f104be3592dddcfe1cd1ec63da60d",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_b22fd053d96784b31095a75c74d3d481",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "038a6a504e5b694a9603299a666f6381"
    ],
    [
      "Hacl.GenericField64.one",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_6167c6ab7da5b7235ecc89829d85aa92",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ef18468237ae51aa9861da9102b843f3",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "03a42e2ceed5c83c85e920696649f297"
    ],
    [
      "Hacl.GenericField64.exp_consttime",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.GenericField64.t_limbs", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "b0e06d158c8c6320c5c87d3dd85d161e"
    ],
    [
      "Hacl.GenericField64.exp_consttime",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_00f2c1a6fadb82aaeb5336724514acf7",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_f07869ce5120a316bd74e738242f36b9",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "7e9aacadf167e7bf27ba5ebe089ae3f4"
    ],
    [
      "Hacl.GenericField64.exp_vartime",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.GenericField64.t_limbs", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "a7d7a32b9c14766045465591b3bc31e0"
    ],
    [
      "Hacl.GenericField64.exp_vartime",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Bignum.Definitions.lbignum",
        "equation_Hacl.Bignum.Definitions.limb",
        "equation_Hacl.GenericField64.km",
        "equation_Hacl.GenericField64.t_limbs",
        "equation_Lib.Buffer.lbuffer_t",
        "lemma_Hacl.Bignum.Montgomery.mk_runtime_mont_len_lemma",
        "refinement_interpretation_Tm_refine_00f2c1a6fadb82aaeb5336724514acf7",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_f07869ce5120a316bd74e738242f36b9",
        "typing_Hacl.GenericField64.t_limbs"
      ],
      0,
      "9979f78e21d72ae1c95ccbae6d6b0864"
    ]
  ]
]