[
"���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"
]
]
]