[ ">\u0002‹\u0003Z\u001b‹äeŸik–ä\b\u0013", [ [ "Vale.Curve25519.X64.FastWide.va_req_Fmul", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "f25ef60b88af98170476dd28050e6d9a" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fmul", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "14145a8fd7e438a183b411c9ba515a57" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42", "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2", "bool_inversion", "constructor_distinct_Prims.Cons", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapImpl.Immutable@tok", "equality_tok_Vale.Arch.HeapImpl.Mutable@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8", "equation_Vale.X64.Decls.modifies_buffer_specific", "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_mem", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.InsMem.create_post", "equation_Vale.X64.InsMem.heaplet_id_is_some", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.buffer64", "equation_Vale.X64.Memory.buffer_info_disjoint", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.init_heaplets_req", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_taint_buf64", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.lemma_heaps_match", "lemma_Vale.X64.Memory.modifies_buffer_addr", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_same_heaplet_id", "lemma_Vale.X64.Memory.modifies_valid_taint", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.X64.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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "string_typing", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_Prims.eq2", "typing_Prims.l_and", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2", "typing_Vale.Lib.Seqs.list_to_seq", "typing_Vale.X64.CPU_Features_s.bmi2_enabled", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.layout_buffers", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapImpl.Immutable@tok", "typing_tok_Vale.Arch.HeapImpl.Mutable@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "b5345a62ebd302396261f126d02a97aa" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fmul", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fmul", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.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.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "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, "d3afe7a3fb6aa17ebed5988f0bcd5ee2" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fmul", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "4296b48602b0c879c367bafbb8154466" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fmul_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "ea862462f3457dc7c1e62b0714c16eed" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fmul_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "f67b831995b67e660ccfbd1f7d6ac141" ], [ "Vale.Curve25519.X64.FastWide.va_qcode_Fmul_stdcall", 1, 1, 0, [ "@query" ], 0, "85aead3a2c7ca4746542db312d0164c4" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.Memory.get_vale_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "refinement_interpretation_Tm_refine_cd9e7a5b2ee1309676e113b1957fd37c" ], 0, "4b0ed8792fa33e6e40a72cc72c9cadcd" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul_stdcall", 2, 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.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.buffer64", "equation_Vale.X64.Memory.get_vale_heap", "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", "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_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "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", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "lemma_Vale.X64.Stack_i.lemma_store_new_valid64", "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64", "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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "8c3f355a468b0af62b629443d1926b5c" ], [ "Vale.Curve25519.X64.FastWide.va_wp_Fmul_stdcall", 1, 1, 0, [ "@query" ], 0, "fb590758130596759e61609cd2221d22" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fmul_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fmul_stdcall", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8", "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8", "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62", "interpretation_Tm_abs_9c68c324fd6522aa76063ec2105d06ce", "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd", "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe", "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e", "interpretation_Tm_abs_ef0bc9bf8c01d8ae396f33430ebcf097", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "1aa9ae501770885d9c66dedb8276cdd7" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fmul_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "92ebcd708e032cbe8ce50f7afe41e7aa" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fmul2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "31a6edabd3a2df5ab6c4e5768a0889a1" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fmul2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "4c04c87e53d4f96393a14311db4446d8" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul2", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42", "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2", "bool_inversion", "constructor_distinct_Prims.Cons", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapImpl.Immutable@tok", "equality_tok_Vale.Arch.HeapImpl.Mutable@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8", "equation_Vale.X64.Decls.modifies_buffer_specific", "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_mem", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.InsMem.create_post", "equation_Vale.X64.InsMem.heaplet_id_is_some", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.buffer64", "equation_Vale.X64.Memory.buffer_info_disjoint", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.init_heaplets_req", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_taint_buf64", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.lemma_heaps_match", "lemma_Vale.X64.Memory.modifies_buffer_addr", "lemma_Vale.X64.Memory.modifies_buffer_elim", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_same_heaplet_id", "lemma_Vale.X64.Memory.modifies_valid_taint", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.X64.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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "string_typing", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Prims.l_and", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2", "typing_Vale.Lib.Seqs.list_to_seq", "typing_Vale.X64.CPU_Features_s.bmi2_enabled", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.layout_buffers", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapImpl.Immutable@tok", "typing_tok_Vale.Arch.HeapImpl.Mutable@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "f24cf00ce35b4482d94a252c51a9163f" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fmul2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fmul2", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.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.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "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, "f0c5a87659a1aed149ebc104d93c3a4b" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fmul2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "607216cc2be262ac00256eb6b52e85fa" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fmul2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "58c6ea4124bb838c5ef05bc32f7f3dad" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fmul2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "625e19493e29af62c0579b814deeecf9" ], [ "Vale.Curve25519.X64.FastWide.va_qcode_Fmul2_stdcall", 1, 1, 0, [ "@query" ], 0, "ac76f6ebebed36f03f7945182d9e60ec" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.Memory.get_vale_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "refinement_interpretation_Tm_refine_517fbeea0eff364d52b82ef78ca88175" ], 0, "1ba9c7d87c683018348ce039c9d62f63" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fmul2_stdcall", 2, 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.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.buffer64", "equation_Vale.X64.Memory.get_vale_heap", "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", "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_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "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", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "lemma_Vale.X64.Stack_i.lemma_store_new_valid64", "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64", "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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "fa0d11f7fa57ecbe0b58fa56f26450b9" ], [ "Vale.Curve25519.X64.FastWide.va_wp_Fmul2_stdcall", 1, 1, 0, [ "@query" ], 0, "80c89611d0bba9d9b1a4722d3639f21f" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fmul2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fmul2_stdcall", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8", "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8", "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62", "interpretation_Tm_abs_9c68c324fd6522aa76063ec2105d06ce", "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd", "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe", "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e", "interpretation_Tm_abs_ef0bc9bf8c01d8ae396f33430ebcf097", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "5958f0d3dae4c656adc5fd9d4493927a" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fmul2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "da7d2fc204b13048a17e8c703bf0c733" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fsqr", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "f4fe8ae1a7d1bdaf3fdd695ec29e37f0" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fsqr", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "65993d189893cd88375ad48c0b73fb3b" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42", "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2", "bool_inversion", "constructor_distinct_Prims.Cons", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapImpl.Immutable@tok", "equality_tok_Vale.Arch.HeapImpl.Mutable@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8", "equation_Vale.X64.Decls.modifies_buffer_specific", "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_mem", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.InsMem.create_post", "equation_Vale.X64.InsMem.heaplet_id_is_some", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_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.buffer64", "equation_Vale.X64.Memory.buffer_info_disjoint", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.init_heaplets_req", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_taint_buf64", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.lemma_heaps_match", "lemma_Vale.X64.Memory.modifies_buffer_addr", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_same_heaplet_id", "lemma_Vale.X64.Memory.modifies_valid_taint", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.X64.Machine_s.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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "string_typing", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_Prims.eq2", "typing_Prims.l_and", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2", "typing_Vale.Lib.Seqs.list_to_seq", "typing_Vale.X64.CPU_Features_s.bmi2_enabled", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.layout_buffers", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapImpl.Immutable@tok", "typing_tok_Vale.Arch.HeapImpl.Mutable@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "a36521203e8f198afd3908f9de9ddef6" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fsqr", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fsqr", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.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.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "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, "f9e3ae261a3eba6a8cd7654548d11ac8" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fsqr", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "2688e639405ab3f2944251b3ac162ecf" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fsqr_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "61e3635a95b4b3de2dcdea0624d062dd" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fsqr_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "335531ac5df2fccf2fcc975f1d2a1438" ], [ "Vale.Curve25519.X64.FastWide.va_qcode_Fsqr_stdcall", 1, 1, 0, [ "@query" ], 0, "c77a1a26dabf3f77d8221a5e154ba1a2" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.Memory.get_vale_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "refinement_interpretation_Tm_refine_df2a2211e22d683bfc5455476189e24f" ], 0, "fb91ec38824fa074b9c26348c80f8d87" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr_stdcall", 2, 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.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.buffer64", "equation_Vale.X64.Memory.get_vale_heap", "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", "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_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "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", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "lemma_Vale.X64.Stack_i.lemma_store_new_valid64", "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64", "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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "744ffd383663cbf38870357e90069e14" ], [ "Vale.Curve25519.X64.FastWide.va_wp_Fsqr_stdcall", 1, 1, 0, [ "@query" ], 0, "6b3773b105c33747d53f6207eb515ee7" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fsqr_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fsqr_stdcall", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8", "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8", "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62", "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd", "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe", "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "f125e35096971e862a95ae954eb9b17d" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fsqr_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "9329f2820a5eb30a2636da22eeef405f" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fsqr2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "0e2478c44d2fcbc8bf03627bd8754bf0" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fsqr2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "8fc6a0dcea6572bf79c8afd4f31f2f3c" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr2", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42", "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2", "bool_inversion", "constructor_distinct_Prims.Cons", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equality_tok_Vale.Arch.HeapImpl.Immutable@tok", "equality_tok_Vale.Arch.HeapImpl.Mutable@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8", "equation_Vale.X64.Decls.modifies_buffer_specific", "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_mem", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.InsMem.create_post", "equation_Vale.X64.InsMem.heaplet_id_is_some", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_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.buffer64", "equation_Vale.X64.Memory.buffer_info_disjoint", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.init_heaplets_req", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Memory.valid_taint_buf64", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Memory.lemma_heaps_match", "lemma_Vale.X64.Memory.modifies_buffer_addr", "lemma_Vale.X64.Memory.modifies_buffer_elim", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_same_heaplet_id", "lemma_Vale.X64.Memory.modifies_valid_taint", "lemma_Vale.X64.QuickCodes.lemma_label_bool", "lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "proj_equation_Vale.X64.Machine_s.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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint", "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "string_typing", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.Seq.Base.length", "typing_Prims.eq2", "typing_Prims.l_and", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint", "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2", "typing_Vale.Lib.Seqs.list_to_seq", "typing_Vale.X64.CPU_Features_s.bmi2_enabled", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.layout_buffers", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_tok_Vale.Arch.HeapImpl.Immutable@tok", "typing_tok_Vale.Arch.HeapImpl.Mutable@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "3346dd6043c27a559adea58e6689c961" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fsqr2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fsqr2", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.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.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "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, "c378ddaf9b59f4e11a1ea16c2361e784" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fsqr2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "51d00c79ed2acb4ccf4231998e76875b" ], [ "Vale.Curve25519.X64.FastWide.va_req_Fsqr2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "cf47573c0f6e5b896341ed2629233f38" ], [ "Vale.Curve25519.X64.FastWide.va_ens_Fsqr2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "7941992561bb7f7bd0c1e593ca59baac" ], [ "Vale.Curve25519.X64.FastWide.va_qcode_Fsqr2_stdcall", 1, 1, 0, [ "@query" ], 0, "34da4dcf6c4cb8d28d2e842ae18a0a9e" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs64", "equation_Vale.X64.Memory.get_vale_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "refinement_interpretation_Tm_refine_797fac492e298d6da118587f4c1d816e" ], 0, "66b81e0d18aeec6cd785b20fd9c2b082" ], [ "Vale.Curve25519.X64.FastWide.va_lemma_Fsqr2_stdcall", 2, 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.TUInt64@tok", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.l_imp", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.buffer64", "equation_Vale.X64.Memory.get_vale_heap", "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", "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_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion", "int_typing", "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", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64", "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "lemma_Vale.X64.Stack_i.lemma_store_new_valid64", "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64", "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.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "string_typing", "typing_Prims.eq2", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Memory.modifies", "typing_Vale.X64.QuickCodes.label", "typing_Vale.X64.QuickCodes.va_range1", "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing" ], 0, "87acb6b4e8d3ab1b4cb1c9cee74d2106" ], [ "Vale.Curve25519.X64.FastWide.va_wp_Fsqr2_stdcall", 1, 1, 0, [ "@query" ], 0, "a65cea742f29e904de0825fb1cae26b8" ], [ "Vale.Curve25519.X64.FastWide.va_wpProof_Fsqr2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Curve25519.X64.FastWide.va_wp_Fsqr2_stdcall", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs64", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs64", "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.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8", "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8", "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62", "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd", "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe", "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_flags", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_mem_heaplet", "typing_Vale.X64.Decls.va_upd_mem_layout", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.State.update_reg", "unit_typing" ], 0, "b59cecbf5b4ead56871eba9ca926d4af" ], [ "Vale.Curve25519.X64.FastWide.va_quick_Fsqr2_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "2c6432c5d1bd541e1d9a77fff1680e0f" ] ] ]