[ "¡³}䛄KQË\u001c•Zf¤\u0019î", [ [ "Vale.Stdcalls.X64.Fswap.as_t", 1, 1, 0, [ "@query" ], 0, "13afd6efcb4b2265d422b0481bc64579" ], [ "Vale.Stdcalls.X64.Fswap.as_normal_t", 1, 1, 0, [ "@query" ], 0, "34f3574fd7afdc63e76b4ed77b9d8e01" ], [ "Vale.Stdcalls.X64.Fswap.cswap_dom", 1, 1, 0, [ "@query", "equation_Vale.Interop.X64.max_stdcall", "projection_inverse_BoxInt_proj_0" ], 0, "c19cb11733fcc1a4794dae2ea0d511b1" ], [ "Vale.Stdcalls.X64.Fswap.cswap_pre", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt64", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "token_correspondence_Prims.pow2.fuel_instrumented" ], 0, "909fcde1b7bbc366a84007ec2aadc74e" ], [ "Vale.Stdcalls.X64.Fswap.cswap_post", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt64", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "token_correspondence_Prims.pow2.fuel_instrumented" ], 0, "f1abd469e18cb84772ed19008d4b6b76" ], [ "Vale.Stdcalls.X64.Fswap.cswap_lemma'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "b2t_def", "bool_inversion", "bool_typing", "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_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eq2", "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.FastUtil.va_ens_Cswap2_stdcall", "equation_Vale.Curve25519.X64.FastUtil.va_req_Cswap2_stdcall", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.Fswap.b64", "equation_Vale.Stdcalls.X64.Fswap.cswap_post", "equation_Vale.Stdcalls.X64.Fswap.cswap_pre", "equation_Vale.Stdcalls.X64.Fswap.uint64", "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.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_0452a8e5b30970c2e0aa52da40d3c869", "interpretation_Tm_abs_2a6a1253ba5b54c4fb688c6c0be657cf", "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.loc_includes_union_r", "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_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "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_regs", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_ec538f56b4ccf7689822c796e80d576e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "typing_FStar.UInt64.v", "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.FastUtil.va_lemma_Cswap2_stdcall", "typing_Vale.Interop.Assumptions.win", "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.MemoryAdapters.as_vale_buffer", "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_Vale.X64.State.update_reg_64", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok" ], 0, "7af0eb6412fd03386488decca0614a8d" ], [ "Vale.Stdcalls.X64.Fswap.cswap_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.eqtype", "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.FastUtil.va_ens_Cswap2_stdcall", "equation_Vale.Curve25519.X64.FastUtil.va_req_Cswap2_stdcall", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Stdcalls.X64.Fswap.b64", "equation_Vale.Stdcalls.X64.Fswap.cswap_post", "equation_Vale.Stdcalls.X64.Fswap.cswap_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_Vale.AsLowStar.MemoryHelpers.fuel_eq", "interpretation_Tm_abs_0452a8e5b30970c2e0aa52da40d3c869", "interpretation_Tm_abs_2a6a1253ba5b54c4fb688c6c0be657cf", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.loc_includes_union_r", "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_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_FStar.UInt64.t", "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, "b5ab070073da376fa8dccf2062feec67" ], [ "Vale.Stdcalls.X64.Fswap.lowstar_cswap_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "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", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "0a5c6dccb73c7d094303d25e59ac9870" ] ] ]