Revision 1068d4afc039dbd12db6dbce298cdb0962d6d224 authored by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC, committed by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC
1 parent d7fe03c
X64.SHA.fst.hints
[
"B�3Q(Y���\u001a�z*���",
[
[
"X64.SHA.va_lemma_preamble",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.Rax",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.l_and", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_SHA_helpers.hash256", "equation_Types_s.byte_to_twobits",
"equation_Types_s.quad32", "equation_Types_s.select_word",
"equation_Words.Four_s.four_select", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_SHA_helpers.word",
"function_token_typing_Words_s.nat32", "int_inversion",
"interpretation_Tm_abs_033c986f28fa90d27d2ea96e5cb797c4",
"interpretation_Tm_abs_26b78bca4f221b4c469edd213f71ebef",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_SHA_helpers.make_hash",
"typing_SHA_helpers.make_ordered_hash",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_X64.Machine_s.Rdi@tok", "unit_typing"
],
0,
"3c750a15b456bbabc8b88a9c148cd8b3"
],
[
"X64.SHA.va_wpMonotone_preamble",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.Rax@tok", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_preamble",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
],
0,
"cdea4bf3c81b1e51b9376481cb558ace"
],
[
"X64.SHA.va_wpCompute_preamble",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_preamble",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"335345a7085aa2fe6e44b6963ec24ff5"
],
[
"X64.SHA.va_wpProof_preamble",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"df21d810399e050c5c74469f971b7d92"
],
[
"X64.SHA.va_wpProof_preamble",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_preamble",
"equation_X64.SHA.va_wp_preamble",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_preamble",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
],
0,
"69cec191490a752901e58da42cb4e2e0"
],
[
"X64.SHA.va_qcode_loop_rounds_0_15",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"b50a725879e3a828ad92daa7c9173f2e"
],
[
"X64.SHA.va_lemma_loop_rounds_0_15",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
"@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Spec.Loops_interpretation_Tm_arrow_4141e6858c055a47126e62563c8ecb9c",
"bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Arch.Types.add_wrap_quad32",
"equation_Arch.Types.reverse_bytes_quad32_seq",
"equation_Collections.Seqs_s.compose",
"equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_SHA_helpers.hash256", "equation_SHA_helpers.k_reqs",
"equation_SHA_helpers.quads_to_block",
"equation_SHA_helpers.size_block_w_256",
"equation_SHA_helpers.ws_quad32",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
"equation_Types_s.quad32", "equation_Types_s.select_word",
"equation_Types_s.twobits", "equation_Words.Four_s.four_select",
"equation_Words_s.nat2", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.Decls.validSrcAddrsOffset128",
"equation_X64.Vale.State.state_eq",
"equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_SHA_helpers.hash256",
"function_token_typing_Types_s.reverse_bytes_quad32",
"function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
"interpretation_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"l_and-interp", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_e8985fc4d83b1f11adbf3a9b5b8bb8f2",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "token_correspondence_FStar.Seq.Base.index",
"typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_FStar.Seq.Base.length", "typing_SHA_helpers.make_hash",
"typing_Spec.Hash.Definitions.word", "typing_Spec.MD5.init",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
"typing_Words_s.__proj__Mkfour__item__lo0",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_Workarounds.index_work_around_quad32",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.base_typ_as_vale_type",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
],
0,
"ab742c472ecf0d8dce541dc159734fc9"
],
[
"X64.SHA.va_wpMonotone_loop_rounds_0_15",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_loop_rounds_0_15",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"4eeb7f20015bcb58505544b0a986263e"
],
[
"X64.SHA.va_wpCompute_loop_rounds_0_15",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop_rounds_0_15",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"3b0917f6e5d5c7b2594ba4e5b53fc977"
],
[
"X64.SHA.va_wpProof_loop_rounds_0_15",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"09e3ed453e36cf2d9fc18fe15e5c73ba"
],
[
"X64.SHA.va_wpProof_loop_rounds_0_15",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rsi@tok",
"equation_Prims.nat", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_rounds_0_15",
"equation_X64.SHA.va_wp_loop_rounds_0_15",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_rounds_0_15",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"e84231297d5a3fbd4bbb73f2f68e8ac1"
],
[
"X64.SHA.va_qcode_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"3b458c0880471257e1a749934dbad9ee"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
"equation_SHA_helpers.hash256", "equation_Types_s.quad32",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bb2789de94cd069ecaf5fcc28df052aa"
],
0,
"83055b24e1a7212b1e412cf2a87297a3"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Arch.Types.add_wrap_quad32", "equation_Prims.eq2",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_SHA_helpers.hash256",
"equation_SHA_helpers.k_reqs",
"equation_SHA_helpers.size_block_w_256",
"equation_SHA_helpers.ws_quad32",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
"equation_Types_s.quad32", "equation_Types_s.select_word",
"equation_Types_s.twobits", "equation_Words.Four_s.four_select",
"equation_Words_s.nat2", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
"l_and-interp", "lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Spec.Hash.Definitions.state_word_length",
"typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_Workarounds.index_work_around_quad32",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rcx@tok", "unit_typing"
],
0,
"d2e6a8bc83c5d8d26c90a0e846e01c63"
],
[
"X64.SHA.va_wp_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"d493436d656bb9e4abeec9341aaafd77"
],
[
"X64.SHA.va_wpMonotone_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_loop_rounds_16_51_body",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
],
0,
"4ddeff230f7081cd27fd5bb15850e05c"
],
[
"X64.SHA.va_wpCompute_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop_rounds_16_51_body",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"0139d79d39bcb1ae21b838209011d63b"
],
[
"X64.SHA.va_wpProof_loop_rounds_16_51_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"20879d221911d6b8221f5b32d83ac516"
],
[
"X64.SHA.va_wpProof_loop_rounds_16_51_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat", "equation_SHA_helpers.counter",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_rounds_16_51_body",
"equation_X64.SHA.va_wp_loop_rounds_16_51_body",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_rounds_16_51_body",
"typing_SHA_helpers.ws_quad32", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"07fee9c67f35c73231207d6f7be99ac9"
],
[
"X64.SHA.va_lemma_msg_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.l_and", "int_typing",
"kinding_Prims.equals@tok", "l_and-interp",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"string_typing", "typing_Prims.eq2", "typing_Prims.l_and",
"typing_Prims.squash",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_Types_s.quad32", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_typing"
],
0,
"64cac9a6327094881784c4b757738eb4"
],
[
"X64.SHA.va_wpMonotone_msg_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_msg_shift",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
],
0,
"d2d6b9519d65426086a85e20aa9f97a4"
],
[
"X64.SHA.va_wpCompute_msg_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_msg_shift",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"55fe460cbb3ead363b42192272696fe4"
],
[
"X64.SHA.va_wpProof_msg_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"0418648dff128eba07614448f728bf43"
],
[
"X64.SHA.va_wpProof_msg_shift",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_msg_shift",
"equation_X64.SHA.va_wp_msg_shift",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_msg_shift",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"unit_typing"
],
0,
"effafa4fc5c01bd01fc46e88ccc70def"
],
[
"X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_e22ba7a032a73f6d0678d3d186686631_0", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"85cc2467e791a22821fcd3a55fe513cf"
],
[
"X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
"equation_Prims.nat", "int_typing",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"b03c878c6ceb5a6e4b75c5f66535c078"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51_recursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
"equation_SHA_helpers.hash256",
"refinement_interpretation_Tm_refine_4c2a6cf89c770d3d5ae1539757c4bf6f"
],
0,
"fb078709686611908de40582a9ee4e5b"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51_recursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
"equation_SHA_helpers.hash256",
"refinement_interpretation_Tm_refine_4c2a6cf89c770d3d5ae1539757c4bf6f"
],
0,
"11facf83f3690709eda8840be60f1044"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51_recursive",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
"@fuel_correspondence_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
"@fuel_irrelevance_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
"@fuel_irrelevance_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_661f8a7e3bd81eb0a2bc263395f5dddc_1",
"binder_x_e22ba7a032a73f6d0678d3d186686631_2",
"binder_x_fc86bc8eb8e2bf328df1838e1072996e_4", "bool_inversion",
"constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"eq2-interp", "equation_Prims.nat", "equation_SHA_helpers.block_w",
"equation_SHA_helpers.counter",
"equation_SHA_helpers.size_block_w_256", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
"equation_with_fuel_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_SHA_helpers.word",
"function_token_typing_SHA_helpers.ws_partial_def", "int_inversion",
"int_typing", "kinding_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_upd_eq",
"lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_GreaterThan",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"subterm_ordering_Prims.Cons",
"subterm_ordering_X64.Machine_s.Block",
"token_correspondence_Opaque_s.make_opaque",
"typing_FStar.Seq.Base.length", "typing_Opaque_s.make_opaque",
"typing_SHA_helpers.ws_quad32",
"typing_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd"
],
0,
"3b2fb8499f0321384516a419a19d9061"
],
[
"X64.SHA.va_lemma_loop_rounds_16_51",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"eq2-interp", "equation_X64.SHA.va_code_loop_rounds_16_51",
"equation_X64.SHA.va_transparent_code_loop_rounds_16_51",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"typing_X64.Vale.State.__proj__Mkstate__item__ok"
],
0,
"50db75a5ea323df58aba494cdcf4cdb2"
],
[
"X64.SHA.va_wpMonotone_loop_rounds_16_51",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_loop_rounds_16_51",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
],
0,
"f65b19b7808adbf42360e9f63e9fac13"
],
[
"X64.SHA.va_wpCompute_loop_rounds_16_51",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_code_loop_rounds_16_51",
"equation_X64.SHA.va_wp_loop_rounds_16_51",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"228e822e5c5757f1bc1036d028a4d0d5"
],
[
"X64.SHA.va_wpProof_loop_rounds_16_51",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"f60c22ab3e3fb87d43de06e066ab55e8"
],
[
"X64.SHA.va_wpProof_loop_rounds_16_51",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat", "equation_SHA_helpers.block_w",
"equation_SHA_helpers.counter", "equation_SHA_helpers.hash256",
"equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_code_loop_rounds_16_51",
"equation_X64.SHA.va_wpCompute_loop_rounds_16_51",
"equation_X64.SHA.va_wp_loop_rounds_16_51",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f28dc85b4b10d4fff3b43739c58e4784",
"token_correspondence_X64.SHA.va_wpCompute_loop_rounds_16_51",
"typing_SHA_helpers.ws_quad32",
"typing_X64.SHA.va_code_loop_rounds_16_51",
"typing_X64.SHA.va_lemma_loop_rounds_16_51",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"9ad0cc379e7776d4ba69050f08d3b8f7"
],
[
"X64.SHA.va_lemma_loop_rounds_52_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Arch.Types.add_wrap_quad32", "equation_Prims.eq2",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_SHA_helpers.hash256",
"equation_SHA_helpers.k_reqs", "equation_SHA_helpers.ws_quad32",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
"equation_Types_s.quad32", "equation_Types_s.select_word",
"equation_Types_s.twobits", "equation_Words.Four_s.four_select",
"equation_Words_s.nat2", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
"l_and-interp", "lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Spec.Hash.Definitions.state_word_length",
"typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_Workarounds.index_work_around_quad32",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_inversion", "unit_typing"
],
0,
"846f1fa2a82390409174a970a45fbcb0"
],
[
"X64.SHA.va_wpMonotone_loop_rounds_52_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_loop_rounds_52_64",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"da09bf6ea2bc04ac671257ca571f24c6"
],
[
"X64.SHA.va_wpCompute_loop_rounds_52_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop_rounds_52_64",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"71043b739caeb6c1d29b502794164d45"
],
[
"X64.SHA.va_wpProof_loop_rounds_52_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"9198386eb2b265262038374a98531cef"
],
[
"X64.SHA.va_wpProof_loop_rounds_52_64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_rounds_52_64",
"equation_X64.SHA.va_wp_loop_rounds_52_64",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_rounds_52_64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"8bc729c309b0b9ff2aa0ba6f6ea602b5"
],
[
"X64.SHA.va_qcode_loop_rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Types_s.quad32",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_337cdcfacffc90745df0e3b2954dd394",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"6954bbe7460382fe31de5b76b136ecff"
],
[
"X64.SHA.va_lemma_loop_rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Collections.Seqs_s.compose",
"equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_SHA_helpers.hash256",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.Decls.validSrcAddrsOffset128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Prims.l_and",
"function_token_typing_SHA_helpers.hash256",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Prims.equals@tok", "kinding_Words_s.four@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_FStar.Seq.Base.length", "typing_Prims.eq2",
"typing_Prims.l_and", "typing_Prims.squash",
"typing_SHA_helpers.make_hash",
"typing_SHA_helpers.update_multi_quads",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
],
0,
"d6be173a90b663f107c88a8855524ed5"
],
[
"X64.SHA.va_wpMonotone_loop_rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_rounds",
"equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"13e341cec9dfd7cedc77a01c18d0a354"
],
[
"X64.SHA.va_wpCompute_loop_rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop_rounds",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"d62b92781814e967e53d509d149dd2d0"
],
[
"X64.SHA.va_wpProof_loop_rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"03ef17248535b064f962deb980319ab1"
],
[
"X64.SHA.va_wpProof_loop_rounds",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.nat",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_rounds",
"equation_X64.SHA.va_wp_loop_rounds",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_rounds",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"3822e2bbcdb381e9f6edef3f8851c3aa"
],
[
"X64.SHA.va_qcode_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"aef3cb099796275e20bd990733399c35"
],
[
"X64.SHA.va_lemma_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Collections.Seqs_s.compose",
"equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_SHA_helpers.hash256",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.Decls.validSrcAddrsOffset128",
"equation_X64.Vale.QuickCodes.lexCons",
"equation_X64.Vale.QuickCodes.precedes_wrap",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_SHA_helpers.hash256",
"function_token_typing_Words_s.nat32",
"function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_eta",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_FStar.Seq.Base.length", "typing_Prims.eq2",
"typing_SHA_helpers.make_hash",
"typing_SHA_helpers.update_multi_quads",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.lexCons",
"typing_X64.Vale.QuickCodes.precedes_wrap",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Prims.LexTop@tok", "typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Secret@tok", "well-founded-ordering-on-nat"
],
0,
"15086551e62160c23f65f37fa8ab6a31"
],
[
"X64.SHA.va_wpMonotone_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_body",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok"
],
0,
"4169a385c5fa8e42710dd9444e014ebf"
],
[
"X64.SHA.va_wpCompute_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop_body",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"f592f8fc4eb13bccd83a98092106d85f"
],
[
"X64.SHA.va_wpProof_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"1b893c63087981f6c7e74942ec059f44"
],
[
"X64.SHA.va_wpProof_loop_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_body",
"equation_X64.SHA.va_wp_loop_body",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_body",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok"
],
0,
"b609031782a4b210a75fd723c42eb6c0"
],
[
"X64.SHA.va_code_loop_while",
1,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"510f7dc0b2f822a70d388f5d040ba6b5"
],
[
"X64.SHA.va_qcode_loop_while",
1,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"cd78ea2839eea89f4bbba50a35422aeb"
],
[
"X64.SHA.va_qcode_loop_while",
2,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"e60668ecf54e25da5cde3e874d997f9c"
],
[
"X64.SHA.va_qcode_loop_while",
3,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"a24b15c50d9ec8af2f24dfdb331c8cdf"
],
[
"X64.SHA.va_lemma_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
"eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_False",
"equation_Prims.l_imp", "equation_Prims.l_not",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_SHA_helpers.hash256",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.lexCons",
"equation_X64.Vale.QuickCodes.precedes_wrap",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_SHA_helpers.hash256",
"function_token_typing_Words_s.nat32", "int_typing",
"kinding_Words_s.four@tok", "l_not-interp",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_eta",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_GreaterThan",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_Prims.eq2", "typing_SHA_helpers.make_hash",
"typing_SHA_helpers.update_multi_quads",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"b22fc5b39d2263b0326ed9b77f494ca3"
],
[
"X64.SHA.va_wpMonotone_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_while",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok"
],
0,
"7b3c858285f384eca0513d607996011b"
],
[
"X64.SHA.va_wpCompute_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_code_loop_while",
"equation_X64.SHA.va_wp_loop_while",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"d7bbfc739600991141cb70c531bc01aa"
],
[
"X64.SHA.va_wpProof_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"ef0b9493dc74fabf13ae0775aee00402"
],
[
"X64.SHA.va_wpProof_loop_while",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop_while",
"equation_X64.SHA.va_wp_loop_while",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop_while",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok"
],
0,
"f2f9f7a5b2e17e55500d0078d37aee2b"
],
[
"X64.SHA.va_lemma_loop",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_SHA_helpers.update_multi_quads.fuel_instrumented",
"@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Arch.Types.reverse_bytes_quad32_seq",
"equation_Collections.Seqs_s.compose",
"equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_SHA_helpers.hash256",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_with_fuel_SHA_helpers.update_multi_quads.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Prims.l_and",
"function_token_typing_SHA_helpers.hash256", "int_inversion",
"int_typing", "kinding_Prims.equals@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Prims.eq2", "typing_Prims.squash",
"typing_SHA_helpers.make_hash",
"typing_SHA_helpers.update_multi_quads",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.base_typ_as_vale_type",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.buffer_length",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"f1c4ef50ef60d3adb41ee910a7c97772"
],
[
"X64.SHA.va_wpMonotone_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop",
"equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"8ae78de166d328c2f4b1bf40deac38f4"
],
[
"X64.SHA.va_wpCompute_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_loop",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"6a810f3dec3ad9d5bca939d15cb08a39"
],
[
"X64.SHA.va_wpProof_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"6aa51eb315655d45a28bced5674a1348"
],
[
"X64.SHA.va_wpProof_loop",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_loop", "equation_X64.SHA.va_wp_loop",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_loop",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"f8796327b054b4dd2aa0dc535bac9632"
],
[
"X64.SHA.va_lemma_epilogue",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_SHA_helpers.hash256", "equation_Types_s.bits_of_byte",
"equation_Types_s.byte_to_twobits", "equation_Types_s.quad32",
"equation_Types_s.select_word", "equation_Types_s.twobits",
"equation_Words.Four_s.four_select", "equation_Words_s.nat2",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.nat8", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_SHA_helpers.word",
"function_token_typing_Words_s.nat2",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"interpretation_Tm_abs_468206d1e1978da391344670f4f23403",
"interpretation_Tm_abs_6d69aedb2edc4e3d4a0c9a18d04d64d6",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.l_and", "typing_SHA_helpers.make_hash",
"typing_SHA_helpers.make_ordered_hash",
"typing_Types_s.byte_to_twobits", "typing_Types_s.quad32",
"typing_Types_s.select_word",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rdi@tok", "unit_typing"
],
0,
"3f899851da50132c2929de2752da73bc"
],
[
"X64.SHA.va_wpMonotone_epilogue",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_epilogue",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
],
0,
"8f58f58ba368bc2754b6fc53e985267f"
],
[
"X64.SHA.va_wpCompute_epilogue",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_epilogue",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"78a780988f04dec4bb5214fe138ee0b1"
],
[
"X64.SHA.va_wpProof_epilogue",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"9410e1564d9c45fcdf81a830166389cb"
],
[
"X64.SHA.va_wpProof_epilogue",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_epilogue",
"equation_X64.SHA.va_wp_epilogue",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_epilogue",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"5000f30cd200a73868f949fcc26a7001"
],
[
"X64.SHA.va_lemma_sha_update",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eqtype",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prop_s.prop0", "equation_SHA_helpers.hash256",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_SHA_helpers.hash256", "int_typing",
"l_and-interp", "lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
"typing_Prims.eq2", "typing_Prims.l_and",
"typing_SHA_helpers.make_ordered_hash",
"typing_SHA_helpers.update_multi_quads",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.base_typ_as_vale_type",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"05588590e9fad32917e475f23f886ee5"
],
[
"X64.SHA.va_wpMonotone_sha_update",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_sha_update",
"equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"3fbc1da32ef4c48a79f4386ffc609171"
],
[
"X64.SHA.va_wpCompute_sha_update",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_sha_update",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"f50996cf5f8a80d2498da7b426ae77e7"
],
[
"X64.SHA.va_wpProof_sha_update",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"2aac83d34a5c4c2a1f8b7a149c19609c"
],
[
"X64.SHA.va_wpProof_sha_update",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_sha_update",
"equation_X64.SHA.va_wp_sha_update",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_sha_update",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"6dd01fc5f49752510a990249263a5dbd"
],
[
"X64.SHA.va_qcode_sha_update_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"db48070c59a53fc3cdb0557c304a5061"
],
[
"X64.SHA.va_qcode_sha_update_bytes",
2,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"5512c385708ade482560fea3a7dc527f"
],
[
"X64.SHA.va_qcode_sha_update_bytes",
3,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"82f1ccd057b005bdf781ae11da34b646"
],
[
"X64.SHA.va_qcode_sha_update_bytes",
4,
1,
0,
[
"@query", "equation_SHA_helpers.block_length",
"equation_SHA_helpers.size_block_w_256",
"projection_inverse_BoxInt_proj_0"
],
0,
"1536da59dfb1c3d2334060495a384a1b"
],
[
"X64.SHA.va_lemma_sha_update_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_SHA_helpers.byte", "equation_SHA_helpers.hash256",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Types_s.quad32", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_SHA_helpers.hash256", "int_inversion",
"int_typing", "l_and-interp",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_eta",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Prims.eq2", "typing_Prims.l_and",
"typing_SHA_helpers.le_bytes_to_hash",
"typing_Types_s.le_seq_quad32_to_bytes",
"typing_Workarounds.slice_workaround",
"typing_X64.CPU_Features_s.sha_enabled",
"typing_X64.Memory.base_typ_as_vale_type",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_length",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
],
0,
"db40c2669a01463408f41c54ad526ddf"
],
[
"X64.SHA.va_wpMonotone_sha_update_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_sha_update_bytes",
"equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_Spec.Hash.Definitions.MD5@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"49f529d724cc843fc97da197b82ef1a0"
],
[
"X64.SHA.va_wpCompute_sha_update_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.SHA.va_wp_sha_update_bytes",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"03330f5ea2ed3baa8afff493f300db78"
],
[
"X64.SHA.va_wpProof_sha_update_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"f059e8df3d295c0825a6fced052ed8f3"
],
[
"X64.SHA.va_wpProof_sha_update_bytes",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_SHA_helpers.byte",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_sha_update_bytes",
"equation_X64.SHA.va_wp_sha_update_bytes",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_sha_update_bytes",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"d7c318c52fd0c2c8b5324a8f47c41d97"
],
[
"X64.SHA.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_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"77478f36328814da0df2afe180b45f4b"
],
[
"X64.SHA.va_ens_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Prims.subtype_of", "equation_SHA_helpers.block_length",
"equation_SHA_helpers.byte", "equation_SHA_helpers.size_block_w_256",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.SHA.va_req_sha_update_bytes_stdcall",
"equation_X64.Vale.Decls.va_state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"3da9e12b698e1f08258c94b2f231831f"
],
[
"X64.SHA.va_qcode_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_SHA_helpers.block_length",
"equation_SHA_helpers.size_block_w_256", "equation_Words_s.nat64",
"equation_Words_s.natN", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"4195522ad107a0ad54b0fb19e91a32ff"
],
[
"X64.SHA.va_qcode_sha_update_bytes_stdcall",
2,
1,
0,
[
"@query", "equation_SHA_helpers.block_length",
"equation_SHA_helpers.size_block_w_256",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0"
],
0,
"9eded98ac254152cbc0b828aa69e8b48"
],
[
"X64.SHA.va_lemma_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"equation_SHA_helpers.block_length", "equation_SHA_helpers.byte",
"equation_SHA_helpers.size_block_w_256", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Memory.buffer128",
"equation_X64.Memory.vuint128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_X64.CPU_Features_s.sha_enabled",
"function_token_typing_X64.Memory.vuint128", "int_inversion",
"proj_equation_X64.Vale.State.Mkstate_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"refinement_interpretation_X64.SHA_Tm_refine_bef743ed8e583a213aacac0db17045bb",
"typing_X64.Memory.buffer_length", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok"
],
0,
"c2902b555cd5ff38830fbcc233e99cf6"
],
[
"X64.SHA.va_lemma_sha_update_bytes_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Machine_s.Rax",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Arch.Types.hi64",
"equation_Arch.Types.lo64", "equation_Prims.eq2",
"equation_Prims.l_and", "equation_Prims.l_imp",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_SHA_helpers.block_length", "equation_SHA_helpers.byte",
"equation_SHA_helpers.hash256",
"equation_SHA_helpers.size_block_w_256",
"equation_Types_s.le_seq_quad32_to_bytes",
"equation_Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_operand_dst_opr64",
"equation_X64.Vale.Decls.va_upd_operand_reg_opr64",
"equation_X64.Vale.Decls.va_upd_operand_xmm",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
"l_and-interp", "l_imp-interp", "l_not-interp",
"lemma_Types_s.le_seq_quad32_to_bytes_length",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Stack_i.lemma_compose_free_stack64",
"lemma_X64.Stack_i.lemma_correct_store_load_stack64",
"lemma_X64.Stack_i.lemma_frame_store_load_stack64",
"lemma_X64.Stack_i.lemma_free_stack_same_load64",
"lemma_X64.Stack_i.lemma_free_stack_same_valid64",
"lemma_X64.Stack_i.lemma_same_init_rsp_free_stack64",
"lemma_X64.Stack_i.lemma_same_init_rsp_store_stack64",
"lemma_X64.Stack_i.lemma_store_new_valid64",
"lemma_X64.Stack_i.lemma_store_stack_same_valid64",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality", "primitive_Prims.op_disEquality",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.Decls.TReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Arch.Types.hi64", "typing_Arch.Types.lo64",
"typing_Prims.eq2", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
"typing_X64.Stack_i.init_rsp", "typing_X64.Stack_i.store_stack64",
"typing_X64.Stack_i.valid_src_stack64",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_inversion", "unit_typing"
],
0,
"f09d791d6adcf4b42a1e7f3d04197a07"
],
[
"X64.SHA.va_wp_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equation_Prims.nat", "equation_SHA_helpers.block_length",
"equation_SHA_helpers.byte", "equation_SHA_helpers.size_block_w_256",
"equation_Words_s.nat64", "equation_Words_s.natN",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Words_s.nat64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"typing_X64.SHA_Tm_abs_33c3994de7d754283ab0cc7b2921b72e",
"typing_X64.SHA_Tm_abs_b1e1a7fb7a7968d210062719315e71c2",
"typing_X64.SHA_Tm_abs_c2631d9abab9b993938b087d5057f4af",
"typing_X64.SHA_Tm_abs_c2bb5b1221b8afc9d05888f8b139b633",
"typing_X64.Vale.Decls.va_if", "unit_typing"
],
0,
"b0884dc8a266d11550b1edcb1ccd5f30"
],
[
"X64.SHA.va_wpMonotone_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
"equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"39232b5152c19489cb7b18f210f81de6"
],
[
"X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Words_s.nat64",
"equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
"interpretation_Tm_abs_50c23f9cc303c7ea6b4d93bbc25b4c06",
"interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
"interpretation_Tm_abs_b6f39720dc3d793091496036edf9db50",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"unit_typing"
],
0,
"a4ca6a055d268186a05886cc56be1abc"
],
[
"X64.SHA.va_wpProof_sha_update_bytes_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"c3bbfe2b3d6beb5cb07dc343b5e5e84b"
],
[
"X64.SHA.va_wpProof_sha_update_bytes_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Words_s.nat64",
"equation_X64.Machine_s.xmm",
"equation_X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
"equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
"interpretation_Tm_abs_50c23f9cc303c7ea6b4d93bbc25b4c06",
"interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
"interpretation_Tm_abs_b6f39720dc3d793091496036edf9db50",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"1bc44e76857472f7150e15a8cf653588"
]
]
]
Computing file changes ...
