[
  "���i\u007f��)�K��)�\u0001�",
  [
    [
      "Hacl.Spec.Ed25519.Field56.Definition.pow32",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "342f3f9021a234da0ce2c86f098bdcbb"
    ],
    [
      "Hacl.Spec.Ed25519.Field56.Definition.pow56",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "0fc2e631ae0440485fdb5fc3d942c01b"
    ],
    [
      "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,
      "841afbe754d7bdf747b2bd21455b571a"
    ],
    [
      "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,
      "adc6e318880425a26c09f835fedc84c1"
    ],
    [
      "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,
      "6b172c4d1808a08e5dde7b10756d444a"
    ],
    [
      "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,
      "ae5ac7018f958e49e3fc20883aa283fb"
    ]
  ]
]