[ ")\u001f)6EeA", [ [ "Vale.Interop.Base.buf_t", 1, 1, 0, [ "@query", "constructor_distinct_BoxInt", "constructor_distinct_Tm_unit", "equation_Vale.Interop.Types.view_n", "projection_inverse_BoxInt_proj_0" ], 0, "a4a9a5375cc10178ecbeb21893756df2" ], [ "Vale.Interop.Base.ibuf_t", 1, 1, 0, [ "@query", "constructor_distinct_BoxInt", "constructor_distinct_Tm_unit", "equation_Vale.Interop.Types.view_n", "projection_inverse_BoxInt_proj_0" ], 0, "b1fe1b8703d9adc7b64d43116e2b4522" ], [ "Vale.Interop.Base.lemma_seq_neq_intro", 1, 1, 0, [ "@query", "lemma_FStar.Seq.Base.lemma_eq_elim" ], 0, "05cceff14c1cbe9dafbb01bb526cce50" ], [ "Vale.Interop.Base.default_v_of_typ", 1, 1, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "disc_equation_Vale.Arch.HeapTypes_s.TUInt128", "disc_equation_Vale.Arch.HeapTypes_s.TUInt16", "disc_equation_Vale.Arch.HeapTypes_s.TUInt32", "disc_equation_Vale.Arch.HeapTypes_s.TUInt64", "disc_equation_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.base_typ_as_type", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.UInt.fits", "typing_Prims.pow2" ], 0, "e6000db67e239582258dabce50bc628e" ], [ "Vale.Interop.Base.coerce", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_754b00004f4a881ff74d076ab276dfe1" ], 0, "0b6bec0e393878d06489e2cca5100680" ], [ "Vale.Interop.Base.buffer_qualifiers", 1, 1, 0, [ "@query", "assumption_Vale.Arch.HeapTypes_s.taint__uu___haseq" ], 0, "b9bccbaed4fbddbd4cc620f46a1dc3c7" ], [ "Vale.Interop.Base.td", 1, 1, 0, [ "@query", "assumption_Vale.Arch.HeapTypes_s.base_typ__uu___haseq", "assumption_Vale.Interop.Base.buffer_qualifiers__uu___haseq", "equation_Vale.Interop.Base.valid_base_type", "haseqTm_refine_7ddc9affe1c24b533b166e85103903e5" ], 0, "502af2376c175c6840c61de70b7bc0ae" ], [ "Vale.Interop.Base.__proj__TD_Base__item___0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_Base", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_cc44fd36d5a2aa45d2e509a17f81b635" ], 0, "0585ec0cd26de14697c7222ac806bd85" ], [ "Vale.Interop.Base.__proj__TD_Buffer__item___0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_Buffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_39040ee1bc7a1fd25198a7c8d017a52d" ], 0, "8fa6361f5f1a643f1eb71174593d1de8" ], [ "Vale.Interop.Base.__proj__TD_Buffer__item___1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_Buffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_39040ee1bc7a1fd25198a7c8d017a52d" ], 0, "cc4f687e3f4f30174dbfa47026d37b82" ], [ "Vale.Interop.Base.__proj__TD_Buffer__item___2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_Buffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_39040ee1bc7a1fd25198a7c8d017a52d" ], 0, "766f9eb28462fc1c4068179565c7ed91" ], [ "Vale.Interop.Base.__proj__TD_ImmBuffer__item___0", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_bce8993854a3cf20cd71d25f44c5c2db" ], 0, "c24735cef47129b00cf9d13a8a60f27c" ], [ "Vale.Interop.Base.__proj__TD_ImmBuffer__item___1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_bce8993854a3cf20cd71d25f44c5c2db" ], 0, "ddfe4ef81b79c99993632ea1311cf123" ], [ "Vale.Interop.Base.__proj__TD_ImmBuffer__item___2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_bce8993854a3cf20cd71d25f44c5c2db" ], 0, "69887eb2f85ea0fbc00fb298ff30f04d" ], [ "Vale.Interop.Base.td_as_type", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "fuel_guarded_inversion_Vale.Interop.Base.td" ], 0, "ffb56ed015400e5c1505627a479829f6" ], [ "Vale.Interop.Base.n_arrow", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons" ], 0, "8b6ece41d6acde0796e3e2279a2ca1f9" ], [ "Vale.Interop.Base.elim_1", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.Interop.Base.n_arrow.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.Base.n_arrow.fuel_instrumented", "@query", "Vale.Interop.Base_interpretation_Tm_arrow_041cbda21204b02a6dc17491dadae014", "Vale.Interop.Base_interpretation_Tm_arrow_e81173c46466d95a4995dcf245651092", "Vale.Interop.Base_pretyping_2f6f4dabbf5d6144c841ea9fcae77848", "data_elim_Prims.Cons", "disc_equation_Prims.Cons", "equation_with_fuel_Vale.Interop.Base.n_arrow.fuel_instrumented", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_ecfd4e8ab2f3ff28d8434bdbec36e171" ], 0, "cb10c093c97ec02ac82630c17ece080b" ], [ "Vale.Interop.Base.elim_nil", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.Interop.Base.n_arrow.fuel_instrumented", "@query", "disc_equation_Prims.Nil", "equation_with_fuel_Vale.Interop.Base.n_arrow.fuel_instrumented", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_71d18a1f3299e9e17837762635cfc22e" ], 0, "f4637959f8bc01b5a5b1424a192b1436" ], [ "Vale.Interop.Base.n_dep_arrow", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.Interop.Base.n_arrow.fuel_instrumented", "@query", "Vale.Interop.Base_pretyping_2f6f4dabbf5d6144c841ea9fcae77848", "binder_x_526e6d294cb2254bfaf1d83666c82832_3", "binder_x_539449a65710b411a0d6ba2b5dcd2e3e_2", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.logical", "equation_Vale.Interop.Base.td_as_type", "equation_with_fuel_Vale.Interop.Base.n_arrow.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Base.td", "function_token_typing_Prims.logical", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "subterm_ordering_Prims.Cons" ], 0, "9e813b8acabba04a0de22d2dfdedefdf" ], [ "Vale.Interop.Base.intro_dep_arrow_1", 1, 1, 1, [ "@query", "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl" ], 0, "73fb4b162297565bda01623ec1fe342c" ], [ "Vale.Interop.Base.intro_dep_arrow_cons", 1, 1, 1, [ "@query", "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl" ], 0, "c51cd916a7c60c0d8f3d456034cdd7e3" ], [ "Vale.Interop.Base.elim_dep_arrow_nil", 1, 1, 1, [ "@query", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Nil", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Nil_a" ], 0, "f9502752374c03d3551a1fbd97da6c76" ], [ "Vale.Interop.Base.elim_dep_arrow_cons", 1, 1, 1, [ "@query", "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl" ], 0, "908252a455e5d438ad78b5941d197c3d" ], [ "Vale.Interop.Base.disjoint_not_eq", 1, 1, 1, [ "@query" ], 0, "01454d44d725a3dd4419695ca5397eed" ], [ "Vale.Interop.Base.live_arg", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.Interop.Base.arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "kinding_Vale.Interop.Base.td@tok", "proj_equation_Prims.Mkdtuple2__1", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "2b0b5b01b617c8ff7a0a83b85e2d7b95" ], [ "Vale.Interop.Base.args_b8", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.Interop.Base.arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "kinding_Vale.Interop.Base.td@tok", "proj_equation_Prims.Mkdtuple2__1", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "2dce23f3d2a8d685d8cc2bbaf8f5e75d" ], [ "Vale.Interop.Base.arg_loc", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.Interop.Base.arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "kinding_Vale.Interop.Base.td@tok", "proj_equation_Prims.Mkdtuple2__1", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "62ef87fa6ca5c9d58856163cf9775d79" ], [ "Vale.Interop.Base.all_live_cons", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "equation_FStar.BigOps.big_and_", "equation_FStar.BigOps.map_op_", "equation_Prims.l_True", "equation_Prims.logical", "equation_Vale.Interop.Base.all_live", "equation_Vale.Interop.Base.arg", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "function_token_typing_Prims.l_True", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "interpretation_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "l_and-interp", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "token_correspondence_Prims.l_and", "token_correspondence_Vale.Interop.Base.live_arg", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f" ], 0, "6be8db85afa3ba9687f7b257438649da" ], [ "Vale.Interop.Base.disjoint_or_eq_def", 1, 1, 1, [ "@query", "equation_Vale.Interop.Base.disjoint_or_eq" ], 0, "6f7aa32405137557e910468b74d391ad" ], [ "Vale.Interop.Base.disjoint_or_eq_cons", 1, 1, 1, [ "@query", "equation_Vale.Interop.Base.disjoint_or_eq", "l_and-interp" ], 0, "4b07188cfcc96b7d98808e04311d4c1a" ], [ "Vale.Interop.Base.args_b8_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2", "disc_equation_Vale.Interop.Base.TD_Base", "disc_equation_Vale.Interop.Base.TD_Buffer", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equation_Vale.Interop.Base.arg", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Vale.Interop.Base.td", "kinding_Vale.Interop.Base.td@tok", "proj_equation_Prims.Mkdtuple2__1", "typing_Prims.__proj__Mkdtuple2__item___1" ], 0, "df1cef53b2f8c05633821a710666bca8" ], [ "Vale.Interop.Base.args_b8_mem", 2, 2, 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.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.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e", "Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1", "binder_x_cc6beaf9e2624d0643670c917b6f53e1_1", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_0", "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_Prims.Mkdtuple2", "data_typing_intro_Prims.Nil@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", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.imm_to_b8", "equation_Vale.Interop.Base.mut_to_b8", "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", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Base.arg", "interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "kinding_Prims.list@tok", "kinding_Vale.Interop.Base.td@tok", "kinding_Vale.Interop.Types.b8@tok", "l_or-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_Base__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__2", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2", "projection_inverse_Vale.Interop.Types.Buffer_bsrc", "projection_inverse_Vale.Interop.Types.Buffer_src", "projection_inverse_Vale.Interop.Types.Buffer_writeable", "subterm_ordering_Prims.Cons", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "typing_Vale.Interop.Base.args_b8", "unit_inversion", "unit_typing" ], 0, "3c4e4c003a61a699497898de53153dbb" ], [ "Vale.Interop.Base.args_b8_disjoint_or_eq", 1, 2, 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.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.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_0", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.Interop.Base.TD_Buffer", "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", "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_LowStar.Buffer.trivial_preorder", "equation_LowStar.ImmutableBuffer.immutable_preorder", "equation_Prims.eqtype", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.disjoint_not_eq", "equation_Vale.Interop.Base.disjoint_or_eq_1", "equation_Vale.Interop.Base.imm_to_b8", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Heap_s.disjoint_or_eq_b8", "equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "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.buffer_qualifiers", "fuel_guarded_inversion_Vale.Interop.Base.td", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq", "interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "kinding_Prims.list@tok", "kinding_Vale.Interop.Base.td@tok", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_subset", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "proj_equation_Prims.Mkdtuple2__1", "proj_equation_Vale.Interop.Types.Buffer_bsrc", "proj_equation_Vale.Interop.Types.Buffer_src", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxBool_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.Types.Buffer_bsrc", "projection_inverse_Vale.Interop.Types.Buffer_src", "projection_inverse_Vale.Interop.Types.Buffer_writeable", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "typing_Vale.Interop.Base.args_b8", "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.Interop.Types.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type" ], 0, "d5b9cdb950ec69c882c399a7c3eb57e7" ], [ "Vale.Interop.Base.args_b8_live", 1, 2, 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.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Interop.Base_interpretation_Tm_arrow_26d16a307c5a50d5d4a3c34f40f76fb9", "Vale.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e", "binder_x_57fc4916ac214618268ab42a3ce6ec6e_1", "binder_x_ed25b04ac1a3660bf4cdc8ae577888d8_0", "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_typing_intro_Prims.Nil@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", "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.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.args_b8", "equation_Vale.Interop.Base.imm_to_b8", "equation_Vale.Interop.Base.live_arg", "equation_Vale.Interop.Base.mut_to_b8", "equation_Vale.Interop.Types.b8_preorder", "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", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Vale.Interop.Base.arg", "interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "kinding_Prims.list@tok", "kinding_Vale.Interop.Base.td@tok", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "proj_equation_Prims.Mkdtuple2__1", "proj_equation_Vale.Interop.Types.Buffer_bsrc", "proj_equation_Vale.Interop.Types.Buffer_src", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.Interop.Base.TD_Base__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__0", "projection_inverse_Vale.Interop.Base.TD_Buffer__1", "projection_inverse_Vale.Interop.Base.TD_Buffer__2", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1", "projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2", "projection_inverse_Vale.Interop.Types.Buffer_bsrc", "projection_inverse_Vale.Interop.Types.Buffer_src", "projection_inverse_Vale.Interop.Types.Buffer_writeable", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_e52791d2278b15d2e9b3eebe40077dd6", "subterm_ordering_Prims.Cons", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Tm_abs_3db3675d2ffe63564180525cd66ca234", "typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d", "typing_Vale.Interop.Base.args_b8", "unit_inversion", "unit_typing" ], 0, "44e2cdfec8eb5e9f80e0a781b6144a1a" ], [ "Vale.Interop.Base.liveness_disjointness", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Interop.Base.mem_roots", "equation_Vale.Interop.Base.mem_roots_p", "refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818" ], 0, "9a9a2cbb9a03c3c7c1bf6752be9ac27e" ], [ "Vale.Interop.Base.mk_mem", 1, 2, 1, [ "@query" ], 0, "500005c827ba83f73f52e1627bd036c6" ], [ "Vale.Interop.Base.mk_mem_injective", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "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", "fuel_guarded_inversion_Prims.list", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs" ], 0, "1bbde628fe4f28b8cd42c44d9fc5222e" ], [ "Vale.Interop.Base.mem_roots_p_modifies_none", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.BigOps.pairwise_op_.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.BigOps.pairwise_op_.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@query", "FStar.BigOps_interpretation_Tm_arrow_ca13e3f48edab78b734271373e04eb58", "FStar.BigOps_interpretation_Tm_ghost_arrow_4893cf450fdcb12f9a707dc878f6dac3", "Prims_interpretation_Tm_arrow_289ee2cc5874944bf725b9e3db8c0fd6", "Vale.Interop.Base_interpretation_Tm_arrow_3b54e6762f20b0c8a1ed0db43e4767dd", "binder_x_ed25b04ac1a3660bf4cdc8ae577888d8_1", "binder_x_ed25b04ac1a3660bf4cdc8ae577888d8_2", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_0", "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_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", "equation_FStar.BigOps.big_and_", "equation_FStar.BigOps.map_op_", "equation_FStar.BigOps.pairwise_and_", "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_LowStar.Buffer.buffer", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype", "equation_Prims.l_True", "equation_Prims.logical", "equation_Vale.Interop.Base.all_live", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Base.disjoint_or_eq", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.live_arg", "equation_Vale.Interop.Base.mem_roots_p", "equation_Vale.Interop.Base.td_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.td", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.l_True", "function_token_typing_Prims.l_and", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "function_token_typing_Vale.Interop.Base.disjoint_or_eq_1", "interpretation_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "kinding_Vale.Interop.Base.td@tok", "l_and-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "proj_equation_Prims.Mkdtuple2__1", "projection_inverse_BoxBool_proj_0", "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", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "subterm_ordering_Prims.Cons", "token_correspondence_Prims.l_and", "token_correspondence_Vale.Interop.Base.live_arg", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ImmutableBuffer.immutable_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Prims.__proj__Mkdtuple2__item___1", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "typing_Vale.Interop.Base.all_live", "typing_Vale.Interop.Types.base_typ_as_type", "unit_inversion", "unit_typing" ], 0, "d44dda6c2c7bd2207e693281e038033a" ], [ "Vale.Interop.Base.disjoint_or_eq_fresh", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "@query", "Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf", "binder_x_21431c8a31031c1695466aec99773a78_1", "binder_x_ed25b04ac1a3660bf4cdc8ae577888d8_3", "binder_x_ff84c9bcd22599fb143a28f5c0a5efa9_2", "bool_inversion", "bool_typing", "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", "data_elim_Vale.Interop.Base.TD_Buffer", "data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.Interop.Base.TD_ImmBuffer", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype", "equation_Prims.l_True", "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Base.all_live", "equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.arg_of_sb", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Base.disjoint_not_eq", "equation_Vale.Interop.Base.disjoint_or_eq_1", "equation_Vale.Interop.Base.ibuf_t", "equation_Vale.Interop.Base.live_arg", "equation_Vale.Interop.Base.stack_bq", "equation_Vale.Interop.Base.td_as_type", "equation_Vale.Interop.Types.base_typ_as_type", "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.td", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "function_token_typing_Prims.l_True", "function_token_typing_Prims.logical", "function_token_typing_Vale.Interop.Base.arg", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "interpretation_Tm_abs_3db3675d2ffe63564180525cd66ca234", "interpretation_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "l_and-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.live_not_unused_in_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "proj_equation_Prims.Mkdtuple2__1", "projection_inverse_BoxBool_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.Mkbuffer_qualifiers_strict_disjointness", "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_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "token_correspondence_Prims.l_and", "token_correspondence_Vale.Interop.Base.disjoint_or_eq_1", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ImmutableBuffer.immutable_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Tm_abs_84d777d109851c58da209e2a4a34fb6f", "typing_Vale.Interop.Base.all_live", "typing_Vale.Interop.Types.base_typ_as_type", "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion", "unit_typing" ], 0, "134fc55affa8af76faed9736f544d271" ], [ "Vale.Interop.Base.write_taint", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_e4836109f73687024ac3edd113084865", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab", "binder_x_a2b389b19c9bd00c88f8324fd9c67eb4_3", "binder_x_b911783ccd7af794e1a094d844818013_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_d3cd8a6631433ad48d6b3e9c57c54ea1_4", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.HeapTypes_s.memTaint_t", "equation_Vale.Interop.Types.base_typ_as_type", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036", "refinement_interpretation_Tm_refine_dd20688ba5635abfb47e96fd328dd7c1", "typing_FStar.Map.domain", "typing_FStar.Set.complement", "typing_FStar.Set.empty", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.Interop.Types.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.get_downview", "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat" ], 0, "e9be10ee08f0f08ddb861f98b5102b50" ], [ "Vale.Interop.Base.create_memtaint", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "bool_inversion", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Types.base_typ_as_type", "function_token_typing_Prims.int", "int_typing", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomConstMap", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty", "primitive_Prims.op_Negation", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.const", "typing_FStar.Map.domain", "typing_FStar.Set.complement", "typing_FStar.Set.empty", "typing_FStar.Set.mem", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.Interop.Types.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.get_downview", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok" ], 0, "7906e6bda4923bd4b0ddfd33520c72c9" ] ] ]