[ "¢\u0012*]ãyÈ6a\u0007Á\u0014€¥€p", [ [ "Vale.SHA.X64.va_lemma_Preamble", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Tm_unit", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.l_and", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.bits_of_byte", "equation_Vale.Def.Types_s.byte_to_twobits", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Types_s.select_word", "equation_Vale.Def.Types_s.twobits", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_buffer_read", "equation_Vale.X64.Memory.valid_layout_buffer", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat2", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "interpretation_Tm_abs_9011f92af99d6f294e8ead5f2dc3bbc2", "interpretation_Tm_abs_accadb694a0737f554f6f8e909a40668", "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.OReg_r", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_52159ea6753e9180a44d69076e7f9cf4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.byte_to_twobits", "typing_Vale.Def.Types_s.select_word", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.SHA.SHA_helpers.make_hash", "typing_Vale.SHA.SHA_helpers.make_ordered_hash", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "unit_typing" ], 0, "026dd30b82f75be04907d0166fc6d0ed" ], [ "Vale.SHA.X64.va_wpProof_Preamble", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.SHA.X64.va_wp_Preamble", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "4b0d4c1c1782a8e98db64a1f0fd68581" ], [ "Vale.SHA.X64.va_quick_Preamble", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "957b5691cf2bc75ff3dcccbb2c67ff45" ], [ "Vale.SHA.X64.va_qcode_Loop_rounds_0_15", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat", "equation_Prims.squash", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "366f70a94000e92469736b5cd7116001" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_0_15", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e617b8e68c21a948cfb3e1fd94613721", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "f107bfb1675cf613a8b6e784e5755b0e" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_0_15", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.Types.add_wrap_quad32", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq", "equation_Vale.Def.Types_s.bits_of_byte", "equation_Vale.Def.Types_s.byte_to_twobits", "equation_Vale.Def.Types_s.select_word", "equation_Vale.Def.Types_s.twobits", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.SHA_helpers.k_reqs", "equation_Vale.SHA.SHA_helpers.quads_to_block", "equation_Vale.SHA.SHA_helpers.repeat_range_vale", "equation_Vale.SHA.SHA_helpers.ws_quad32", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_buffer_read", "equation_Vale.X64.Memory.valid_layout_buffer", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Arch.Types.reverse_bytes_nat32_quad32", "function_token_typing_Vale.Def.Words_s.nat2", "int_inversion", "int_typing", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "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_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_33841fdfdbf14c16be832537b069201d", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "token_correspondence_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Prims.eq2", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.byte_to_twobits", "typing_Vale.Def.Types_s.select_word", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.base_typ_as_vale_type", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion" ], 0, "b63bed0078161fd38bde4bc91c2f295b" ], [ "Vale.SHA.X64.va_wp_Loop_rounds_0_15", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "534d925318377332f53aff9c36503d2c" ], [ "Vale.SHA.X64.va_wpProof_Loop_rounds_0_15", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq", "equation_Vale.Def.Types_s.quad32", "equation_Vale.SHA.SHA_helpers.block_w", "equation_Vale.SHA.SHA_helpers.counter", "equation_Vale.SHA.SHA_helpers.k_reqs", "equation_Vale.SHA.SHA_helpers.quads_to_block", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "equation_Vale.SHA.X64.va_wp_Loop_rounds_0_15", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_typing", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913", "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_FStar.Seq.Base.init", "typing_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.Types.add_wrap_quad32", "typing_Vale.SHA.SHA_helpers.ws_partial", "typing_Vale.SHA.SHA_helpers.ws_quad32", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "4f000d4dc47abb41a984eeaf191301d1" ], [ "Vale.SHA.X64.va_quick_Loop_rounds_0_15", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "feed714fa02db3c0ea04cc31e472e962" ], [ "Vale.SHA.X64.va_qcode_Loop_rounds_16_51_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat", "equation_Prims.squash", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "c7acfc68c12ef211bc1d0c2271797a42" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550e1debb2eb3d1c6af62a8faf83930a" ], 0, "b27a7e1e7433714132383cab0df9d270" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51_body", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Loops_interpretation_Tm_arrow_991012978bfe18b65525b7a05d6a8a37", "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccbe963048a758dd021e4e7682cf18f7", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.Types.add_wrap_quad32", "equation_Vale.Def.Types_s.bits_of_byte", "equation_Vale.Def.Types_s.byte_to_twobits", "equation_Vale.Def.Types_s.select_word", "equation_Vale.Def.Types_s.twobits", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.counter", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.SHA_helpers.k_reqs", "equation_Vale.SHA.SHA_helpers.repeat_range_vale", "equation_Vale.SHA.SHA_helpers.ws_quad32", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_buffer_read", "equation_Vale.X64.Memory.valid_layout_buffer", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat2", "function_token_typing_Vale.SHA.SHA_helpers.shuffle_core_opaque", "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_2", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_kinding_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "string_typing", "typing_Prims.eq2", "typing_Spec.Loops.repeat_range", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.Types.add_wrap_quad32", "typing_Vale.Def.Types_s.byte_to_twobits", "typing_Vale.Def.Types_s.select_word", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Lib.Map16.get", "typing_Vale.SHA.SHA_helpers.make_hash", "typing_Vale.SHA.SHA_helpers.ws_partial", "typing_Vale.SHA.SHA_helpers.ws_quad32", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "0fcce33822f97a6497174e45232f2c95" ], [ "Vale.SHA.X64.va_wp_Loop_rounds_16_51_body", 1, 1, 0, [ "@query" ], 0, "94c064c828b5198543d9d49b5134c619" ], [ "Vale.SHA.X64.va_wpProof_Loop_rounds_16_51_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.SHA_helpers.counter", "equation_Vale.SHA.X64.va_wp_Loop_rounds_16_51_body", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.Types.add_wrap_quad32", "typing_Vale.SHA.SHA_helpers.ws_partial", "typing_Vale.SHA.SHA_helpers.ws_quad32", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "87a0caed00b6827d60501bcb5756197b" ], [ "Vale.SHA.X64.va_quick_Loop_rounds_16_51_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "8be8973d5e60541d90ea7709da5f51e8" ], [ "Vale.SHA.X64.va_lemma_Msg_shift", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "eq2-interp", "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "unit_typing" ], 0, "9339e188a4d4f76e7ca760da845f420b" ], [ "Vale.SHA.X64.va_wpProof_Msg_shift", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.X64.va_wp_Msg_shift", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "unit_typing" ], 0, "8ebfe2918fd833acb5b5cb1f901141a9" ], [ "Vale.SHA.X64.va_quick_Msg_shift", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "fe440d70a33e4224b06be2d5163f4601" ], [ "Vale.SHA.X64.va_code_Loop_rounds_16_51_recursive", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_e4836109f73687024ac3edd113084865", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equality_tok_Prims.LexTop@tok", "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_542f9d4f129664613f2483a6c88bc7c2", "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat" ], 0, "85d9dfc20ce68c1e71eea4026b21a10e" ], [ "Vale.SHA.X64.va_codegen_success_Loop_rounds_16_51_recursive", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_e4836109f73687024ac3edd113084865", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equality_tok_Prims.LexTop@tok", "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_542f9d4f129664613f2483a6c88bc7c2", "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat" ], 0, "e798a00c03a947a6944ad155d8a34d9a" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51_recursive", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_ab8b02266be49a94c5f944ce72ca5519" ], 0, "8a32466daac50229bb6b5b3b3ecf3839" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51_recursive", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_ab8b02266be49a94c5f944ce72ca5519" ], 0, "366f4ad738999fdf365a0ed701dc9926" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51_recursive", 3, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_e4836109f73687024ac3edd113084865", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "binder_x_0df71b5e34cded18ce6754646a0b75b9_4", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_eb96f2119e19317ec6e3b596d5a46609_1", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "data_elim_Vale.X64.State.Mkvale_state", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "equality_tok_Prims.LexTop@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.SHA.SHA_helpers.counter", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_GreaterThan", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.Machine_s.Reg_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "subterm_ordering_Prims.Cons", "subterm_ordering_Vale.X64.Machine_s.Block", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.SHA.SHA_helpers.ws_partial", "typing_Vale.SHA.SHA_helpers.ws_quad32", "typing_Vale.SHA.X64.va_code_Loop_rounds_16_51_recursive", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "typing_tok_Prims.LexTop@tok" ], 0, "31c03c20953fb117bdb6bdc8ee025a25" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_16_51", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "eq2-interp", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "fuel_guarded_inversion_Vale.X64.State.vale_state", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok" ], 0, "8e7991651495cb738a34dc2299089ac9" ], [ "Vale.SHA.X64.va_wpProof_Loop_rounds_16_51", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.SHA_helpers.counter", "equation_Vale.SHA.X64.va_wp_Loop_rounds_16_51", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.Types.add_wrap_quad32", "typing_Vale.SHA.SHA_helpers.ws_partial", "typing_Vale.SHA.SHA_helpers.ws_quad32", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "fba7a3479a3103fbbe8c4603da6975bf" ], [ "Vale.SHA.X64.va_quick_Loop_rounds_16_51", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "3309d76eddce434953f224d93cd4171f" ], [ "Vale.SHA.X64.va_qcode_Loop_rounds_52_64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "10bd5bbaaa79da70de57640d0ab07df6" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds_52_64", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.Types.add_wrap_quad32", "equation_Vale.Def.Types_s.bits_of_byte", "equation_Vale.Def.Types_s.byte_to_twobits", "equation_Vale.Def.Types_s.select_word", "equation_Vale.Def.Types_s.twobits", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.SHA_helpers.k_reqs", "equation_Vale.SHA.SHA_helpers.repeat_range_vale", "equation_Vale.SHA.SHA_helpers.ws_quad32", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_buffer_read", "equation_Vale.X64.Memory.valid_layout_buffer", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat2", "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_2", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThan", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_kinding_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.byte_to_twobits", "typing_Vale.Def.Types_s.select_word", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel", "typing_Vale.SHA.SHA_helpers.make_hash", "typing_Vale.SHA.SHA_helpers.update_block", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion", "unit_typing" ], 0, "84a17d171324fb3a9034d874740d9546" ], [ "Vale.SHA.X64.va_wpProof_Loop_rounds_52_64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.X64.va_wp_Loop_rounds_52_64", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "1af907ff3ee93e608eed4c87b39c24c5" ], [ "Vale.SHA.X64.va_quick_Loop_rounds_52_64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "562ea9815d2bcff1057d5735fc53de42" ], [ "Vale.SHA.X64.va_qcode_Loop_rounds", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_Prims.nat", "equation_Prims.squash", "int_inversion", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "68e8ea1e1c2b949f30413be0ff779df1" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_54e027cbb9ea2d87aa65e18b272b3560", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "97248afb1dc2ca3d1d2953e8bfffa827" ], [ "Vale.SHA.X64.va_lemma_Loop_rounds", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.base_typ_as_vale_type", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion" ], 0, "e8ccd3c248ab4037868b1f80c23a643c" ], [ "Vale.SHA.X64.va_wp_Loop_rounds", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "6f0e73cd055693167c110d8813d19d25" ], [ "Vale.SHA.X64.va_wpProof_Loop_rounds", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.X64.va_wp_Loop_rounds", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "typing_FStar.Seq.Base.length", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "fe44559da690fdc98401f03944ed712c" ], [ "Vale.SHA.X64.va_quick_Loop_rounds", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "edb5f848e9e0a25db7abe48ff511958c" ], [ "Vale.SHA.X64.va_qcode_Loop_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "982d7596a494a283ead2608d895acee7" ], [ "Vale.SHA.X64.va_lemma_Loop_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b48d4ac423ec5caa6d0f09dc23fe91d8", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "fc03655fbf740290e640216848fd4239" ], [ "Vale.SHA.X64.va_lemma_Loop_body0", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Prims.LexTop@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Decls.validSrcAddrsOffset128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCodes.lexCons", "equation_Vale.X64.QuickCodes.precedes_wrap", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.state_eta", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat64", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_eta", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.validSrcAddrs128", "typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Memory.buffer_addr", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.lexCons", "typing_Vale.X64.QuickCodes.precedes_wrap", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Prims.LexTop@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "well-founded-ordering-on-nat" ], 0, "c7d0aaccdbf8508e94a06f4040901f32" ], [ "Vale.SHA.X64.va_wp_Loop_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "44cdee4d03686886d165a61c10e73c2a" ], [ "Vale.SHA.X64.va_wpProof_Loop_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.X64.va_wp_Loop_body0", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "typing_FStar.Seq.Base.length", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs" ], 0, "95662f3033c6ea28b93538fd803fb35a" ], [ "Vale.SHA.X64.va_quick_Loop_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "30fac09d9e77d2923ce7b9a26d4bbfd8" ], [ "Vale.SHA.X64.va_code_Loop_while0", 1, 1, 0, [ "@query", "constructor_distinct_Vale.X64.Machine_s.OConst", "constructor_distinct_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0" ], 0, "f78dfd277c8bae530b6aac1f76b319f4" ], [ "Vale.SHA.X64.va_qcode_Loop_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "constructor_distinct_Vale.X64.Machine_s.OConst", "constructor_distinct_Vale.X64.Machine_s.OReg", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.OStack", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "beaf67673b9826943cb8032749d9a4bb" ], [ "Vale.SHA.X64.va_lemma_Loop_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_553a30598e7cfb7c658987963368b182", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "3734d2812dd9737f4d032052805e2515" ], [ "Vale.SHA.X64.va_lemma_Loop_while0", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "b2t_typing", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_not", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCodes.precedes_wrap", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.state_eta", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "l_not-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_eta", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Prims.l_not", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.validSrcAddrs128", "typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "184ca884f4db31d9d89b34f74bc4ab7c" ], [ "Vale.SHA.X64.va_wp_Loop_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "fba9a500f27de464f9dd92ad49b7137f" ], [ "Vale.SHA.X64.va_wpProof_Loop_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.X64.va_wp_Loop_while0", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "typing_FStar.Seq.Base.length", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.upd_register", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg" ], 0, "3d816b827b4b255c62bef533984204d0" ], [ "Vale.SHA.X64.va_quick_Loop_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "0f62ba82812f76b90332c4864bc7383f" ], [ "Vale.SHA.X64.va_lemma_Loop", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68ddfba9651945fbb3d5395d252150de", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "9ac2b42c863a68647a5e1914dc420c32" ], [ "Vale.SHA.X64.va_lemma_Loop", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_211facd8812fd94e95b65d3b8891b14a", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Prims.eq2", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel", "typing_Vale.SHA.SHA_helpers.make_hash", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Memory.base_typ_as_vale_type", "typing_Vale.X64.Memory.buffer_addr", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "e12a26568e763d84ec6176207c8bcbba" ], [ "Vale.SHA.X64.va_wp_Loop", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "6ed6ef548f145cbf0f2ad376d71a5858" ], [ "Vale.SHA.X64.va_wpProof_Loop", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.SHA.X64.va_wp_Loop", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.upd_register", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "a91d31ee6cd6ddb1c1810da4669ccc29" ], [ "Vale.SHA.X64.va_quick_Loop", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "9269464957db2f8f5d4f7fe027b12a38" ], [ "Vale.SHA.X64.va_lemma_Epilogue", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Types_s.bits_of_byte", "equation_Vale.Def.Types_s.byte_to_twobits", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Types_s.select_word", "equation_Vale.Def.Types_s.twobits", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.InsVector.buffer128_write", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_buffer_read", "equation_Vale.X64.Memory.valid_buffer_write", "equation_Vale.X64.Memory.valid_layout_buffer", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat2", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.SHA.SHA_helpers.word", "int_inversion", "int_typing", "interpretation_Tm_abs_724e7331c31308c0db7769cc73342745", "interpretation_Tm_abs_fe5e69c993ae4cd67fe2462e7e4d4748", "kinding_Vale.Def.Words_s.four@tok", "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_Lib.IntTypes.pow2_2", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.modifies_buffer_addr", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "lemma_Vale.X64.Memory.modifies_goal_directed_trans2", "lemma_Vale.X64.Memory.modifies_valid_taint", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7", "refinement_interpretation_Tm_refine_52159ea6753e9180a44d69076e7f9cf4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Def.Types_s.byte_to_twobits", "typing_Vale.Def.Types_s.select_word", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Lib.Map16.sel", "typing_Vale.SHA.SHA_helpers.make_hash", "typing_Vale.SHA.SHA_helpers.make_ordered_hash", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.buffer_write", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "1fa8b76bbc9a7745a2671911f51bfe1c" ], [ "Vale.SHA.X64.va_wpProof_Epilogue", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.X64.va_wp_Epilogue", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "5d89e087bb9111c5a764e6fc99a364d7" ], [ "Vale.SHA.X64.va_quick_Epilogue", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "8c482d1da2a613e932d4438de0ffefdc" ], [ "Vale.SHA.X64.va_lemma_Sha_update", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_339af6cc29dd9968a9f9b189ac2ee419", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "d78aced1b8ce11b5ba9301f9621c3395" ], [ "Vale.SHA.X64.va_lemma_Sha_update", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.modifies_buffer_elim", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_211facd8812fd94e95b65d3b8891b14a", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "337b6c1e9b6756e222ea1b8eb59dd7d8" ], [ "Vale.SHA.X64.va_wp_Sha_update", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_self", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "f43f936e6ae4dd46717c99364db2d08c" ], [ "Vale.SHA.X64.va_wpProof_Sha_update", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.X64.va_wp_Sha_update", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "unit_typing" ], 0, "f2598fec61db090b17ae27ee2c46f2e6" ], [ "Vale.SHA.X64.va_quick_Sha_update", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "38c8ee5d5c9dd18a136d9bb8a85a6416" ], [ "Vale.SHA.X64.va_qcode_Sha_update_bytes", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs" ], 0, "3b286d8a31e614e36d45b06bbd3dc835" ], [ "Vale.SHA.X64.va_lemma_Sha_update_bytes", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_289ee2cc5874944bf725b9e3db8c0fd6", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get", "equation_Vale.SHA.SHA_helpers.byte", "equation_Vale.SHA.SHA_helpers.bytes", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Prims.l_and", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "l_and-interp", "lemma_FStar.Seq.Properties.slice_length", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e", "string_typing", "typing_Prims.eq2", "typing_Prims.l_and", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "typing_Vale.Lib.Map16.sel", "typing_Vale.SHA.SHA_helpers.le_bytes_to_hash", "typing_Vale.SHA.SHA_helpers.update_multi_opaque_vale", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.base_typ_as_vale_type", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_length", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion", "unit_typing" ], 0, "e58660bb64da502196837cfe11e5bc36" ], [ "Vale.SHA.X64.va_wpProof_Sha_update_bytes", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.SHA.X64.va_wp_Sha_update_bytes", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Memory.buffer_length", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "444f44d4883aaf2a7582ae3519dcfffd" ], [ "Vale.SHA.X64.va_quick_Sha_update_bytes", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "310d17fa0e18f88eefa1464e242b33d8" ], [ "Vale.SHA.X64.va_req_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "03b41acc60c27d864d05b1ead0cda6f8" ], [ "Vale.SHA.X64.va_ens_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.byte", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "equation_Vale.SHA.X64.va_req_Sha_update_bytes_stdcall", "equation_Vale.X64.Decls.va_state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "unit_typing" ], 0, "37c287822e555ee586653301ace4c5aa" ], [ "Vale.SHA.X64.va_qcode_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "function_token_typing_Prims.__cache_version_number__", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0" ], 0, "414dcb0da729fdf394b23b4bdcc17c04" ], [ "Vale.SHA.X64.va_lemma_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.byte", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "equation_Vale.X64.Decls.va_int_range", "equation_Vale.X64.Decls.va_require_total", "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cbaa862e461df0ff4edfd6ae3330fb67" ], 0, "30fafda1a07b0a8342762b153700f36e" ], [ "Vale.SHA.X64.va_lemma_Sha_update_bytes_stdcall", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42", "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapImpl.Immutable@tok", "equality_tok_Vale.Arch.HeapImpl.Mutable@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eq2", "equation_Prims.l_and", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.byte", "equation_Vale.SHA.SHA_helpers.hash256", "equation_Vale.SHA.SHA_helpers.k_reqs", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.InsMem.create_post", "equation_Vale.X64.InsMem.heaplet_id_is_some", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.buffer_info_disjoint", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.init_heaplets_req", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_taint_buf128", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp", "l_imp-interp", "l_not-interp", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.lemma_heaps_match", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "lemma_Vale.X64.Stack_i.lemma_store_new_valid64", "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "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_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.OReg_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_length", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.layout_buffers", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.store_stack64", "typing_Vale.X64.Stack_i.store_taint_stack64", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapImpl.Immutable@tok", "typing_tok_Vale.Arch.HeapImpl.Mutable@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion", "unit_typing" ], 0, "7811accadacd198854e13db228258d61" ], [ "Vale.SHA.X64.va_wp_Sha_update_bytes_stdcall", 1, 1, 0, [ "@query", "equation_Vale.SHA.SHA_helpers.block_length", "equation_Vale.SHA.SHA_helpers.byte", "equation_Vale.SHA.SHA_helpers.size_block_w_256", "projection_inverse_BoxInt_proj_0" ], 0, "e501d66e00c4e474eefbfb08f4e3e3ed" ], [ "Vale.SHA.X64.va_wpProof_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.SHA.X64.va_wp_Sha_update_bytes_stdcall", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8", "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8", "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62", "interpretation_Tm_abs_9c68c324fd6522aa76063ec2105d06ce", "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd", "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe", "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e", "interpretation_Tm_abs_ef0bc9bf8c01d8ae396f33430ebcf097", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Memory.buffer_length", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.State.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "513bd77dce5faa32f7e938bb97ff946d" ], [ "Vale.SHA.X64.va_quick_Sha_update_bytes_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "63e4bbfb95f6d6680a28c3f9f16a6cec" ] ] ]