[ "¾•ƒ\u001b1ûB¢{üwgÖâ\u0015±", [ [ "Vale.Stdcalls.X64.Fsub.z3rlimit_hack", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "dc74ae564c2db618916f711552e43b8b" ], [ "Vale.Stdcalls.X64.Fsub.as_t", 1, 1, 0, [ "@query" ], 0, "db91d00bae50a0c7af78abdb3d49db9d" ], [ "Vale.Stdcalls.X64.Fsub.as_normal_t", 1, 1, 0, [ "@query" ], 0, "297c4faafce1bd7e57dbd8acfea2d41e" ], [ "Vale.Stdcalls.X64.Fsub.dom", 1, 1, 0, [ "@query", "equation_Vale.Interop.X64.max_stdcall", "projection_inverse_BoxInt_proj_0" ], 0, "d93af70deae7376b16d1b7c0b8c7e502" ], [ "Vale.Stdcalls.X64.Fsub.fsub_lemma'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.Curve25519.X64.FastHybrid.va_ens_Fsub_stdcall", "equation_Vale.Curve25519.X64.FastHybrid.va_req_Fsub_stdcall", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.Fsub.b64", "equation_Vale.Stdcalls.X64.Fsub.fsub_post", "equation_Vale.Stdcalls.X64.Fsub.fsub_pre", "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.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.reg_xmm", "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.set_vale_heap", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_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", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.Interop.X64.regs_modified_stdcall", "int_typing", "interpretation_Tm_abs_138091b81012b0bbcb716913bf498356", "interpretation_Tm_abs_a810575fd82014589fda340470b8b592", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Reg_rf", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_a061d567099c8c8fb98feba0ebc93653", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Curve25519.X64.FastHybrid.va_lemma_Fsub_stdcall", "typing_Vale.Interop.Assumptions.win", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.view_n", "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd", "typing_Vale.X64.Decls.va_upd_mem", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_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.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok" ], 0, "fe8d20cfb59df0c6e01e71ddcdd67d15" ], [ "Vale.Stdcalls.X64.Fsub.fsub_lemma", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.Curve25519.X64.FastHybrid.va_ens_Fsub_stdcall", "equation_Vale.Curve25519.X64.FastHybrid.va_req_Fsub_stdcall", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Stdcalls.X64.Fsub.b64", "equation_Vale.Stdcalls.X64.Fsub.fsub_post", "equation_Vale.Stdcalls.X64.Fsub.fsub_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "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.Memory.buffer64", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.UInt64.t", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "interpretation_Tm_abs_138091b81012b0bbcb716913bf498356", "interpretation_Tm_abs_a810575fd82014589fda340470b8b592", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok" ], 0, "30ebe4fcc15524b95d6e16b08344990d" ], [ "Vale.Stdcalls.X64.Fsub.lowstar_Fsub_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "9cf82a471cca0940c3e0a204a6149ef6" ], [ "Vale.Stdcalls.X64.Fsub.lowstar_Fsub", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "00666f31893ec42789d3d6235884ea9e" ] ] ]