Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Spec.Cipher16.fsti.hints
[
"��A����{�hN��3z",
[
[
"Spec.Cipher16.keylen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Cipher16.AES128",
"disc_equation_Spec.Cipher16.AES256",
"disc_equation_Spec.Cipher16.CHACHA20",
"fuel_guarded_inversion_Spec.Cipher16.alg"
],
0,
"7803929439da84ee4d6732fb2ce90c33"
],
[
"Spec.Cipher16.slen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Cipher16.AES128",
"disc_equation_Spec.Cipher16.AES256",
"disc_equation_Spec.Cipher16.CHACHA20",
"fuel_guarded_inversion_Spec.Cipher16.alg"
],
0,
"5ba29404e643a6fed8af433b43a2971d"
],
[
"Spec.Cipher16.lbytes",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d439c543b65ca9741f1af48a37f9c2d4"
],
[
"Spec.Cipher16.key",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Cipher16.keylen",
"fuel_guarded_inversion_Spec.Cipher16.alg",
"projection_inverse_BoxInt_proj_0"
],
0,
"f8eedff1e2dc82ec2da20da809de7a8c"
],
[
"Spec.Cipher16.expand",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Cipher16.bytes", "equation_Spec.Cipher16.key",
"equation_Spec.Cipher16.keylen", "equation_Spec.Cipher16.lbytes",
"equation_Spec.Cipher16.slen", "function_token_typing_FStar.UInt8.t",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_fa9367774f23a225015924c83bbe1f7c",
"typing_FStar.Seq.Base.length"
],
0,
"ab93c8a730944fdc28894899aa109c19"
]
]
]
Computing file changes ...