[
  "\u00116\u0012™æÿÅp|\u0019Ä\u000fšÌp\u0003",
  [
    [
      "Hacl.Impl.P256.MM.Exponent.square_root",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.P256.Definitions.as_nat",
        "equation_Spec.P256.prime", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4753fc6eae560e46a35cdc89d8ec69b5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.P256.Definitions.as_nat", "typing_Spec.P256.prime"
      ],
      0,
      "b96280bb8492b8177e0d2b93584385ed"
    ]
  ]
]