[
"ñÿä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"
]
]
]