[ "0Òü\u0003—cóºbˆy¡õ@šX", [ [ "Vale.AES.X64.AESopt2.scratch_b_blocks", 1, 1, 0, [ "@query" ], 0, "5c8ca525c82afde1b1b0da2f5864b882" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_step", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "equation_Prims.nat", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.CPU_Features_s.avx_enabled" ], 0, "bd35fe05e13517e8f7afd45f90840177" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_step", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b", "Vale.AES.GHash_interpretation_Tm_arrow_e08d3fabe0cebf63a55bab906bc9480d", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "constructor_distinct_Vale.X64.Machine_s.Block", "constructor_distinct_Vale.X64.Machine_s.MReg", "constructor_distinct_Vale.X64.Machine_s.OMem", "constructor_distinct_Vale.X64.Machine_s.OReg", "data_typing_intro_Vale.X64.Machine_s.MReg@tok", "data_typing_intro_Vale.X64.Machine_s.OReg@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "equation_Vale.AES.GHash.poly128", "equation_Vale.Arch.HeapImpl.heaplet_id", "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.CPU_Features_s.sse_enabled", "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.Decls.valid_buf_maddr128", "equation_Vale.X64.Decls.valid_mem_operand128", "equation_Vale.X64.Decls.valid_operand128", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.operand128", "equation_Vale.X64.Machine_s.operand64", "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.Machine_s.t_reg_to_int", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.get_vale_heap", "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.State.eval_maddr", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.eval_operand128", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_xmm", "equation_Vale.X64.State.valid_src_operand128", "equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "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_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat64", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144", "kinding_Vale.Def.Words_s.four@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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.MReg_offset", "projection_inverse_Vale.X64.Machine_s.MReg_r", "projection_inverse_Vale.X64.Machine_s.OMem_m", "projection_inverse_Vale.X64.Machine_s.OMem_tc", "projection_inverse_Vale.X64.Machine_s.OMem_tr", "projection_inverse_Vale.X64.Machine_s.OReg_r", "projection_inverse_Vale.X64.Machine_s.OReg_tc", "projection_inverse_Vale.X64.Machine_s.OReg_tr", "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_3070833ad63c2d9af4addc8393937324", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "true_interp", "typing_FStar.Seq.Base.length", "typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.sse4_1_enabled", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.InsVector.va_code_Mem128_lemma", "typing_Vale.X64.InsVector.va_lemma_Mem128_lemma", "typing_Vale.X64.Memory.base_typ_as_vale_type", "typing_Vale.X64.Memory.buffer_addr", "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_Vale.X64.State.eval_maddr", "typing_Vale.X64.State.eval_operand", "typing_Vale.X64.State.eval_operand128", "typing_Vale.X64.State.update_reg", "typing_Vale.X64.State.update_reg_xmm", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "018c575caacefbe5f7562adb6c7510fc" ], [ "Vale.AES.X64.AESopt2.va_wp_MulAdd_step", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "37cc81bee2cc9e6183cead061136f43b" ], [ "Vale.AES.X64.AESopt2.va_wpProof_MulAdd_step", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.AES.X64.AESopt2.va_wp_MulAdd_step", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "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_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_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "interpretation_Tm_abs_3f6e482b335232017bc52fd2f46c873d", "interpretation_Tm_abs_597606c564b47fb87fb32e90b12eb571", "interpretation_Tm_abs_8669db4e848bec7d496f888f75136856", "interpretation_Tm_abs_ed6d0e419459456a33e996d20caefe71", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "primitive_Prims.op_Equality", "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_BoxBool_proj_0", "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.CPU_Features_s.avx_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", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "6c3817c43568d31064015c5448141981" ], [ "Vale.AES.X64.AESopt2.va_quick_MulAdd_step", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "f81e8694bdde1bb97904fe8cc6baac6e" ], [ "Vale.AES.X64.AESopt2.va_qcode_MulAdd_unroll_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "primitive_Prims.op_GreaterThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "650e198f8bd6dba71f93d50d33496d07" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f26e21a6f2e44168aacf3c1b38e9ab08" ], 0, "cda932f75788c4f0a869403d6f15b3a8" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll_i", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b", "Vale.AES.GHash_interpretation_Tm_arrow_e08d3fabe0cebf63a55bab906bc9480d", "b2t_def", "bool_inversion", "bool_typing", "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_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "equation_Vale.AES.GHash.poly128", "equation_Vale.AES.X64.AESopt2.index_opt_rev", "equation_Vale.AES.X64.AESopt2.quad32_opt_rev", "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.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_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.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", "equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "interpretation_Tm_abs_123c1a5163fc256d7d016e4edc552e21", "interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144", "interpretation_Tm_abs_2d8fb4d5989ffbd80b3415d0a3c649fc", "interpretation_Tm_abs_3e030d5d4967980168d3804a77b4cb65", "interpretation_Tm_abs_5ffce3adededdc5467795e6924e4d26f", "interpretation_Tm_abs_6fd0c5b43664c088eb63a43ea4f760b9", "interpretation_Tm_abs_71ac58aaf99a8a6690ce956a082a9a1c", "interpretation_Tm_abs_ad9915ab071893bd05d70a3a9778882f", "interpretation_Tm_abs_b605c3e960084ffb6cda376bbb4a6dd5", "interpretation_Tm_abs_d3ee1c9356f9ebd1b016900a8f6ef7dc", "interpretation_Tm_abs_f2ee72ed45f10ade38408b5c1dbcbeda", "kinding_Vale.Def.Words_s.four@tok", "l_imp-interp", "l_not-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "lemma_Vale.Math.Poly2.lemma_add_degree", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "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.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_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_Vale.AES.GHash.ghash_unroll_back", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Math.Poly2.Bits_s.of_quad32", "typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.poly", "typing_Vale.Math.Poly2_s.shift", "typing_Vale.X64.CPU_Features_s.sse4_1_enabled", "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.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", "unit_inversion", "unit_typing" ], 0, "4ccd84246ea78a71c8956f3fdaaf15ae" ], [ "Vale.AES.X64.AESopt2.va_wp_MulAdd_unroll_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "int_inversion" ], 0, "e6e64a09fc53fa3fde5114615023cd4b" ], [ "Vale.AES.X64.AESopt2.va_wpProof_MulAdd_unroll_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.AES.X64.AESopt2.va_wp_MulAdd_unroll_i", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "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.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_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "interpretation_Tm_abs_596f7608f35e91f4354888144e27cd61", "interpretation_Tm_abs_5ffce3adededdc5467795e6924e4d26f", "interpretation_Tm_abs_71ac58aaf99a8a6690ce956a082a9a1c", "interpretation_Tm_abs_e56d7aec68177a18f923a13452b6004e", "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.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, "cd344b1ecf21a662e6e4eb24a4c6adc4" ], [ "Vale.AES.X64.AESopt2.va_quick_MulAdd_unroll_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "8b104f9dba8fad902b715b319b325eaa" ], [ "Vale.AES.X64.AESopt2.va_code_MulAdd_unroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@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", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703" ], 0, "234501b1d058b1070e9f9b08f5c8c8a8" ], [ "Vale.AES.X64.AESopt2.va_qcode_MulAdd_unroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.X64.Machine_s.OConst", "constructor_distinct_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.nat", "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.Machine_s.reg_64", "function_token_typing_Vale.Def.Words_s.nat32", "kinding_Vale.Def.Words_s.four@tok", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.Seq.Base.length" ], 0, "ba72c54e6395fdabd5e909f10c95982a" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_dd54464bc13c30978673ebcbc382c6c4" ], 0, "4d5c7102bc8e15a0ea5d5cc7e52bf113" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll_n", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "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_imp", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.index_opt_rev", "equation_Vale.AES.X64.AESopt2.quad32_opt_rev", "equation_Vale.AES.X64.AESopt2.scratch_b_blocks", "equation_Vale.AES.X64.AESopt2.scratch_b_data", "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.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_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", "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_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "interpretation_Tm_abs_596f7608f35e91f4354888144e27cd61", "interpretation_Tm_abs_5ffce3adededdc5467795e6924e4d26f", "interpretation_Tm_abs_71ac58aaf99a8a6690ce956a082a9a1c", "interpretation_Tm_abs_e56d7aec68177a18f923a13452b6004e", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "l_imp-interp", "l_not-interp", "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", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "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.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_r", "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", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "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_FStar.Seq.Base.length", "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_ok", "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", "unit_typing" ], 0, "7a4212079623af56d3dd1b85732a04bd" ], [ "Vale.AES.X64.AESopt2.va_wp_MulAdd_unroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Vale.Def.Words_s.nat32", "kinding_Vale.Def.Words_s.four@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.Seq.Base.length" ], 0, "462df3aca8186fb3ad55eec046aacf74" ], [ "Vale.AES.X64.AESopt2.va_wpProof_MulAdd_unroll_n", 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.AES.X64.AESopt2.va_wp_MulAdd_unroll_n", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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.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.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, "dd5c345108164f16496fa43784b05957" ], [ "Vale.AES.X64.AESopt2.va_quick_MulAdd_unroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "74accf1eca6428e1e7d50504bbfeb89e" ], [ "Vale.AES.X64.AESopt2.va_qcode_MulAdd_unroll", 1, 1, 0, [ "@query" ], 0, "9f5e4bfb2ae0d6400defa295bdc05ef0" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "6bd0bc56e85bc2366d23ab6dc0de4358" ], [ "Vale.AES.X64.AESopt2.va_lemma_MulAdd_unroll", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b", "Vale.AES.GHash_interpretation_Tm_arrow_e08d3fabe0cebf63a55bab906bc9480d", "bool_inversion", "bool_typing", "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.AES.GHash.fun_seq_quad32_LE_poly128", "equation_Vale.AES.GHash.poly128", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.index_opt_rev", "equation_Vale.AES.X64.AESopt2.quad32_opt_rev", "equation_Vale.AES.X64.AESopt2.scratch_b_blocks", "equation_Vale.AES.X64.AESopt2.scratch_b_data", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.insert_nat32", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_insert", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.get", "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.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Machine_s.t_reg_to_int", "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_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "interpretation_Tm_abs_1042507aa3d97d7ea94b078e8fd7ed52", "interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144", "interpretation_Tm_abs_9900b7be49b9243f58b31bc7b47d33bb", "interpretation_Tm_abs_ad9915ab071893bd05d70a3a9778882f", "interpretation_Tm_abs_d3ee1c9356f9ebd1b016900a8f6ef7dc", "kinding_Vale.Def.Words_s.four@tok", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "lemma_Vale.Math.Poly2.lemma_add_degree", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "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_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "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.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_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.OReg_r", "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_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.AES.GHash.ghash_unroll_back", "typing_Vale.AES.X64.AESopt2.index_opt_rev", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Lib.Map16.sel", "typing_Vale.Math.Poly2.Bits_s.of_quad32", "typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.poly", "typing_Vale.Math.Poly2_s.shift", "typing_Vale.X64.CPU_Features_s.sse4_1_enabled", "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, "c501107889decbbd1e7f040a2a68fb1a" ], [ "Vale.AES.X64.AESopt2.va_wp_MulAdd_unroll", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "323888416d25c49ad227dce56045e020" ], [ "Vale.AES.X64.AESopt2.va_wpProof_MulAdd_unroll", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.AES.X64.AESopt2.va_wp_MulAdd_unroll", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "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.Def.Words_s.nat32", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "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_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_ok", "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, "edc3871e0a5ce4754834385b93ae2232" ], [ "Vale.AES.X64.AESopt2.va_quick_MulAdd_unroll", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "1ca8e79e8b13f23242778f56f8028b97" ], [ "Vale.AES.X64.AESopt2.va_qcode_Reduce", 1, 1, 0, [ "@query" ], 0, "e996685c0e43621e435db73b85d45ccd" ], [ "Vale.AES.X64.AESopt2.va_lemma_Reduce", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equation_Prims.eq2", "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.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_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.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.State.state_eq", "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", "interpretation_Tm_abs_7548440acfd5dc6e8fc39251d83a5244", "interpretation_Tm_abs_78661a0cf2d6a7591887cfbe96dfa840", "interpretation_Tm_abs_96a4ac7557fcfb6abd2f40a0b7d8576d", "interpretation_Tm_abs_ad9915ab071893bd05d70a3a9778882f", "interpretation_Tm_abs_bb568a473f658d2865f0a1b33e1663c7", "interpretation_Tm_abs_c7b23c431685e872445565f4eb56b689", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "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.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.X64.Machine_s.Reg_rf", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Math.Poly2_s.poly_index", "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_inversion", "unit_typing" ], 0, "38e016d9f72a441aa13f847515b80c1f" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Reduce", 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.AES.X64.AESopt2.va_wp_Reduce", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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_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", "interpretation_Tm_abs_75bc6c3c432275052c6e3d5eac834ca9", "interpretation_Tm_abs_7c4c81e8cb4e7b9fb9f66b6de6e04cea", "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.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, "b3cba25ee46ca5f376e2e05d4d7156e1" ], [ "Vale.AES.X64.AESopt2.va_quick_Reduce", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "a1e533ec0399b79e1ed0e6b1bc453445" ], [ "Vale.AES.X64.AESopt2.va_qcode_ReduceLast", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "primitive_Prims.op_GreaterThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "b5be54c7e5e9442ea7cb08c61c12d0d5" ], [ "Vale.AES.X64.AESopt2.va_lemma_ReduceLast", 1, 1, 0, [ "@query" ], 0, "c0301d0ec46de3722b3765c37b870fbd" ], [ "Vale.AES.X64.AESopt2.va_lemma_ReduceLast", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equation_Prims.eq2", "equation_Prims.l_and", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GF128.gf128_low_shift", "equation_Vale.AES.GF128.mod_rev", "equation_Vale.AES.GF128_s.gf128_modulus", "equation_Vale.AES.GF128_s.gf128_modulus_low_terms", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "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_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.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_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "interpretation_Tm_abs_7548440acfd5dc6e8fc39251d83a5244", "interpretation_Tm_abs_78661a0cf2d6a7591887cfbe96dfa840", "interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "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.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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.X64.CPU_Features_s.avx_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_inversion", "unit_typing" ], 0, "805c73f8e8a19c158d411057224ac1e9" ], [ "Vale.AES.X64.AESopt2.va_wp_ReduceLast", 1, 1, 0, [ "@query" ], 0, "8f29048491a97580bba42bdb17a0152b" ], [ "Vale.AES.X64.AESopt2.va_wpProof_ReduceLast", 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.AES.X64.AESopt2.va_wp_ReduceLast", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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_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", "interpretation_Tm_abs_75bc6c3c432275052c6e3d5eac834ca9", "interpretation_Tm_abs_7c4c81e8cb4e7b9fb9f66b6de6e04cea", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32", "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.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, "494c04ef2cd0f5ff19a355a735a748d6" ], [ "Vale.AES.X64.AESopt2.va_quick_ReduceLast", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "d94f6b3d366d07744afdb6bbbd2eb1a1" ], [ "Vale.AES.X64.AESopt2.va_lemma_GhashUnroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "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_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.insert_nat32", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_insert", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.get", "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.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", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_be5d70634f1f3f1f083b59d3e8c8c39d", "l_and-interp", "l_imp-interp", "l_not-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32", "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.Def.Words_s.Mkfour_hi2", "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_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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "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, "07bdf0ba4896cef1d3d082998e36ebb1" ], [ "Vale.AES.X64.AESopt2.va_wpProof_GhashUnroll_n", 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.AES.X64.AESopt2.va_wp_GhashUnroll_n", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "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.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.Def.Words_s.four", "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.AES.GHash.ghash_incremental", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_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", "unit_typing" ], 0, "3150d291400c8de666f14f3f9bcef261" ], [ "Vale.AES.X64.AESopt2.va_quick_GhashUnroll_n", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "a506181f82f949abe671d1073b52ae7e" ], [ "Vale.AES.X64.AESopt2.va_qcode_Ghash_register", 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, "4ba9bd753d036501cd264923238e46c7" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_register", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "bool_typing", "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_Vale.AES.GF128.gf128_low_shift", "equation_Vale.AES.GF128.mod_rev", "equation_Vale.AES.GF128_s.gf128_modulus", "equation_Vale.AES.GF128_s.gf128_modulus_low_terms", "equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.insert_nat32", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_insert", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.get", "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.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_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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.nat32", "int_typing", "interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144", "interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c", "interpretation_Tm_abs_ad9915ab071893bd05d70a3a9778882f", "interpretation_Tm_abs_be5d70634f1f3f1f083b59d3e8c8c39d", "interpretation_Tm_abs_d3ee1c9356f9ebd1b016900a8f6ef7dc", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree", "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "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_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "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.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_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.X64.Machine_s.OReg_r", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "string_typing", "token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_FStar.Seq.Base.create", "typing_Prims.eq2", "typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c", "typing_Vale.AES.GF128_s.gf128_modulus_low_terms", "typing_Vale.AES.GHash.fun_seq_quad32_LE_poly128", "typing_Vale.AES.GHash.ghash_incremental", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Lib.Map16.sel", "typing_Vale.Math.Poly2.Bits_s.of_quad32", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.poly_index", "typing_Vale.X64.CPU_Features_s.avx_enabled", "typing_Vale.X64.CPU_Features_s.sse4_1_enabled", "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, "e17c500e14e9f5080ef22245d778b84f" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Ghash_register", 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.AES.X64.AESopt2.va_wp_Ghash_register", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "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_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, "5e850f32389e99c409950d472f099fd4" ], [ "Vale.AES.X64.AESopt2.va_quick_Ghash_register", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "c26fc48ba56e15433c248b44ac6fae60" ], [ "Vale.AES.X64.AESopt2.va_qcode_Ghash_buffer_loop_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_Prims.nat", "equation_Prims.squash", "int_inversion", "l_and-interp", "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, "30c824ba78786df99ba0e44cdb81aa24" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_loop_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.Decls.va_require_total", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "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", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e014bbd008089f182718bd24cddbce9d", "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, "1ff136da61002388887d195823fe0ff2" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_loop_body", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "bool_typing", "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_FStar.Seq.Base.op_At_Bar", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GHash.ghash_incremental0", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.index_opt_rev", "equation_Vale.AES.X64.AESopt2.quad32_opt_rev", "equation_Vale.AES.X64.AESopt2.scratch_b_blocks", "equation_Vale.AES.X64.AESopt2.scratch_b_data", "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.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", "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_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", "int_inversion", "int_typing", "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_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32", "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_GreaterThan", "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_2a09f2450e26fe8d9312d402cf7d7936", "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_ac201cf927190d39c033967b63cb957b", "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", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_FStar.Seq.Base.slice", "typing_Prims.eq2", "typing_Vale.AES.GHash.ghash_incremental", "typing_Vale.AES.GHash.ghash_incremental0", "typing_Vale.AES.X64.AESopt2.hkeys_b_powers", "typing_Vale.AES.X64.AESopt2.index_opt_rev", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Lib.Map16.sel", "typing_Vale.Math.Poly2.Bits_s.of_quad32", "typing_Vale.X64.Decls.validSrcAddrs128", "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.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion", "unit_typing" ], 0, "e180b051ea6e1a3c4e49fec3a28d8eee" ], [ "Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_loop_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "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.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.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "e68ad06c84c299dd3c0febd558f99cda" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Ghash_buffer_loop_body", 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.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_loop_body", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "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.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_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_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.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, "8fb2e1efbdb27c3d8f4db79bd207e8c8" ], [ "Vale.AES.X64.AESopt2.va_quick_Ghash_buffer_loop_body", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "ed15b25abb91ee9d9d42e15790964b0b" ], [ "Vale.AES.X64.AESopt2.va_qcode_Ghash_buffer_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "54d38eb7acdc415c4de6414f5687ffef" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_require_total", "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.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.X64.Machine_s.Reg_rf", "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", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_301dbb0b801a1c8c1a1cb443c901f184", "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_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "0434820f339fe2054a2674cdb1b5c1b3" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_body0", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "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.AES.X64.AESopt2.hkeys_b_powers", "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.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.Def.Words_s.nat64", "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", "lemma_Vale.X64.Regs.lemma_eta", "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_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.AES.X64.AESopt2.hkeys_b_powers", "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.QuickCodes.label", "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_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "well-founded-ordering-on-nat" ], 0, "7c5f019bf832654c47ebd77509f3ad61" ], [ "Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.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.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.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.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_reg64", "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, "005ef686c3f6f67375bb266502a62454" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Ghash_buffer_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.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_body0", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "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.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_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_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.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, "b6a574eaf88dcb956693e2f9967231e5" ], [ "Vale.AES.X64.AESopt2.va_quick_Ghash_buffer_body0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "f6d6c4c243e6b9d3401c5f652dd76e72" ], [ "Vale.AES.X64.AESopt2.va_code_Ghash_buffer_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, "7e2cb26c6283963ebe947e5dd2959d90" ], [ "Vale.AES.X64.AESopt2.va_qcode_Ghash_buffer_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "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.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.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_inversion", "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_BarBar", "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_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, "c265ab05583aff52f0e7e418e4638c53" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.va_require_total", "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.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "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.X64.Machine_s.Reg_rf", "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", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_aaa1dc280345354c66be6be89aaece16", "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.Memory.buffer_length", "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, "fd4c33e7b039ea5bdd414f22dca180fe" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer_while0", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "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.l_False", "equation_Prims.l_imp", "equation_Prims.l_not", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "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.Lib.Map16.sel16", "equation_Vale.X64.Decls.state_inv", "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.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", "false_interp", "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", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_imp-interp", "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_GreaterThanOrEqual", "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_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Prims.eq2", "typing_Prims.l_imp", "typing_Vale.AES.GHash.ghash_incremental0", "typing_Vale.AES.X64.AESopt2.hkeys_b_powers", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.upd_register", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.validSrcAddrs128", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_length", "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, "9e0d32c1ff190476bdd7451a2bb63345" ], [ "Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "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.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.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.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.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_reg64", "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, "7ff8fb9230b777e78a3e6d9a7ce6908f" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Ghash_buffer_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.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.va_wp_Ghash_buffer_while0", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "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.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_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_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.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, "e3d2b4e5f5c576421ba8c99cfeb17321" ], [ "Vale.AES.X64.AESopt2.va_quick_Ghash_buffer_while0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "5e594a1aa545ca6a6709b1f34c364710" ], [ "Vale.AES.X64.AESopt2.va_code_Ghash_buffer", 1, 1, 0, [ "@MaxIFuel_assumption", "@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", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703" ], 0, "cca7b65f702b432b86db91922deb6f37" ], [ "Vale.AES.X64.AESopt2.va_qcode_Ghash_buffer", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_Vale.X64.Machine_s.OConst", "constructor_distinct_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.squash", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703" ], 0, "8b89f458d96e10bb0a1fc4e41d107dfa" ], [ "Vale.AES.X64.AESopt2.va_lemma_Ghash_buffer", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Def.Types_s_interpretation_Tm_arrow_f33a1e80d097b65957309e13d3848492", "bool_inversion", "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_FStar.Seq.Base.op_At_Bar", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.AES.GHash.ghash_incremental0", "equation_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.AES.X64.AESopt2.index_opt_rev", "equation_Vale.AES.X64.AESopt2.quad32_opt_rev", "equation_Vale.AES.X64.AESopt2.scratch_b_blocks", "equation_Vale.AES.X64.AESopt2.scratch_b_data", "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.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", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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.Types_s.reverse_bytes_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_imp-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32", "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_GreaterThan", "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_2a09f2450e26fe8d9312d402cf7d7936", "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_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "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", "string_typing", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Prims.eq2", "typing_Prims.l_imp", "typing_Vale.AES.GHash.ghash_incremental", "typing_Vale.AES.GHash.ghash_incremental0", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.CPU_Features_s.avx_enabled", "typing_Vale.X64.Memory.buffer_addr", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.buffer_length", "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, "7d04021844360cf0f8c16209bba744b6" ], [ "Vale.AES.X64.AESopt2.va_wpProof_Ghash_buffer", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.nat", "equation_Vale.AES.X64.AESopt2.va_wp_Ghash_buffer", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "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.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.Def.Words_s.four", "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.AES.GHash.ghash_incremental0", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Memory.buffer_as_seq", "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, "8a94e0ba8232bb6047d521f0f30d917c" ], [ "Vale.AES.X64.AESopt2.va_quick_Ghash_buffer", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "7c120bacc144aac9fb65137b29952fae" ], [ "Vale.AES.X64.AESopt2.va_lemma_GhashUnroll6x", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "49ccd4397b949d58c6a5500bfef6bf62" ], [ "Vale.AES.X64.AESopt2.va_lemma_GhashUnroll6x", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "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_Vale.AES.X64.AESopt2.hkeys_b_powers", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Map16.get", "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_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.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", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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", "interpretation_Tm_abs_be5d70634f1f3f1f083b59d3e8c8c39d", "kinding_Vale.Def.Words_s.four@tok", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32", "lemma_Vale.X64.Flags.lemma_equal_intro", "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.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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Vale.AES.GHash.ghash_incremental", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "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", "unit_typing" ], 0, "390e60d19674d60fd59d56bc9fcbbfa5" ], [ "Vale.AES.X64.AESopt2.va_wp_GhashUnroll6x", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "510b60d950f4273ca47d4d14521ab591" ], [ "Vale.AES.X64.AESopt2.va_wpProof_GhashUnroll6x", 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.AES.X64.AESopt2.va_wp_GhashUnroll6x", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "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.Def.Words_s.four", "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", "kinding_Vale.Def.Words_s.four@tok", "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_FStar.Seq.Base.length", "typing_Vale.AES.GHash.ghash_incremental", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "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_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, "0854a67b42ad6a99b6d29750ee39bf52" ], [ "Vale.AES.X64.AESopt2.va_quick_GhashUnroll6x", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "17dc5ef355bd102c0d3f4c879bef3bfc" ] ] ]