Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Vale.SHA.X64.fsti.hints
[
"HKd f�W;\u0004H:�\u001b�}�",
[
[
"Vale.SHA.X64.va_req_Sha_update_bytes_stdcall",
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,
"67f80037843cda5f3ef272f2a3e6fc1d"
],
[
"Vale.SHA.X64.va_ens_Sha_update_bytes_stdcall",
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.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.X64.va_req_Sha_update_bytes_stdcall",
"equation_Vale.X64.Decls.va_state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"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,
"0ec9b081c3807b1932fb52df816ef5ed"
],
[
"Vale.SHA.X64.va_lemma_Sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cbaa862e461df0ff4edfd6ae3330fb67"
],
0,
"0a142efc69198fb44dcf7ad0c181e067"
],
[
"Vale.SHA.X64.va_wp_Sha_update_bytes_stdcall",
1,
1,
0,
[
"@query", "equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"projection_inverse_BoxInt_proj_0"
],
0,
"752741312d69fb9b14eb999de0e26846"
],
[
"Vale.SHA.X64.va_quick_Sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"a3b7958d5d436c8fc8c1d230f5916636"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...