[
  "Èû‘i\u007fõ˜)¢K«¤)„\u0001”",
  [
    [
      "Hacl.Spec.Ed25519.Field56.Definition.pow32",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "e087fc633fc62eee9be10ca2b5b0b075"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.pow56",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b9a88384ccf039754980cbfc58d354f6"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.as_nat5",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1"
      ],
      0,
      "db76b7c0e808dd66df70172d512dd3b2"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.as_nat10",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p1",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p2",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p3",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p4",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p5",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p6",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p7",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p8",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p9",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "aeabdf94d8402129dd641ae1cf03b1fd"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.eval_wide9",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p1",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p2",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p3",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p4",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p5",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p6",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p7",
        "equation_Hacl.Spec.Ed25519.Field56.Definition.p8",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok"
      ],
      0,
      "0a551bd4ae34910e9ce3d90aefc49df7"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.felem_fits",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "42302354e59d16dcb5adac28caca1bc9"
    ]
  ]
]