[
  "vá8Oˆ? 4eÄ\u0010ZñÞ¢•",
  [
    [
      "Hacl.Bignum32.add_mod",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "65a84d17d52d16701c1a066970cdf8c8"
    ],
    [
      "Hacl.Bignum32.sub_mod",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "cae60ecec4030ad083fcfa5ec2a85017"
    ],
    [
      "Hacl.Bignum32.mul",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Bignum32.t_limbs", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "049cf6cbe48044754629d1cb2547b6d6"
    ],
    [
      "Hacl.Bignum32.sqr",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Bignum32.t_limbs", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "16c5b23b3061d9e4092604d9dbf68d0a"
    ],
    [
      "Hacl.Bignum32.bn_to_bytes_be",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Bignum32.t_limbs", "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_Prims.nat",
        "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_Lib.IntTypes.numbytes",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e4ab4c721d2c908e12d74b122308a922"
    ],
    [
      "Hacl.Bignum32.bn_to_bytes_le",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Bignum32.t_limbs", "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_Prims.nat",
        "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_Lib.IntTypes.numbytes",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c45a0220cc99c868f7571f1d522f213e"
    ]
  ]
]