Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Vale.X64.InsSha.fsti.hints
[
"�e���z�(\u0007.�W���\u0006",
[
[
"Vale.X64.InsSha.va_lemma_SHA256_rnds2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1ac5541806f355944a04e7bdf6a74b55",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"48fb42d7d6af6a3a66c4d23d4d39f84e"
],
[
"Vale.X64.InsSha.va_wp_SHA256_rnds2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"a4f875e8e206814e744055989b88e0fc"
],
[
"Vale.X64.InsSha.va_quick_SHA256_rnds2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b672162e654080fc6c344760d0d634fd"
],
[
"Vale.X64.InsSha.va_lemma_SHA256_msg1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b967a8468023c5d864ececc4f584ab81"
],
[
"Vale.X64.InsSha.va_wp_SHA256_msg1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"d63a0f3c5e4adef9014af67c85680a22"
],
[
"Vale.X64.InsSha.va_quick_SHA256_msg1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"a19f310ef60dfe2f9c42ac8a26226eac"
],
[
"Vale.X64.InsSha.va_lemma_SHA256_msg2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"3b215a48bbb3f935555a897a40c63fe3"
],
[
"Vale.X64.InsSha.va_wp_SHA256_msg2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f48f6643aa73b24ee44e490153a7aa48"
],
[
"Vale.X64.InsSha.va_quick_SHA256_msg2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"8d619dc6f715778ce3ea4bd769cea8b5"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...