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
Vale.Poly1305.X64.fsti.hints
[
"\b\r����Y��C�pS1�(",
[
[
"Vale.Poly1305.X64.va_req_Poly1305",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"unit_typing"
],
0,
"0ebe9d5bbb19a80499e7f968d695c6d9"
],
[
"Vale.Poly1305.X64.va_ens_Poly1305",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prims.subtype_of",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"unit_typing"
],
0,
"79ae872dd54d9420390bc0a76f168bb4"
],
[
"Vale.Poly1305.X64.va_lemma_Poly1305",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Util.readable_words",
"equation_Vale.Poly1305.Util.validSrcAddrs64",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.validDstAddrs64",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6688d8d4d0a4ee4e5fc12d9bf7990aa3",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"5785f36f053a2f2f347c121905c3198b"
],
[
"Vale.Poly1305.X64.va_wp_Poly1305",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"d9155e0f2acf1a844b14e9224b0b6a38"
],
[
"Vale.Poly1305.X64.va_quick_Poly1305",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"065cfb6b4337034cf607a1d77641c82e"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...