[ "ñÿä5ñ\u0010\u007fªW¥®[V0Y7", [ [ "Vale.AsLowStar.Wrapper.prediction_pre_rel", 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, "73af35835157dfce113c6881a486d56c" ], [ "Vale.AsLowStar.Wrapper.prediction_post_rel", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_Exists", "equation_Prims.squash", "equation_Prims.subtype_of", "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.mem_eq", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "6eafe1c63af042005f56b127346dedb6" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_disjointness", 1, 1, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.BigOps.pairwise_op_.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@query", "FStar.BigOps_interpretation_Tm_ghost_arrow_4893cf450fdcb12f9a707dc878f6dac3", "Prims_interpretation_Tm_arrow_289ee2cc5874944bf725b9e3db8c0fd6", "Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf", "Vale.AsLowStar.ValeSig_interpretation_Tm_arrow_a60bc968ba6f8a060052ba2ad1d9fbc9", "Vale.Def.Words.Four_s_interpretation_Tm_arrow_ca13e3f48edab78b734271373e04eb58", "Vale.Interop.Base_interpretation_Tm_arrow_3b54e6762f20b0c8a1ed0db43e4767dd", "binder_x_c37ae1fa25eb52771e5e16ed24154679_0", "constructor_distinct_Prims.Nil", "data_elim_Prims.Cons", "data_elim_Prims.Mkdtuple2", "data_elim_Vale.Interop.Base.TD_Buffer", "data_elim_Vale.Interop.Base.TD_ImmBuffer", "data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_FStar.BigOps.big_and_", "equation_FStar.BigOps.map_op_", "equation_FStar.BigOps.pairwise_and_", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_LowStar.ImmutableBuffer.immutable_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.l_True", "equation_Prims.logical", "equation_Vale.AsLowStar.ValeSig.disjoint_or_eq", "equation_Vale.AsLowStar.ValeSig.disjoint_or_eq_1", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.buf_t", "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.td_as_type", "equation_Vale.Interop.Types.base_typ_as_type", "equation_with_fuel_FStar.BigOps.pairwise_op_.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.buffer_qualifiers", "fuel_guarded_inversion_Vale.Interop.Base.td", "function_token_typing_Prims.l_True", "function_token_typing_Prims.l_and", "function_token_typing_Prims.logical", "function_token_typing_Vale.AsLowStar.ValeSig.disjoint_or_eq_1", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.Base.disjoint_or_eq_1", "interpretation_Tm_abs_3db3675d2ffe63564180525cd66ca234", "l_and-interp", "l_or-interp", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_disjoint", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_imm_disjoint", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_immbuffer_imm_disjoint", "lemma_Vale.AsLowStar.MemoryHelpers.loc_disjoint_sym", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_5f251b47f4f1d9b47d2ef5f7264b19cd", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "subterm_ordering_Prims.Cons", "true_interp", "typing_FStar.List.Tot.Base.fold_right_gtot", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ImmutableBuffer.immutable_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "typing_Vale.Interop.Base.disjoint_or_eq", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.MemoryAdapters.as_vale_immbuffer" ], 0, "e4572ff96b2c1d5388fc8c203e026acf" ], [ "Vale.AsLowStar.Wrapper.args_b8_lemma", 1, 1, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.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.memP.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd", "Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf", "Vale.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e", "binder_x_c8ae51e7e32588c3fc442c63c1bb566c_1", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_0", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Prims.Cons", "data_elim_Prims.Mkdtuple2", "data_elim_Vale.Interop.Base.TD_Buffer", "data_elim_Vale.Interop.Base.TD_ImmBuffer", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok", "data_typing_intro_Vale.Interop.Types.Buffer@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_LowStar.Buffer.buffer", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.imm_to_b8", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Types.b8_preorder", "equation_Vale.Interop.Types.base_typ_as_type", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.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", "function_token_typing_Vale.Interop.Base.arg", "interpretation_Tm_abs_3db3675d2ffe63564180525cd66ca234", "interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "kinding_Prims.list@tok", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "projection_inverse_BoxBool_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_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "subterm_ordering_Prims.Cons", "typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "typing_Vale.Interop.Base.args_b8", "typing_Vale.Interop.Base.imm_to_b8" ], 0, "aea21be4f5b349d30d65a59706e456c9" ], [ "Vale.AsLowStar.Wrapper.readable_cons", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.squash", "equation_Vale.AsLowStar.ValeSig.readable", "fuel_guarded_inversion_Vale.Interop.Base.interop_heap", "function_token_typing_Vale.X64.MemoryAdapters.mem_eq", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "d54e03527c48f0e1b7c4bc060836a9bf" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_readable", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_33afdcf6a0b392aeb39811347623ec9c", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_b9642c00164ecb8b7f18f2a75fdd241c", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.Interop.Base.TD_Base", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Mkdtuple2", "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.big_and_", "equation_FStar.BigOps.map_op_", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.l_True", "equation_Prims.logical", "equation_Prims.nat", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.AsLowStar.ValeSig.readable", "equation_Vale.AsLowStar.ValeSig.readable_one", "equation_Vale.AsLowStar.Wrapper.arg_is_registered_root", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.mk_mem", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.state_builder_t", "equation_Vale.X64.Memory.get_vale_heap", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.l_True", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.create_initial_trusted_state", "int_inversion", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "kinding_Vale.Interop.Base.td@tok", "l_and-interp", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_Vale.AsLowStar.MemoryHelpers.lemma_as_mem_as_vale_mem", "proj_equation_Prims.Mkdtuple2__1", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Prims.Nil_a", "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.Heap_s.InteropHeap_ptrs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1799a1d1476f6fd78433d92bcf710b9a", "refinement_interpretation_Tm_refine_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "true_interp", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap" ], 0, "9c2322601649a534e82f5ea09490d0d4" ], [ "Vale.AsLowStar.Wrapper.readable_live_one", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "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", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "eq2-interp", "equation_Prims.eq2", "equation_Prims.squash", "equation_Vale.AsLowStar.ValeSig.readable_one", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.live_arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.interop_heap", "fuel_guarded_inversion_Vale.Interop.Base.td", "function_token_typing_Vale.X64.MemoryAdapters.mem_eq", "kinding_Vale.Interop.Base.td@tok", "l_and-interp", "proj_equation_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "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_2de20c066034c13bf76e9c0b94f4806c", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "4db18b8ea39896ae19359e1595dd248d" ], [ "Vale.AsLowStar.Wrapper.readable_all_live", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@query", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_1", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_FStar.BigOps.big_and_", "equation_FStar.BigOps.map_op_", "equation_Prims.l_True", "equation_Prims.logical", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.AsLowStar.ValeSig.readable", "equation_Vale.Interop.Base.all_live", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.l_True", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Nil_a", "subterm_ordering_Prims.Cons", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f" ], 0, "3a00ac0c5e7eb50c34b832626ac69e5d" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_mem_correspondance", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_33afdcf6a0b392aeb39811347623ec9c", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_b9642c00164ecb8b7f18f2a75fdd241c", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.Interop.Base.TD_Base", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_LowStar.BufferView.Down.View", "data_elim_LowStar.BufferView.Up.View", "data_elim_Prims.Mkdtuple2", "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.Seq.Properties.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_LowStar.ImmutableBuffer.immutable_preorder", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.AsLowStar.LowStarSig.mem_correspondence_1", "equation_Vale.AsLowStar.LowStarSig.mem_imm_correspondence_1", "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ", "equation_Vale.Interop.Base.all_live", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.mem_roots_p", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.Views.down_view128", "equation_Vale.Interop.Views.down_view16", "equation_Vale.Interop.Views.down_view32", "equation_Vale.Interop.Views.down_view64", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Interop.Views.up_view128", "equation_Vale.Interop.Views.up_view16", "equation_Vale.Interop.Views.up_view32", "equation_Vale.Interop.Views.up_view64", "equation_Vale.Interop.Views.up_view8", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.state_builder_t", "equation_Vale.X64.Memory.get_vale_heap", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_LowStar.BufferView.Up.view", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "fuel_token_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented_token", "function_token_typing_FStar.UInt8.t", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.create_initial_trusted_state", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_56016e210d3137fede03530c544bd88f", "interpretation_Tm_abs_7ec7f3492e13b2106aa7b5db29c362c0", "interpretation_Tm_abs_9534a54182a89b506343041a28349d9c", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "kinding_Vale.Interop.Base.td@tok", "l_and-interp", "l_or-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "lemma_Vale.X64.Memory_Sems.lemma_heap_taint", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "proj_equation_LowStar.BufferView.Up.View_n", "proj_equation_Prims.Mkdtuple2__1", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_LowStar.BufferView.Down.View_n", "projection_inverse_LowStar.BufferView.Up.View_get", "projection_inverse_LowStar.BufferView.Up.View_n", "projection_inverse_LowStar.BufferView.Up.View_put", "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.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence", "token_correspondence_Vale.Interop.Base.td_as_type", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "true_interp", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.BufferView.Up.as_seq", "typing_LowStar.ImmutableBuffer.immutable_preorder", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.AsLowStar.LowStarSig.nat_to_uint_seq_t", "typing_Vale.AsLowStar.LowStarSig.view_of_base_typ", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.down_view", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.MemoryAdapters.as_vale_immbuffer", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.MemoryAdapters.create_initial_vale_heap", "unit_inversion", "unit_typing" ], 0, "e996e78993011b3c359d9d0b232fc4fa" ], [ "Vale.AsLowStar.Wrapper.register_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, "cbd259830e1294c324eb3a92f3b6b0df" ], [ "Vale.AsLowStar.Wrapper.register_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", "Prims_pretyping_0da546199211a769a972571cdb3aec67", "binder_x_48a2217f2059f4cffbb91dbc99cfc561_3", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Prims.T@tok", "equation_Prims.l_True", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.Interop.Base.arg", "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", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "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_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_4d2a1ba9661c7cd8587b24f7b38c1ad9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_tok_Prims.T@tok", "well-founded-ordering-on-nat" ], 0, "06b498d30784066d9fe8a0ccd4899f7d" ], [ "Vale.AsLowStar.Wrapper.lemma_register_args'_aux", 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, "cfc4e9db1418bed64fbb5e4b505559e7" ], [ "Vale.AsLowStar.Wrapper.lemma_register_args'_aux", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_7b93b99fb8000cd672145629f584ce31", "Vale.Interop.X64_interpretation_Tm_arrow_8586951a648edf3e1a4ab7205cd76f9a", "binder_x_48a2217f2059f4cffbb91dbc99cfc561_3", "binder_x_8d85ee59233e417cddd559329afb92f7_4", "binder_x_8d85ee59233e417cddd559329afb92f7_5", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.X64.Machine_s.reg_64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Prims.int", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "l_and-interp", "l_quant_interp_a7a8bd3c5137b5cef6ff7880f0a4d281", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "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_01591046ae0ac5682c2bbf24a4d41dda", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_30717a2fe2b5f84dbb8dbb8d5f517985", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_462e4df7e967ee094b8ca981d20e8efd", "refinement_interpretation_Tm_refine_4d2a1ba9661c7cd8587b24f7b38c1ad9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "true_interp", "well-founded-ordering-on-nat" ], 0, "a27d4b6a909983115dde06bec199dede" ], [ "Vale.AsLowStar.Wrapper.lemma_register_args'", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.register_of_args.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.X64.register_of_args.fuel_instrumented", "@query", "Vale.Interop.X64_interpretation_Tm_arrow_10fca7f1452c541e0ca0aee8ba120fe9", "Vale.Interop.X64_interpretation_Tm_arrow_8586951a648edf3e1a4ab7205cd76f9a", "binder_x_49b65ff426cd1f25d61dfaad9d6052cd_2", "binder_x_8d85ee59233e417cddd559329afb92f7_3", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.Interop.X64.Rel", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Def.Words_s.nat64", "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", "equation_with_fuel_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.register_of_args.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", "function_token_typing_Vale.Interop.X64.register_of_args", "int_inversion", "int_typing", "interpretation_Tm_abs_40c176358d0f08dc3044d9601a70555e", "l_and-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.Interop.X64.Rel_of_reg", "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_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_30717a2fe2b5f84dbb8dbb8d5f517985", "refinement_interpretation_Tm_refine_3779f33f649bd76bb5217e2711267ef3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ce8b9161614f1283d6759a022a629b5", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_b331b2c61b99a96a17a60b1ef451a4b8", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg", "true_interp", "typing_FStar.List.Tot.Base.length" ], 0, "4f8616475ac8623a236dd52c47f5770a" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_register_args", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.LowStarSig.register_args.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.LowStarSig.register_args.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_a211ea19c81e32a0acbc5caed299dc1e", "Vale.Interop.Assumptions_interpretation_Tm_arrow_df3353718654c1c5f6338809f358a4f2", "Vale.Interop.X64_interpretation_Tm_arrow_33afdcf6a0b392aeb39811347623ec9c", "Vale.Interop.X64_interpretation_Tm_arrow_7b93b99fb8000cd672145629f584ce31", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_b9642c00164ecb8b7f18f2a75fdd241c", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.Interop.Base.TD_Base", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons", "data_elim_Vale.Interop.X64.Rel", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "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", "equality_tok_Prims.LexTop@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AsLowStar.LowStarSig.arg_as_nat64", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.mk_mem", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Base.valid_base_type", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.Heap_s.mk_addr_map", "equation_Vale.Interop.X64.arg_as_nat64", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.reg_nat", "equation_Vale.Interop.X64.registers", "equation_Vale.Interop.X64.state_builder_t", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.get_vale_heap", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.LowStarSig.register_args.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.register_args_.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "fuel_guarded_inversion_Vale.X64.State.vale_state", "fuel_token_correspondence_Vale.AsLowStar.LowStarSig.register_args.fuel_instrumented_token", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.create_initial_trusted_state", "function_token_typing_Vale.Interop.X64.register_of_args", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "interpretation_Tm_abs_28ed72e13966710f65b95658f8bb53c7", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_61d02bd97a75bcd3f3fdee8bb8289eb2", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "interpretation_Tm_abs_de21ef4046a172ba9b452104b7b78b25", "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.X64.Memory_Sems.lemma_heap_taint", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.X64.Rel_of_arg", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Cons_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.Heap_s.InteropHeap_addrs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "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_0555eb297fb367cf735a2ee7d5dd9d14", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_610f1abe8da643877455975003828a15", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_7ddc9affe1c24b533b166e85103903e5", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.AsLowStar.LowStarSig.register_args", "token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_arg", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp", "typing_FStar.FunctionalExtensionality.on_domain", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "typing_Tm_abs_28ed72e13966710f65b95658f8bb53c7", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.Regs.of_fun", "unit_inversion", "unit_typing" ], 0, "145979481da7b2427d86d4d3e491d705" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_state", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.X64.Flags_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "eq2-interp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.fst", "equation_Prims.eq2", "equation_Prims.squash", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.Interop.Base.create_memtaint", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.arg_list_sb", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.taint_map", "equation_Vale.X64.Decls.vale_state_with_inv", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Machine_s.flag", "equation_Vale.X64.Regs.regs_fun", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Vale.Interop.Assumptions.init_flags", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.X64.Memory_Sems.lemma_heap_taint", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "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_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3a2e4681f7edb97cad4ee17c2c4e0a55", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_4d82b0a921f761d5dd19407476f31082", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_b1ecbb54de43c72e39a025eeadb88801", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.X64.Flags.sel_curry", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_FStar.FunctionalExtensionality.on_domain", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.Heap.heap_create_impl", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.Interop.Base.args_b8", "typing_Vale.Interop.Base.create_memtaint", "typing_Vale.Interop.Base.mk_mem", "typing_Vale.Interop.X64.init_taint", "typing_Vale.Interop.X64.mk_taint", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.Flags.to_fun", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.to_fun", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs" ], 0, "73b488852c8015c327adad5e5e421f82" ], [ "Vale.AsLowStar.Wrapper.stack_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, "b3277c1f31a85f663bc75df13f06afad" ], [ "Vale.AsLowStar.Wrapper.stack_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", "Prims_pretyping_0da546199211a769a972571cdb3aec67", "binder_x_5fe154f56be615abdf86ac31dfd7220b_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Prims.T@tok", "equation_Prims.l_True", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.Interop.Base.arg", "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_2a97db85acbdfb6a27e1c00f4435becf", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_tok_Prims.T@tok", "well-founded-ordering-on-nat" ], 0, "b686a6241e2a9ab5b0c1c32706a4ac44" ], [ "Vale.AsLowStar.Wrapper.frame_update_get_heap", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.MachineHeap_s.get_heap_val64_def", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Arch.MachineHeap_s.update_heap64_def", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Map.upd", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64", "function_token_typing_Vale.Arch.MachineHeap_s.update_heap64", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def", "token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def", "typing_FStar.Map.upd", "typing_Prims.pow2", "typing_Vale.Def.Words.Four_s.nat_to_four", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Def.Words_s.natN" ], 0, "ca65a5c3ba234594f291a0ad70a71ae0" ], [ "Vale.AsLowStar.Wrapper.frame_update_valid_heap", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Arch.MachineHeap_s.update_heap64_def", "equation_Vale.Arch.MachineHeap_s.valid_addr", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Map.upd", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.MachineHeap_s.update_heap64", "function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def", "typing_FStar.Map.domain", "typing_FStar.Map.upd", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Prims.pow2", "typing_Vale.Arch.MachineHeap_s.update_heap64", "typing_Vale.Arch.MachineHeap_s.valid_addr", "typing_Vale.Def.Words.Four_s.nat_to_four", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1" ], 0, "8186fd63656784707903900a84743914" ], [ "Vale.AsLowStar.Wrapper.stack_of_args_stack_args'_aux", 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, "f7c284a2c154dd1379ca64c6e1897f92" ], [ "Vale.AsLowStar.Wrapper.stack_of_args_stack_args'_aux", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@query", "binder_x_4e172140eae8c666cd84959713963229_6", "binder_x_5e21a79f92ae754b956b9a185a77dbdf_5", "binder_x_ae567c2fb75be05905677af440075565_4", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_d44bc976b7abffa2383f9beda9ed2be2_3", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.l_True", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "function_token_typing_Vale.Interop.Base.arg", "int_inversion", "int_typing", "l_and-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_14339eb8533e3614a873a95b131397c3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "true_interp", "typing_Vale.Arch.MachineHeap_s.update_heap64", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "699c142ee0d5ecf9a74aedbcf5510643" ], [ "Vale.AsLowStar.Wrapper.stack_of_args_stack_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, "a47652e2910a25732dd7e5538aa22fa8" ], [ "Vale.AsLowStar.Wrapper.stack_of_args_stack_args'", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.stack_of_args.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.X64.stack_of_args.fuel_instrumented", "@query", "FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_eda366bb3b4e12e04a044320b4b70b4d_3", "binder_x_f1a25a7a9568029cc84ed0689b5f2730_2", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equality_tok_Prims.LexTop@tok", "equation_Prims.l_True", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Arch.MachineHeap_s.update_heap64_def", "equation_Vale.Arch.MachineHeap_s.valid_addr", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.X64.arg_list", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Prims.pow2.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.stack_of_args.fuel_instrumented", "function_token_typing_FStar.Map.upd", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.MachineHeap_s.update_heap64", "function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64", "function_token_typing_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Interop.Base.arg", "int_inversion", "int_typing", "interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc", "l_and-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "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", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_2023a85859015575478d3c82f97e9605", "refinement_interpretation_Tm_refine_3779f33f649bd76bb5217e2711267ef3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def", "true_interp", "typing_FStar.List.Tot.Base.length", "typing_FStar.Map.domain", "typing_FStar.Map.upd", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Vale.Arch.MachineHeap_s.update_heap64", "typing_Vale.Def.Words.Four_s.nat_to_four", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Interop.X64.stack_of_args", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "6b0793c49932b936073fe505162c9a0f" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma_stack_args", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.LowStarSig.stack_args.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.LowStarSig.stack_args.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Interop.X64_interpretation_Tm_arrow_56ff75899c018f73041073e81157888d", "Vale.Interop.X64_interpretation_Tm_ghost_arrow_a7b3c2a41660b40b8fbaa962dc484880", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_True", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.AsLowStar.LowStarSig.arg_as_nat64", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.create_memtaint", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.Base.mk_mem", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.Heap_s.mk_addr_map", "equation_Vale.Interop.X64.arg_as_nat64", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.mk_taint", "equation_Vale.Interop.X64.registers", "equation_Vale.Interop.X64.taint_map", "equation_Vale.X64.Decls.vale_state_with_inv", "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.get_vale_heap", "equation_Vale.X64.Stack_i.valid_stack_slot64", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.LowStarSig.stack_args.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.stack_args_.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "fuel_token_correspondence_Vale.AsLowStar.LowStarSig.stack_args.fuel_instrumented_token", "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.Base.arg", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "function_token_typing_Vale.Interop.X64.register_of_args", "function_token_typing_Vale.Interop.X64.upd_taint_map_arg", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.MemoryAdapters.stack_eq", "int_inversion", "int_typing", "interpretation_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "interpretation_Tm_abs_2ea3cdf2621fcefd70a13c6c6278a44a", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "interpretation_Tm_abs_de21ef4046a172ba9b452104b7b78b25", "kinding_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Map.lemma_SelConst", "lemma_Vale.X64.Stack_Sems.equiv_load_stack64", "lemma_Vale.X64.Stack_Sems.equiv_valid_src_stack64", "primitive_Prims.op_Addition", "proj_equation_Prims.Mkdtuple2__1", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Prims.Nil_a", "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.Heap_s.InteropHeap_addrs", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "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", "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_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_19df052c5be3a78e6dc7481200c8be37", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3779f33f649bd76bb5217e2711267ef3", "refinement_interpretation_Tm_refine_3a2e4681f7edb97cad4ee17c2c4e0a55", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4d82b0a921f761d5dd19407476f31082", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_58dd236680791b7019269235cc52bbff", "refinement_interpretation_Tm_refine_7b48a611171356fe393a59880fa238fc", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_b33984d78ec57a6fe71ec7dee5d92a16", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.AsLowStar.LowStarSig.stack_args", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.Interop.X64.register_of_args", "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp", "typing_FStar.FunctionalExtensionality.on_domain", "typing_FStar.List.Tot.Base.fold_right_gtot", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "typing_Vale.Arch.Heap.heap_create_impl", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.Interop.Assumptions.win", "typing_Vale.Interop.Base.args_b8", "typing_Vale.Interop.Base.create_memtaint", "typing_Vale.Interop.Base.mk_mem", "typing_Vale.Interop.X64.init_taint", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "c8321b0eee62e8595d354ea1c4c598eb" ], [ "Vale.AsLowStar.Wrapper.core_create_lemma", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.heaplet_id", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.AsLowStar.LowStarSig.taint_hyp", "equation_Vale.AsLowStar.LowStarSig.vale_pre_hyp", "equation_Vale.AsLowStar.ValeSig.disjoint_or_eq", "equation_Vale.AsLowStar.ValeSig.readable", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.Base.mem_roots_p", "equation_Vale.Interop.Base.mk_mem", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.vale_state_with_inv", "equation_Vale.X64.Machine_Semantics_s.regs_t", "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.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_a9947d4164c51b7df323ce9524474bf8", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "interpretation_Tm_abs_dc894ff2fb363ce2de95711fc36b475e", "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.Set.lemma_equal_refl", "lemma_Vale.AsLowStar.MemoryHelpers.lemma_as_mem_as_vale_mem", "lemma_Vale.X64.Memory_Sems.lemma_heap_taint", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "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", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_4d82b0a921f761d5dd19407476f31082", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.AsLowStar.LowStarSig.taint_hyp", "token_correspondence_Vale.AsLowStar.LowStarSig.vale_pre_hyp", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_Tm_abs_21aef62468fbbaaabfc4fa849b7f5900", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.Interop.Base.mk_mem", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.Regs.of_fun" ], 0, "ad2dfa47969c28256dee1062fdfb16f5" ], [ "Vale.AsLowStar.Wrapper.eval_code_rel", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AsLowStar.Wrapper.eval_code_ts", "equation_Vale.Interop.Base.coerce", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "f5917a5f189799f5d7be7cba2e9bba86" ], [ "Vale.AsLowStar.Wrapper.mem_correspondence_refl", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "@query", "binder_x_eb96f2119e19317ec6e3b596d5a46609_1", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "constructor_distinct_Vale.Interop.Base.TD_ImmBuffer", "data_elim_Prims.Mkdtuple2", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.AsLowStar.LowStarSig.mem_correspondence_1", "equation_Vale.AsLowStar.LowStarSig.mem_imm_correspondence_1", "equation_Vale.Interop.Base.arg", "equation_with_fuel_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.X64.State.vale_state", "fuel_token_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence.fuel_instrumented_token", "interpretation_Tm_abs_56016e210d3137fede03530c544bd88f", "interpretation_Tm_abs_7ec7f3492e13b2106aa7b5db29c362c0", "interpretation_Tm_abs_9534a54182a89b506343041a28349d9c", "kinding_Vale.Interop.Base.td@tok", "l_and-interp", "proj_equation_Prims.Mkdtuple2__1", "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_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", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.AsLowStar.LowStarSig.mem_correspondence", "true_interp", "typing_Prims.__proj__Mkdtuple2__item___1", "unit_inversion", "unit_typing" ], 0, "a87d3d29cc034b5cb8f804c651debee6" ], [ "Vale.AsLowStar.Wrapper.loc_includes_union", 1, 1, 0, [ "@query", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl" ], 0, "fdd823d5296cd3fe85601ae0333be207" ], [ "Vale.AsLowStar.Wrapper.vale_lemma_as_prediction", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "58a083bed9efe24b05b8461adb5caf15" ], [ "Vale.AsLowStar.Wrapper.vale_lemma_as_prediction", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "043de556fd689f951e4dac33222ae3d9" ], [ "Vale.AsLowStar.Wrapper.vale_lemma_as_prediction", 3, 1, 1, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "FStar.UInt64_pretyping_0a6d0526dc068d94bc7967094b2dd513", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.Reg", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "equation_Vale.AsLowStar.LowStarSig.to_low_post", "equation_Vale.AsLowStar.LowStarSig.to_low_pre", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.AsLowStar.Wrapper.eval_code_ts", "equation_Vale.AsLowStar.Wrapper.prediction_post_rel", "equation_Vale.AsLowStar.Wrapper.prediction_pre_rel", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.elim_nil", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.Base.mem_roots_p", "equation_Vale.Interop.Base.mk_mem", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.calling_conventions", "equation_Vale.Interop.X64.create_initial_trusted_state", "equation_Vale.Interop.X64.prediction_post", "equation_Vale.Interop.X64.prediction_pre", "equation_Vale.Interop.X64.return_val_t", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Decls.vale_state_with_inv", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.regs_t", "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.Memory.get_vale_heap", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_bc295df6c9aefaa61f8d8fe823aba12e", "interpretation_Tm_abs_cb7298f66cf2c1038336f036e81ad33e", "interpretation_Tm_abs_d2f6e6116a3eccf24c4081e9c506e778", "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp", "l_quant_interp_0ff76c03fcc623c734538eefccab1119", "l_quant_interp_6f320a0fb561a6a1f7833ce881ec6649", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.AsLowStar.MemoryHelpers.lemma_as_mem_as_vale_mem", "lemma_Vale.X64.Memory_Sems.lemma_heap_taint", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_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_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace", "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_1823d45635e4544c7ad45a2297f16540", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_4d82b0a921f761d5dd19407476f31082", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5977ee79043fefe2a87cdf265daeff0e", "refinement_interpretation_Tm_refine_7312a52aad41f203e098c3df58c443e9", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "token_correspondence_Vale.AsLowStar.LowStarSig.create_initial_vale_state", "token_correspondence_Vale.Interop.X64.create_initial_trusted_state", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.AsLowStar.ValeSig.fuel_of", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Base.mk_mem", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "typing_Vale.Interop.X64.return_val", "typing_Vale.X64.Machine_s.n_regs", "typing_Vale.X64.MemoryAdapters.create_initial_vale_full_heap", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok" ], 0, "2cc068720cd2d14a430d0ddb4ffae3d6" ], [ "Vale.AsLowStar.Wrapper.pre_rel_generic", 1, 1, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.List.Tot.Base.length" ], 0, "f4d42046efa3daf583e80a07ce30f911" ], [ "Vale.AsLowStar.Wrapper.pre_rel_generic", 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.AsLowStar.Wrapper_interpretation_Tm_arrow_0f1eb0bdc3bd6a30ce5ae4140ecbdc23", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_922591bf7788f693780f5cf469a58fda", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_3", "binder_x_6297ae5f737aaa6bc9dfa87506c2566c_2", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_a6b3b6f0fb0875824086163164df9d9e_4", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "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.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.prediction_pre_rel_t", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_c3cbe7f117264d27f668c6bc66a2ceff", "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_683d68069a932552c920115a8da6ba36", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "c9d105cac9a28a33de7958d88bf1c47f" ], [ "Vale.AsLowStar.Wrapper.post_rel_generic", 1, 1, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a35207d7a1af5a6a7a10e1a20befcfdb", "typing_FStar.List.Tot.Base.length" ], 0, "f98b18fb24e29ebde1d993e0e55205fa" ], [ "Vale.AsLowStar.Wrapper.post_rel_generic", 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.AsLowStar.Wrapper_interpretation_Tm_arrow_56d0533291d70399238e3abbeb4cc0d3", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_58a74084664ca087aa1825590429218e", "Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551", "Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7", "binder_x_4e5fa8d30a41da8adfd375da86aca9b0_3", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_2", "binder_x_6297ae5f737aaa6bc9dfa87506c2566c_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "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.Base.td", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.X64.prediction_post_rel_t", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "int_inversion", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_e8f0078e53c2c55a8ce5ff532aaeb238", "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_37b69f3328e9de32eb8d5b2db37458b3", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "f45ce599b3b3967a0ab3aef80a4d0d3c" ], [ "Vale.AsLowStar.Wrapper.mk_prediction", 1, 1, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "kinding_Vale.Interop.Base.td@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.List.Tot.Base.length" ], 0, "1ab756538e1a646d1aafd6e8972fc195" ], [ "Vale.AsLowStar.Wrapper.mk_prediction", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.post_rel_generic.fuel_instrumented", "@fuel_correspondence_Vale.AsLowStar.Wrapper.pre_rel_generic.fuel_instrumented", "@fuel_correspondence_Vale.Interop.X64.prediction_t.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.post_rel_generic.fuel_instrumented", "@fuel_irrelevance_Vale.AsLowStar.Wrapper.pre_rel_generic.fuel_instrumented", "@query", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_1038cea3781b8e8015e4bc8cc2815e31", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_dd5d23b2a8b38e450000aef5445b54ea", "binder_x_18188c0989a4beba9930605826f0255e_2", "binder_x_49f2b0686d89026c6c650d37442eba41_8", "binder_x_50928706450ce7e88c67bba3d083489c_6", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5", "binder_x_6297ae5f737aaa6bc9dfa87506c2566c_4", "binder_x_79deb58d926b1bf42fda656bdbf70515_7", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_dd9e83b52f92ad97e2c16a5b757872ef_3", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.elim_1", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.X64.arg_list", "equation_Vale.Interop.X64.elim_rel_gen_t_cons", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.post_rel_generic.fuel_instrumented", "equation_with_fuel_Vale.AsLowStar.Wrapper.pre_rel_generic.fuel_instrumented", "equation_with_fuel_Vale.Interop.X64.prediction_t.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "int_inversion", "interpretation_Tm_abs_2ab3e838e3477be23a1ed9f2add9d341", "interpretation_Tm_abs_74815e270789770810c1ee89a0651dfe", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "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_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_518f8d46747c28a6d8e504a1715d599c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68c575862832f04af62b305429dbfc2c", "refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0", "refinement_interpretation_Tm_refine_a35207d7a1af5a6a7a10e1a20befcfdb", "refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.AsLowStar.Wrapper.post_rel_generic.fuel_instrumented", "token_correspondence_Vale.AsLowStar.Wrapper.pre_rel_generic.fuel_instrumented", "token_correspondence_Vale.Interop.Base.elim_1", "token_correspondence_Vale.Interop.X64.elim_rel_gen_t_cons", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_515da3fc9bc63b1bb38188700f0c6326", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "829fe8bcb8242add84ab8470d08f9201" ], [ "Vale.AsLowStar.Wrapper.lowstar_typ", 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", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Interop.Base_interpretation_Tm_arrow_26d16a307c5a50d5d4a3c34f40f76fb9", "binder_x_419a1f9cfe95c45ddf8352069090c461_4", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_2", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Mkdtuple2@tok", "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.Base.td_as_type", "equation_Vale.Interop.X64.arg_list", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.Interop.Base.arg", "int_inversion", "interpretation_Tm_abs_3db3675d2ffe63564180525cd66ca234", "kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "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_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_475572f7185263500f59598a03191ca8", "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_Tm_abs_3db3675d2ffe63564180525cd66ca234" ], 0, "035de66d122bdf99e7952caaee115632" ], [ "Vale.AsLowStar.Wrapper.__test__wrap", 1, 1, 1, [ "@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", "typing_FStar.List.Tot.Base.length" ], 0, "2db808b1d921252f2c1e9c12661df256" ], [ "Vale.AsLowStar.Wrapper.__test__wrap", 2, 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", "FStar.UInt64_pretyping_0a6d0526dc068d94bc7967094b2dd513", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_16a4c33fda3a81d83e93895f1470744f", "Vale.AsLowStar.Wrapper_interpretation_Tm_arrow_18e6df19687ecdd2c29006d7580a9bf4", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_4", "binder_x_7cf7bf6c5d1872b9363024eb4713af40_6", "binder_x_a2968b5aedabccc4f9a87ef4627271f7_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Pervasives.Native.fst", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.AsLowStar.Wrapper.prediction_post_rel", "equation_Vale.AsLowStar.Wrapper.prediction_pre_rel", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.coerce", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.X64.as_lowstar_sig_post", "equation_Vale.Interop.X64.op_Plus_Plus", "equation_Vale.Interop.X64.prediction_post", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_", "function_token_typing_Vale.AsLowStar.Wrapper.prediction_pre_rel", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "int_inversion", "interpretation_Tm_abs_cb7298f66cf2c1038336f036e81ad33e", "interpretation_Tm_abs_d2f6e6116a3eccf24c4081e9c506e778", "kinding_Vale.Interop.Base.td@tok", "l_quant_interp_0ff76c03fcc623c734538eefccab1119", "primitive_Prims.op_Addition", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6e6dd249699f129c8606b8c4af5d7941", "refinement_interpretation_Tm_refine_a5e21a2c79639304d111a1b5a8aa9757", "refinement_interpretation_Tm_refine_cdc7404428a294dac60f04672c7fce7d", "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.length", "typing_Tm_abs_e6dd81f3f1d941d129d7098bb059eee3", "typing_Vale.Interop.X64.op_Plus_Plus" ], 0, "50e5b7f0aa75f51220c3db9095bf1b14" ] ] ]