[ "|o[=%ˆt", [ [ "Vale.Interop.X64.calling_conventions", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "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", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "int_inversion", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.X64.Machine_s.__proj__Reg__item__rf" ], 0, "da4feef241cb661f79c81bbc18a8e13b" ], [ "Vale.Interop.X64.arg_reg_relation'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "58577137fad52b87f6e254913f1cda67" ], [ "Vale.Interop.X64.__proj__Rel__item__of_arg", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "baebb6b4c389a2b27efa0a66b5af8110" ], [ "Vale.Interop.X64.__proj__Rel__item__of_arg", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "proj_equation_Vale.Interop.X64.Rel_of_reg", "projection_inverse_Vale.Interop.X64.Rel_of_reg", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg" ], 0, "9763317f02ef740cdd64be4ad7e3d943" ], [ "Vale.Interop.X64.arg_reg_relation", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a21f24134033cd71d10802f9b10a57a6" ], [ "Vale.Interop.X64.upd_reg", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "eda57e8a560e21dde8087c28ee3585bf" ], [ "Vale.Interop.X64.arg_as_nat64", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "constructor_distinct_Vale.Interop.Base.TD_Base", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "disc_equation_Vale.Arch.HeapTypes_s.TUInt16", "disc_equation_Vale.Arch.HeapTypes_s.TUInt32", "disc_equation_Vale.Arch.HeapTypes_s.TUInt64", "disc_equation_Vale.Arch.HeapTypes_s.TUInt8", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "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.Base.buf_t", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Base.valid_base_type", "equation_Vale.Interop.Types.b8_preorder", "equation_Vale.Interop.Types.base_typ_as_type", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Base.td", "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", "proj_equation_Vale.Interop.Base.TD_Base__0", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Interop.Base.TD_Base__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__2", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ddc9affe1c24b533b166e85103903e5", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_cc44fd36d5a2aa45d2e509a17f81b635", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Vale.Interop.Base.__proj__TD_Base__item___0" ], 0, "bfe11c926ee6669772a05a89378c1451" ], [ "Vale.Interop.X64.register_of_args", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "84723e25ea49a11532ff9c636bdbe567" ], [ "Vale.Interop.X64.register_of_args", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_8586951a648edf3e1a4ab7205cd76f9a", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_d44bc976b7abffa2383f9beda9ed2be2_3", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_as_nat64", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.Interop.X64.upd_reg", "equation_Vale.Interop.X64.update_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg", "int_inversion", "int_typing", "interpretation_Tm_abs_40c176358d0f08dc3044d9601a70555e", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_14339eb8533e3614a873a95b131397c3", "refinement_interpretation_Tm_refine_15685006ec438bc2f8ca7bff4430c057", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_30717a2fe2b5f84dbb8dbb8d5f517985", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.Interop.X64.update_regs", "well-founded-ordering-on-nat" ], 0, "8fe8b56523b761df4cc3485ab3c4f34b" ], [ "Vale.Interop.X64.stack_of_args", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "de8c7531861df4388335cb43e63eade8" ], [ "Vale.Interop.X64.stack_of_args", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "binder_x_f1a25a7a9568029cc84ed0689b5f2730_3", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_2023a85859015575478d3c82f97e9605", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "well-founded-ordering-on-nat" ], 0, "5bb0695d2b92fd2c96344981e5ce8b47" ], [ "Vale.Interop.X64.upd_taint_map_arg", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.Interop.Base.arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "kinding_Vale.Interop.Base.td@tok", "proj_equation_Prims.Mkdtuple2__1", "projection_inverse_BoxBool_proj_0", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "489b3936b7f8cda8618dbb8beca1c9a0" ], [ "Vale.Interop.X64.taint_arg_b8", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Types.b8_preorder", "equation_Vale.Interop.X64.taint_of_arg", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__2", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok" ], 0, "40080983d63731bce86f843f99a44bea" ], [ "Vale.Interop.X64.taint_arg_args_b8_mem", 1, 1, 0, [ "@query" ], 0, "4c6de2cdcceff2fe71ab5b364d1bf767" ], [ "Vale.Interop.X64.taint_arg_args_b8_mem", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e", "binder_x_49b65ff426cd1f25d61dfaad9d6052cd_0", "binder_x_c8ae51e7e32588c3fc442c63c1bb566c_1", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_Prims.Mkdtuple2", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.taint_arg_b8", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Base.arg", "interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "kinding_Prims.list@tok", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10", "subterm_ordering_Prims.Cons", "typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "typing_Vale.Interop.Base.args_b8", "typing_Vale.Interop.X64.taint_arg_b8" ], 0, "077dffd2fd6c13a41d52fc11945aa81d" ], [ "Vale.Interop.X64.mk_taint_equiv", 1, 1, 0, [ "@query" ], 0, "262e746eacb6c6cf55b9624b5aed39d4" ], [ "Vale.Interop.X64.mk_taint_equiv", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.BigOps.pairwise_op_.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_FStar.BigOps.pairwise_op_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "FStar.BigOps_interpretation_Tm_ghost_arrow_4893cf450fdcb12f9a707dc878f6dac3", "FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd", "Prims_interpretation_Tm_arrow_289ee2cc5874944bf725b9e3db8c0fd6", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Def.Words.Four_s_interpretation_Tm_arrow_ca13e3f48edab78b734271373e04eb58", "Vale.Interop.Base_interpretation_Tm_arrow_3b54e6762f20b0c8a1ed0db43e4767dd", "Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab", "Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1", "Vale.Interop.X64_interpretation_Tm_arrow_56ff75899c018f73041073e81157888d", "Vale.Interop.X64_interpretation_Tm_arrow_b9c27cd0ffecc7b6756f5a4119295d50", "binder_x_1cd5ca4beffacc47a478b6133a0431ac_0", "binder_x_c8ae51e7e32588c3fc442c63c1bb566c_1", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Interop.Base.TD_Base", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_elim_Prims.Mkdtuple2", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "eq2-interp", "equation_FStar.BigOps.map_op_", "equation_FStar.BigOps.pairwise_and_", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_LowStar.ImmutableBuffer.immutable_preorder", "equation_Prims.eq2", "equation_Prims.l_True", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.disjoint_not_eq", "equation_Vale.Interop.Base.disjoint_or_eq", "equation_Vale.Interop.Base.disjoint_or_eq_1", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.imm_to_b8", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.X64.arg_list_sb", "equation_Vale.Interop.X64.mk_taint", "equation_Vale.Interop.X64.taint_arg_b8", "equation_Vale.Interop.X64.taint_map", "equation_Vale.Interop.X64.taint_of_arg", "equation_Vale.Interop.X64.upd_taint_map_arg", "equation_Vale.Interop.X64.upd_taint_map_b8", "equation_with_fuel_FStar.BigOps.pairwise_op_.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.l_True", "function_token_typing_Prims.l_and", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.Base.disjoint_or_eq_1", "function_token_typing_Vale.Interop.X64.mk_taint", "function_token_typing_Vale.Interop.X64.upd_taint_map_arg", "int_inversion", "interpretation_Tm_abs_89e176a9e84a687a65f35a76255cd46e", "kinding_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab", "kinding_Vale.Interop.Types.b8@tok", "l_and-interp", "l_or-interp", "primitive_Prims.op_Addition", "proj_equation_FStar.Pervasives.Native.Some_v", "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.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.Interop.Base.TD_Base__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__2", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2", "projection_inverse_Vale.Interop.Types.Buffer_bsrc", "projection_inverse_Vale.Interop.Types.Buffer_src", "projection_inverse_Vale.Interop.Types.Buffer_writeable", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_85be0c420eb68f4e7a21abb89e018245", "refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10", "refinement_interpretation_Tm_refine_b1ecbb54de43c72e39a025eeadb88801", "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "subterm_ordering_Prims.Cons", "token_correspondence_Prims.l_and", "token_correspondence_Vale.Interop.X64.mk_taint", "token_correspondence_Vale.Interop.X64.upd_taint_map_arg", "typing_FStar.List.Tot.Base.length", "typing_FStar.StrongExcludedMiddle.strong_excluded_middle", "typing_Prims.eq2", "typing_Vale.Interop.Base.imm_to_b8", "typing_Vale.Interop.X64.init_taint", "typing_Vale.Interop.X64.taint_arg_b8", "unit_inversion", "unit_typing" ], 0, "2327fa3eb0aa6b6f5a44ded4c2c0253b" ], [ "Vale.Interop.X64.create_initial_trusted_state", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "bool_inversion", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Interop.Assumptions.init_regs", "function_token_typing_Vale.Interop.X64.register_of_args", "int_inversion", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomConstMap", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty", "primitive_Prims.op_Negation", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_19df052c5be3a78e6dc7481200c8be37", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_610f1abe8da643877455975003828a15", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_FStar.Map.const", "typing_FStar.Map.domain", "typing_FStar.Set.complement", "typing_FStar.Set.empty", "typing_FStar.Set.mem", "typing_Vale.X64.Machine_s.__proj__Reg__item__rf", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok" ], 0, "317447d103599eae12cbc25c32fbcd74" ], [ "Vale.Interop.X64.return_val_t", 1, 1, 0, [ "@query" ], 0, "dc737090876dea0d43263ad1f1b3d36a" ], [ "Vale.Interop.X64.return_val", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "b71bf1cc0b2e4a924187df5278e54ffd" ], [ "Vale.Interop.X64.prediction_post", 1, 1, 0, [ "@query" ], 0, "b8aa3863aaf03b068adfc9d46cac41c2" ], [ "Vale.Interop.X64.as_lowstar_sig_post", 1, 1, 0, [ "@query", "equation_Vale.Interop.X64.prediction_pre" ], 0, "4a7e3ee8384bfc35ddb5f3dece9bd42e" ], [ "Vale.Interop.X64.as_lowstar_sig", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_31fb0c066152aad9773967074755b671" ], 0, "45f53067187f88abd696fcebbdb72e6a" ], [ "Vale.Interop.X64.wrap_variadic", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_0d4779e4452bcc98cf90aa3d3290d68f", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_44657b0dc6094dfa0cb4d159b23c54a2", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "constructor_distinct_Tm_unit", "data_typing_intro_Vale.Interop.X64.As_lowstar_sig_ret@tok", "disc_equation_FStar.Pervasives.Native.Some", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.X64.as_lowstar_sig_post", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.prediction", "equation_Vale.Interop.X64.prediction_post", "equation_Vale.Interop.X64.prediction_pre", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "int_inversion", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "kinding_Vale.Interop.Heap_s.interop_heap@tok", "kinding_Vale.Interop.X64.as_lowstar_sig_ret@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Ghost.reveal_hide", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_args", "proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_final_mem", "proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_fuel", "proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_n", "projection_inverse_BoxBool_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_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_args", "projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_final_mem", "projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_fuel", "projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_n", "refinement_interpretation_Tm_refine_31fb0c066152aad9773967074755b671", "refinement_interpretation_Tm_refine_427964005be28d37845727035e1dec26", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_a3541cbaa1e5d11c6f771b017004cb9c", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_efd0f8a81ce2caa3973fda37b5c108c1", "refinement_interpretation_Tm_refine_f416aaa513efc2872a5219f88f959c6a", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "typing_FStar.Pervasives.Native.fst", "typing_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc" ], 0, "ad3bef8a26fbc9c3599cf2d53ef23244" ], [ "Vale.Interop.X64.rel_gen_t", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "binder_x_419a1f9cfe95c45ddf8352069090c461_3", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_2", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7f4d02dbd27ce887ddfabaa0a6cb4e3f", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.List.Tot.Base.length", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "ebb39780968eaac3a9030defaf8fe8d2" ], [ "Vale.Interop.X64.elim_rel_gen_t_cons", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "equation_Prims.nat", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_ee32529582ab288f5f4d513adc54182a", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "dac9f086aab2b63845d11bd84a3f6d3c" ], [ "Vale.Interop.X64.prediction_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a677c11b47fe58c8994e22a304c138ba" ], [ "Vale.Interop.X64.prediction_t", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_07bf7a800fe5b6f7326c4a1398117bb8_8", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_7cb5666207c5130a392b3a823a693392_6", "binder_x_97ef5ff619e486c846fe112d821f649f_4", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_c9a5b2c01f528cab5ea8751bf4318890_7", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ff49fd1edd7220d4f3ccd4421aaa025", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.Interop.X64.prediction_post_rel_t", "token_correspondence_Vale.Interop.X64.prediction_pre_rel_t", "typing_FStar.List.Tot.Base.length", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "951fed40cc4c80fc5f6d72b1df2b4871" ], [ "Vale.Interop.X64.elim_predict_t_nil", 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", "equation_Vale.Interop.X64.arg_list", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0" ], 0, "3f6b17fe14343cd36dcec7399b186fcc" ], [ "Vale.Interop.X64.elim_predict_t_cons", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.Base_pretyping_2f6f4dabbf5d6144c841ea9fcae77848", "constructor_distinct_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_41c6a2194855737ab1ee36516ff41a5e" ], 0, "3f0e4aae00e23b5da1d1c3b620fdf31d" ], [ "Vale.Interop.X64.elim_predict_t_cons", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "equation_Prims.nat", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_41c6a2194855737ab1ee36516ff41a5e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "typing_FStar.List.Tot.Base.length", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "f1d97a695920008621bff96261c808d1" ], [ "Vale.Interop.X64.as_lowstar_sig_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "dc2a4bd9be03a5e6eda045ecacf21313" ], [ "Vale.Interop.X64.as_lowstar_sig_t", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_5af8168932a4bf3947dc018963e66e23_8", "binder_x_66831f94ffcc1a2a32f7393d1a9f2388_6", "binder_x_97ef5ff619e486c846fe112d821f649f_4", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_b9f940dce8bb49bea5d289cc241fd504_7", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_a31f7a9e4f73955bed5763b111fc28da", "refinement_interpretation_Tm_refine_b024999814ba64acd5a9575e2d26ee00", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.Interop.X64.prediction_post_rel_t", "token_correspondence_Vale.Interop.X64.prediction_pre_rel_t", "typing_FStar.List.Tot.Base.length", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "01e9a66ecdb3de1abec6adeb87a946a7" ], [ "Vale.Interop.X64.wrap_aux", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71", "typing_FStar.List.Tot.Base.length" ], 0, "1528827b8db9788fc59fbeae58df9458" ], [ "Vale.Interop.X64.wrap_aux", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_094cffd6b008f86820e77aea17a251f5", "Vale.Interop.X64_interpretation_Tm_arrow_5993bb75c594ddb42550fe0d7bf0eb16", "Vale.Interop.X64_interpretation_Tm_arrow_9cbac494a47f7def70a027d5494bb917", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6", "binder_x_97ef5ff619e486c846fe112d821f649f_4", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.elim_rel_gen_t_nil", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.elim_rel_gen_t_nil", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_3c3b8feb4e2389d801357b22c35f1c8d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aab1f6c3af5a5d18fbf1f6c548d272de", "refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e", "refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.X64.elim_rel_gen_t_nil", "token_correspondence_Vale.Interop.X64.prediction_post_rel_t", "token_correspondence_Vale.Interop.X64.prediction_pre_rel_t", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_3f50ee6e2ed0fdae3704b80b11005055", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "3589a21c401c325adfcb191f93072b18" ], [ "Vale.Interop.X64.wrap'", 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "c36b5883bb900fbc3a113c7413dfd9c4" ], [ "Vale.Interop.X64.wrap'", 2, 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "19844557018c668ff67939f334507a3c" ], [ "Vale.Interop.X64.wrap'", 3, 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "381517e2a845b0c4edc420d4f13e3ad4" ], [ "Vale.Interop.X64.as_lowstar_sig_t_weak'", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71", "typing_FStar.List.Tot.Base.length" ], 0, "1d73abb0928c5c57057a44b3e1eec4e3" ], [ "Vale.Interop.X64.as_lowstar_sig_t_weak'", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6", "binder_x_97ef5ff619e486c846fe112d821f649f_4", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e", "refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.X64.prediction_post_rel_t", "token_correspondence_Vale.Interop.X64.prediction_pre_rel_t", "typing_FStar.List.Tot.Base.length", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "37b5d52c952626fbd3713bf47df03258" ], [ "Vale.Interop.X64.wrap_aux_weak", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71", "typing_FStar.List.Tot.Base.length" ], 0, "23dd6779a31028fc126650f75378eb5a" ], [ "Vale.Interop.X64.wrap_aux_weak", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_33afdcf6a0b392aeb39811347623ec9c", "Vale.Interop.X64_interpretation_Tm_arrow_5993bb75c594ddb42550fe0d7bf0eb16", "Vale.Interop.X64_interpretation_Tm_arrow_7ce33a73121f98da3b5328c0b8dab0d3", "Vale.Interop.X64_interpretation_Tm_arrow_980b79c62767264e2d550623d192cfbc", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_b9642c00164ecb8b7f18f2a75fdd241c", "binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6", "binder_x_97ef5ff619e486c846fe112d821f649f_4", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_FStar.Pervasives.Native.Some", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.X64.als_ret", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.as_lowstar_sig_post", "equation_Vale.Interop.X64.as_lowstar_sig_post_weak", "equation_Vale.Interop.X64.elim_predict_t_nil", "equation_Vale.Interop.X64.elim_rel_gen_t_nil", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.Interop.X64.prediction_post", "equation_Vale.Interop.X64.state_builder_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.create_initial_trusted_state", "function_token_typing_Vale.Interop.X64.elim_rel_gen_t_nil", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "kinding_Vale.Interop.Heap_s.interop_heap@tok", "kinding_Vale.Interop.X64.as_lowstar_sig_ret@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "primitive_Prims.op_Addition", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_3c3b8feb4e2389d801357b22c35f1c8d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aab1f6c3af5a5d18fbf1f6c548d272de", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e", "refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.Interop.X64.elim_rel_gen_t_nil", "token_correspondence_Vale.Interop.X64.prediction_post_rel_t", "token_correspondence_Vale.Interop.X64.prediction_pre_rel_t", "typing_FStar.Ghost.erased", "typing_FStar.Ghost.reveal", "typing_FStar.List.Tot.Base.length", "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1", "typing_FStar.Pervasives.Native.snd", "typing_FStar.UInt64.t", "typing_Tm_abs_94ccf6309093b3b002127c057db2dfa7", "typing_Vale.Interop.X64.__proj__As_lowstar_sig_ret__item__final_mem", "typing_Vale.Interop.X64.__proj__As_lowstar_sig_ret__item__fuel", "typing_Vale.Interop.X64.op_Plus_Plus", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code" ], 0, "65c3eb52abbbf9847cb025d9c8ccf4da" ], [ "Vale.Interop.X64.wrap_weak'", 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "16aee4b3dc60d821cb2528634f045bbf" ], [ "Vale.Interop.X64.wrap_weak'", 2, 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "8d6b7339cc16eff8aac8c34a73948722" ], [ "Vale.Interop.X64.wrap_weak'", 3, 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", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b" ], 0, "946de3b46c3061d19a6bf68d9f8d3d20" ], [ "Vale.Interop.X64.as_lowstar_sig_t_weak", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "equation_Prims.nat", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9c77630db93706b12998369544649e46", "refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452", "typing_FStar.List.Tot.Base.length" ], 0, "89295b4c0c5f7c0c98f6f6b8b6f79a99" ], [ "Vale.Interop.X64.as_lowstar_sig_t_weak", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452" ], 0, "25452b65fd2399267f4eefed9fe4e46f" ], [ "Vale.Interop.X64.wrap_weak", 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", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arity_ok", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103", "refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452" ], 0, "9af6d944d31e43aee311997ee126ba35" ], [ "Vale.Interop.X64.wrap_weak", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452" ], 0, "b007e6799f158760f909781bb73ddc77" ], [ "Vale.Interop.X64.register_of_arg_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "b9c044fcec1eadd919a4318c37595d67" ], [ "Vale.Interop.X64.arg_of_register", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "7ad8ef70671a701c51328dcabf365999" ], [ "Vale.Interop.X64.arg_reg_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59", "Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb", "Vale.Interop.X64_interpretation_Tm_arrow_7b93b99fb8000cd672145629f584ce31", "bool_inversion", "constructor_distinct_BoxInt", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.X64.arg_of_register", "equation_Vale.Interop.X64.max_stdcall", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.Interop.X64.register_of_arg_i", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat2", "function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg", "function_token_typing_Vale.Interop.X64.arg_of_register", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "lemma_FStar.Pervasives.invertOption", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.Interop.X64.Rel_of_arg", "proj_equation_Vale.Interop.X64.Rel_of_reg", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Vale.Interop.X64.Rel_of_arg", "projection_inverse_Vale.Interop.X64.Rel_of_reg", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_arg", "token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg", "token_correspondence_Vale.Interop.X64.arg_of_register", "token_correspondence_Vale.Interop.X64.register_of_arg_i", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Vale.Interop.X64.arg_of_register", "typing_Vale.Interop.X64.max_stdcall", "typing_Vale.Interop.X64.reg_nat", "typing_Vale.Interop.X64.register_of_arg_i" ], 0, "137839201e4bcf25331973625ef8b995" ], [ "Vale.Interop.X64.regs_modified_stdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "167005bf49d8b27b021fd2aff1258144" ] ] ]