[
"ä)\u001f¬)6E¥e“„…þ•A",
[
[
"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"
]
]
]