Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.X64.Memory.fst.hints
[
"qP!��}��p��-�-@\u0012",
[
[
"Vale.X64.Memory.base_typ_as_vale_type",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"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",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0bb64cc803fc9ddea8a3e9a53da3a47a"
],
[
"Vale.X64.Memory.v_of_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"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",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"ff33bc20e49e80ff102f3b7bbdb77e3c"
],
[
"Vale.X64.Memory.v_to_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"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",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"92b9f83bddbf76564aa1dd97bd3c9bad"
],
[
"Vale.X64.Memory.lemma_v_to_of_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.v_of_typ",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt16.vu_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_FStar.UInt64.vu_inv", "lemma_FStar.UInt8.vu_inv",
"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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"90e136d9d2506c99c9b80030503f4d95"
],
[
"Vale.X64.Memory.uint_view",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"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",
"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",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"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.X64.Memory.uint128_view",
"equation_Vale.X64.Memory.uint16_view",
"equation_Vale.X64.Memory.uint32_view",
"equation_Vale.X64.Memory.uint64_view",
"equation_Vale.X64.Memory.uint8_view",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_n"
],
0,
"e4c2d383312bd715f1b4e43cf892f637"
],
[
"Vale.X64.Memory.buffer",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Interop.Types.view_n",
"fuel_guarded_inversion_Vale.Interop.Types.base_typ",
"projection_inverse_BoxInt_proj_0"
],
0,
"0dadc0049c4b6e902e53c4e59fc8f262"
],
[
"Vale.X64.Memory.buffer_as_seq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.X64.Memory.buffer",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b"
],
0,
"50afb23235510be768fbbe88dfee4e62"
],
[
"Vale.X64.Memory.buffer_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.X64.Memory.buffer",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b"
],
0,
"4c99f2036e2cdf7e792b5e7555264b75"
],
[
"Vale.X64.Memory.modifies",
1,
2,
1,
[ "@query" ],
0,
"77f48abcdb5ba7155ca4fa4606a04052"
],
[
"Vale.X64.Memory.index64_heap_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"Vale.X64.Memory_interpretation_Tm_arrow_f4c4992cf843ea442af1288d1d5d4d22",
"b2t_def", "bool_inversion", "bool_typing",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Def.Types_s.le_bytes_to_nat64",
"equation_Vale.Def.Types_s.le_bytes_to_nat64_def",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get64",
"equation_Vale.Interop.Views.get64_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt64.vu_inv",
"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_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a97bb01c04ffe0871485a0f7264ef673",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt8.v",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get64_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt64.v",
"typing_Prims.pow2",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"typing_Vale.Def.Types_s.le_bytes_to_nat64",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Def.Words.Two_s.two_to_nat",
"typing_Vale.Def.Words_s.natN", "typing_Vale.Interop.Views.get64"
],
0,
"8f951f8e1e6b178bf08577e20250a6db"
],
[
"Vale.X64.Memory.index_helper",
1,
2,
1,
[ "@query" ],
0,
"ce0eba46122bb420604e7680ffdcdcf9"
],
[
"Vale.X64.Memory.index_mul_helper",
1,
2,
1,
[
"@query", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"7f68e19c706f27fc66ad6ca26bee5c02"
],
[
"Vale.X64.Memory.index64_get_heap_val64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Words_s.nat64",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_9539918077828aa633026534394b5105",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"7598a9389dc28e2c3f403234dd6840bb"
],
[
"Vale.X64.Memory.index64_get_heap_val64",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"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_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view64",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint64_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Words_s.nat64",
"function_token_typing_Vale.Interop.Views.get64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_3ed59215883a7995a44c81874590454d",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9539918077828aa633026534394b5105",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c5e41889e8aa79424c019ae4913df676",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_de9eee4fe618f0aed28fb9c6f457edb8",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"05b2e57cc6c59ea3f9dcd39fd1bf28b5"
],
[
"Vale.X64.Memory.index128_get_heap_val128_aux",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Def.Types_s.le_bytes_to_quad32",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Views.get128",
"equation_Vale.Interop.Views.get128_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get128_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"c922c6d126a67813afe214a4a0583131"
],
[
"Vale.X64.Memory.index128_get_heap_val128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"refinement_interpretation_Tm_refine_00753086f0a5091e4281a2f51c385e86",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"4562f0c89a77b328f17925a3a5938ddb"
],
[
"Vale.X64.Memory.index128_get_heap_val128",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"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_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view128",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint128_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_3ed59215883a7995a44c81874590454d",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_00753086f0a5091e4281a2f51c385e86",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_080f24dfea74b17188b02c3d688dc2d1",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_de9eee4fe618f0aed28fb9c6f457edb8",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.get128",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"4f308ff0d527d766e98cc4d85077d20a"
],
[
"Vale.X64.Memory.lemma_modifies_goal_directed",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"eca75e5f71b516c0395da0b30347dade"
],
[
"Vale.X64.Memory.buffer_length_buffer_as_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view"
],
0,
"8fcb58586b9d91e543107912fe5ae439"
],
[
"Vale.X64.Memory.same_underlying_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"bool_inversion", "equality_tok_Prims.LexTop@tok",
"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_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_3ed59215883a7995a44c81874590454d",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_Vale.Lib.BufferViewHelpers.lemma_uv_equal",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_155df05ad67f874c58a5e9d67f28cc44",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64c7cdf80f5eb0b5f10cf9506fa04793",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_8ae5e7ec51c01b06a6c5c069c9bd60bc",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2c7b3113f8978139a51593955da6aab",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_dcbfc73242b72914ef6a7370bbd5f53b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"3985aab9224ceb4c09d7d8c4a249ecda"
],
[
"Vale.X64.Memory.modifies_buffer_elim",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.loc",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.modifies",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq"
],
0,
"2d1a59fa7bbe13aebd73fdca3ee7ea34"
],
[
"Vale.X64.Memory.modifies_buffer_addr",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.modifies",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs"
],
0,
"251711f2b912b1a2ddcba0f38b90cb61"
],
[
"Vale.X64.Memory.modifies_buffer_readable",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.modifies"
],
0,
"a63902b29843317ed1259836fb7185fd"
],
[
"Vale.X64.Memory.loc_disjoint_none_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_none"
],
0,
"28787a2ecc1725ec92208f37b3768df0"
],
[
"Vale.X64.Memory.loc_disjoint_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_union"
],
0,
"1568a240b1d0264a85f90cb3e3150a36"
],
[
"Vale.X64.Memory.loc_includes_refl",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"186856eafe40fd6fcbbf916fec0065d4"
],
[
"Vale.X64.Memory.loc_includes_trans",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"af5516308fd9e371d02c0c9de4d80084"
],
[
"Vale.X64.Memory.loc_includes_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"ef06ef403d091763b70d0ad1b7273544"
],
[
"Vale.X64.Memory.loc_includes_union_l",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"abd4f40e6bea495e618cfd359733e818"
],
[
"Vale.X64.Memory.loc_includes_union_l_buffer",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"b9a70e4d1f9988748cd2eaf6e0707ac9"
],
[
"Vale.X64.Memory.loc_includes_none",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_none"
],
0,
"42207561e8fd10168b93e1b81670a6b6"
],
[
"Vale.X64.Memory.modifies_refl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.Set.lemma_equal_refl",
"proj_equation_Vale.Interop.Base.InteropHeap_hs",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_7ae5a5d89e52da1d5454233e706a9bd8",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Interop.Base.__proj__InteropHeap__item__hs"
],
0,
"1cbdaf3da316cbc9ec8556aea9b1a648"
],
[
"Vale.X64.Memory.modifies_goal_directed_refl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.modifies_goal_directed",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"lemma_Vale.X64.Memory.modifies_refl"
],
0,
"6fdc2bb5aac97a03f95fd390979a0879"
],
[
"Vale.X64.Memory.modifies_loc_includes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap"
],
0,
"1f6800e2e9d2d4e60ebe455a5dd3c119"
],
[
"Vale.X64.Memory.modifies_trans",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.loc_union",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"proj_equation_Vale.Interop.Base.InteropHeap_hs",
"refinement_interpretation_Tm_refine_7ae5a5d89e52da1d5454233e706a9bd8",
"typing_Vale.Interop.Base.__proj__InteropHeap__item__hs"
],
0,
"3c436506aa98b3a6f0e038c84ae2e86f"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.modifies_goal_directed",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_r"
],
0,
"7f069eaca55fcbdf4f524e631dfae9b3"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans2",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"a24a3f37d5a09fa7394d57d14b431b38"
],
[
"Vale.X64.Memory.default_of_typ",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"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", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"inversion-interp", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"18ea3bc1f86771e3361a03cd694538ae"
],
[
"Vale.X64.Memory.buffer_read",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"9283f93f06988350dfede95f203b6d5c"
],
[
"Vale.X64.Memory.buffer_read",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_7c64067490892c791d00e02d4d1ae606"
],
0,
"0e3863d0bc62dd4630b7127023cbb8d5"
],
[
"Vale.X64.Memory.seq_upd",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"refinement_interpretation_Tm_refine_87f65bf36fef1b919603d458579dd2c0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_LowStar.BufferView.Up.as_seq"
],
0,
"e2f7f049115c8271da95471d3443ced8"
],
[
"Vale.X64.Memory.seq_upd",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equality_tok_Prims.LexTop@tok",
"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_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6d5ab57ac719f3d34aaa0ac8c62a3164",
"refinement_interpretation_Tm_refine_87f65bf36fef1b919603d458579dd2c0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.index", "typing_LowStar.BufferView.Up.length",
"well-founded-ordering-on-nat"
],
0,
"adde8333e552d2f2ebbdafb7d575115a"
],
[
"Vale.X64.Memory.buffer_write",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"cf41b239274472f677d842a01d9402db"
],
[
"Vale.X64.Memory.buffer_write",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53",
"Vale.X64.Memory_interpretation_Tm_arrow_81aac8ba692481017bca6e707e93646b",
"b2t_def", "bool_inversion", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Interop.Types.b8",
"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.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_of_typ",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t", "int_inversion",
"interpretation_Tm_abs_3ed59215883a7995a44c81874590454d",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.lemma_v_to_of_typ",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"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.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_BoxInt_proj_0",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_ih",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs",
"refinement_interpretation_Tm_refine_081e033567703f73e0895a06d1bc5c83",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.upd",
"typing_LowStar.BufferView.Up.as_seq",
"typing_Tm_abs_3ed59215883a7995a44c81874590454d",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_Vale.X64.Memory.v_of_typ"
],
0,
"79c92b359f25abbad111ef57110b960b"
],
[
"Vale.X64.Memory.addr_in_ptr",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"a9a9bf96b3e9b4b4aedaa959551b4686"
],
[
"Vale.X64.Memory.get_addr_in_ptr",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_da856fadfd0ceae8299e329c69653ead_4",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Memory.valid_offset",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81af2485641f3fbf34b8c6c3aa5cc18e",
"well-founded-ordering-on-nat"
],
0,
"8c4cec0fa1c810032ac0c765627ac769"
],
[
"Vale.X64.Memory.valid_buffer",
1,
0,
0,
[
"@query", "constructor_distinct_BoxInt",
"constructor_distinct_Tm_unit", "equation_Vale.Interop.Types.view_n",
"projection_inverse_BoxInt_proj_0"
],
0,
"46fd9b715ae1834a67122e6f4aded072"
],
[
"Vale.X64.Memory.valid_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1",
"binder_x_c7f2158a2d8b780acacc5b0c5511ae9c_3", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_Vale.Interop.Types.b8", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_or-interp", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"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_5c7618d4b342242f635d965bf64dfd25",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_b6df1ca25e089cb674c96de6ee21cc57",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_Vale.X64.Memory.valid_buffer",
"typing_Vale.X64.Memory.valid_mem_aux"
],
0,
"4fa1deba095cf0baf462cb6370e0e9f5"
],
[
"Vale.X64.Memory.valid_mem",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"01973fcb2c0f0111d6ffc110bc2ae730"
],
[
"Vale.X64.Memory.find_valid_buffer_aux",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Memory.buffer"
],
0,
"8c0f12cb60cf92ad5e5b4ea76bfb8983"
],
[
"Vale.X64.Memory.find_valid_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1",
"binder_x_c7f2158a2d8b780acacc5b0c5511ae9c_3", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"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_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_5c7618d4b342242f635d965bf64dfd25",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d61f82aa10cb7a21acc22496aabac3e9",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.X64.Memory.buffer"
],
0,
"6c3c06ecce75c62c4057fd2cc380913a"
],
[
"Vale.X64.Memory.find_valid_buffer",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"7802d86f4cb53fb2416b3b5d1acd54bc"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.X64.Memory.buffer",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0e3159b4aafaa59dddeca639dba14e85",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.X64.Memory.buffer"
],
0,
"4bc253aed796d8386f7d11b13c23b376"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_aa267eb9de75fe19df06fbeab5d08b54_4",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"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.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_133f293ff9ad12e0f36c8e40a5566847",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_4078df4fbf10d8eebed2a346e674f8d8",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"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.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer",
"typing_Vale.X64.Memory.find_valid_buffer_aux"
],
0,
"234367144f1c5700a203d05004ae9e43"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
3,
1,
1,
[ "@query" ],
0,
"d8209252708305114e2a269feb358396"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
4,
1,
1,
[ "@query" ],
0,
"bd88d507baebdc2842fb9d7ec98d42af"
],
[
"Vale.X64.Memory.find_valid_buffer_ps",
1,
1,
1,
[ "@query" ],
0,
"ef094acb91da060be406b43a0c7c15b4"
],
[
"Vale.X64.Memory.find_valid_buffer_ps",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.Interop.Types.b8", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.sub_list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_14c074c83df2a183bc549b3a98277390",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Memory.buffer"
],
0,
"707710b773531229603c9263d5849b01"
],
[
"Vale.X64.Memory.find_valid_buffer_valid_offset",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion", "bool_typing",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Arch.HeapImpl.ValeHeap",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"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.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_86118ab3e5deebe70fb8dba18f60f35f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer",
"typing_Vale.X64.Memory.find_valid_buffer",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"5c7177740f5ca694f0c4a94dd9ceadf6"
],
[
"Vale.X64.Memory.writeable_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"b2t_def", "binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1",
"binder_x_c7f2158a2d8b780acacc5b0c5511ae9c_3", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"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.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1127b6ab48c20c2fb9fddaf914f6e04f",
"refinement_interpretation_Tm_refine_5c7618d4b342242f635d965bf64dfd25",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a81b42d9f7f2452a617b25fcb666c841",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"f8090c75715ee2e36ae225ad2a1727db"
],
[
"Vale.X64.Memory.writeable_mem",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"cbac7cf81c063b02f2669ad4ae0e1de3"
],
[
"Vale.X64.Memory.find_writeable_buffer_aux",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Memory.buffer"
],
0,
"d55ca5e7cad521603b35c8cbed2df4b9"
],
[
"Vale.X64.Memory.find_writeable_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1",
"binder_x_c7f2158a2d8b780acacc5b0c5511ae9c_3", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"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_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_3822b85b28cc32a98a6e49b6d2a31bbe",
"refinement_interpretation_Tm_refine_5c7618d4b342242f635d965bf64dfd25",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.X64.Memory.buffer"
],
0,
"990e7f7a4049e82b890d3855dfb59fe8"
],
[
"Vale.X64.Memory.find_writeable_buffer",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"9ec4a60570c54fee20302409d769f62a"
],
[
"Vale.X64.Memory.load_mem",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "lemma_FStar.Pervasives.invertOption",
"primitive_Prims.op_AmpAmp",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_86118ab3e5deebe70fb8dba18f60f35f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.addr_in_ptr", "typing_Vale.X64.Memory.buffer"
],
0,
"d986aee3391c3699af6180b2b5cd8b24"
],
[
"Vale.X64.Memory.load_mem64",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1989aefc4fb1fb3d9297a48192fc2009",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"11b22a8b71d866901648d1e59705f205"
],
[
"Vale.X64.Memory.length_t_eq",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_length",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t", "int_inversion",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_482879c16db7e151e318434e1c9fd9f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.uint_view"
],
0,
"fdef03f0b726b3e71ac7bcc1ea47b2bb"
],
[
"Vale.X64.Memory.get_addr_ptr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1989aefc4fb1fb3d9297a48192fc2009",
"refinement_interpretation_Tm_refine_86118ab3e5deebe70fb8dba18f60f35f",
"refinement_interpretation_Tm_refine_c4ca66be96921abff4fd5d2fc79941c6",
"typing_Vale.X64.Memory.valid_mem"
],
0,
"961c1b4b2d1b5cf7e5d0e5f96fcb3788"
],
[
"Vale.X64.Memory.load_buffer_read",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Tm_unit", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8c1c09786c5b2f5e0966db4e7642d2f9",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c4ca66be96921abff4fd5d2fc79941c6",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr"
],
0,
"584c5aeee1c8466cf30a0856f65ca7b4"
],
[
"Vale.X64.Memory.load_buffer_read",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.get_addr_ptr",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.valid_mem",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "proj_equation_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_86118ab3e5deebe70fb8dba18f60f35f",
"refinement_interpretation_Tm_refine_c4ca66be96921abff4fd5d2fc79941c6",
"typing_Vale.X64.Memory.find_valid_buffer"
],
0,
"af98bfea57b361e27b7689395a7fdfcb"
],
[
"Vale.X64.Memory.store_mem",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.mk_addr_map",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_write",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "lemma_FStar.Pervasives.invertOption",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5b3b808db4db11754713a4bf85b66ef8",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c30e627a3e9565f635803e90c17d233a",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr", "typing_Vale.X64.Memory.buffer"
],
0,
"cd60deea5f27c16c267b81da22e89d83"
],
[
"Vale.X64.Memory.store_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1989aefc4fb1fb3d9297a48192fc2009",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"9b79b320b0ba7c015c164a4c409d03da"
],
[
"Vale.X64.Memory.store_buffer_write",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion", "constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_Vale.X64.Memory.writeable_mem",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_1127b6ab48c20c2fb9fddaf914f6e04f",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5b3b808db4db11754713a4bf85b66ef8",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_84546b2005fd76a260f5489d82a11b6b",
"refinement_interpretation_Tm_refine_aa311741644f2a2768d777f8e523a38c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.writeable_mem",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"49c6a900c8200fbbd0b80b51cc37bb81"
],
[
"Vale.X64.Memory.store_buffer_write",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.writeable_mem",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "proj_equation_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_5b3b808db4db11754713a4bf85b66ef8",
"refinement_interpretation_Tm_refine_aa311741644f2a2768d777f8e523a38c",
"typing_Vale.X64.Memory.find_writeable_buffer"
],
0,
"f3087c73b5ab5b87aed83052997fc424"
],
[
"Vale.X64.Memory.valid_mem128",
1,
0,
0,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"14669a65c0e9ffcd2472de0aafa3ac5d"
],
[
"Vale.X64.Memory.writeable_mem128",
1,
0,
0,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"095771729e0208fa97b4d499c461d1f7"
],
[
"Vale.X64.Memory.load_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"93fcb4e2076ba81cf5093899496355fb"
],
[
"Vale.X64.Memory.store_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"e3dce6338ffe5e31a90aa3c341ca9602"
],
[
"Vale.X64.Memory.lemma_valid_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1989aefc4fb1fb3d9297a48192fc2009",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"fa0406968333d7cddf0762f974e5c740"
],
[
"Vale.X64.Memory.lemma_writeable_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_84546b2005fd76a260f5489d82a11b6b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"bcd9af9cb057f878fd507d03ef1a13d9"
],
[
"Vale.X64.Memory.lemma_store_mem",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing", "l_and-interp",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_1127b6ab48c20c2fb9fddaf914f6e04f",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_280477f8beafac540f58d201ea80f0ab",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5b3b808db4db11754713a4bf85b66ef8",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9db89dad77c79e4470143cd4330b4841",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_d923626f416f10c73177bf3fe8f2c31b",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"typing_FStar.Seq.Base.length",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.find_writeable_buffer",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view"
],
0,
"8870f39d55109b65f30fda251c0abf15"
],
[
"Vale.X64.Memory.lemma_load_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0ea764bd1f5f3325aded493ad828ee7a"
],
[
"Vale.X64.Memory.lemma_load_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"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.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_read",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem64",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_280477f8beafac540f58d201ea80f0ab",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_9db89dad77c79e4470143cd4330b4841",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c9cf69caee17e8d6fd551f69ef906d1c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.disjoint_addr",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"4b914edf4dc4d072cc53266f70d9e02b"
],
[
"Vale.X64.Memory.lemma_store_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"8915b4e22aab1eec13a2beab673890d9"
],
[
"Vale.X64.Memory.lemma_store_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem64",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1989aefc4fb1fb3d9297a48192fc2009",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem64",
"typing_Vale.X64.Memory.valid_mem",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"b7789b3a107c151f1b2d196494be9f82"
],
[
"Vale.X64.Memory.lemma_valid_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"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.nat",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"bf71ed4347fc80663eebf00fcf92f069"
],
[
"Vale.X64.Memory.lemma_writeable_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_1127b6ab48c20c2fb9fddaf914f6e04f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"edc58909a94c4563a6997ccfcdbf1f89"
],
[
"Vale.X64.Memory.lemma_load_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"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.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem128",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_280477f8beafac540f58d201ea80f0ab",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4b302147c2db27dcdf388538490f391f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_9db89dad77c79e4470143cd4330b4841",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"80bda00a39f6aa935c35e933624901f8"
],
[
"Vale.X64.Memory.lemma_store_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"e3bd21fe02fa9dfa083a033482749efc"
],
[
"Vale.X64.Memory.lemma_store_mem128",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem128",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0123b5d61540e7701743bb14e4bea64e",
"refinement_interpretation_Tm_refine_02cf365122212f6201f1d812ba6aca45",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_74029d41dd5a790d6f2b31b78c405e2e",
"refinement_interpretation_Tm_refine_938a25ff915313affa8c512a023f29fc",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem",
"typing_Vale.X64.Memory.store_mem128",
"typing_Vale.X64.Memory.valid_mem128",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"d58d97d768fcc69cc9303e4a5a00e1d0"
],
[
"Vale.X64.Memory.apply_taint_buf",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Memory.valid_taint_buf", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"bb944b5521597d823fd87252775bebab"
],
[
"Vale.X64.Memory.lemma_valid_taint64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_taint_buf64",
"fuel_guarded_inversion_Vale.Interop.Types.b8_", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2bc69a528535ed6093b3e6a59ecec1b",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs"
],
0,
"a209965a79f152c1e665d6eaa134a285"
],
[
"Vale.X64.Memory.lemma_valid_taint128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.valid_taint_buf128", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba"
],
0,
"131ed3fc88128b33e2a340c462abe7f4"
],
[
"Vale.X64.Memory.same_memTaint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Prims.eqtype", "equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Memory.memtaint",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion",
"kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Map.lemma_equal_intro",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"d37be5f89c4b453408423f7bbdf6b37f"
],
[
"Vale.X64.Memory.modifies_valid_taint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.valid_taint_buf",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_7c64067490892c791d00e02d4d1ae606",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955"
],
0,
"4a982e51f63b36889670d44391699da8"
],
[
"Vale.X64.Memory.modifies_valid_taint64",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.valid_taint_buf64" ],
0,
"8f51c76182ce1207c416fd26c7f69540"
],
[
"Vale.X64.Memory.modifies_valid_taint128",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.valid_taint_buf128" ],
0,
"4d41384d21c1b6e4329a642d4099a20c"
],
[
"Vale.X64.Memory.write_taint_lemma",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Interop.Base.write_taint.fuel_instrumented",
"@fuel_irrelevance_Vale.Interop.Base.write_taint.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_0ffaae0d0679fffbd6ed3d4448c53757",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_389d5d241173f8bfa97353db96d468ed",
"binder_x_40dec2fdc42f7b5efafe5762d6761d53_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_be7c2a18d08c6a4d6565e5e55131f012_3",
"binder_x_d6412aa93b41ab4ee6bc145cbe00b503_2",
"binder_x_d70fe261a81b05988c6be838dae24ef1_4",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.memtaint",
"equation_with_fuel_Vale.Interop.Base.write_taint.fuel_instrumented",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"fuel_guarded_inversion_Vale.X64.Machine_s.taint",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "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_GreaterThanOrEqual",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1840f272ec40e2885d1f3745fe21a00c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_aba125c2fdf18c30de849e118ca1f35e",
"refinement_interpretation_Tm_refine_d0ef603fa357a33a7efe8074f74c27a6",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok",
"well-founded-ordering-on-nat"
],
0,
"b688c17489ece20af0f79421b4270dcf"
],
[
"Vale.X64.Memory.valid_memtaint",
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.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_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_0ffaae0d0679fffbd6ed3d4448c53757",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_aa21ce7dd46ea14789673caa849b06b9",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_389d5d241173f8bfa97353db96d468ed",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_0",
"binder_x_d6412aa93b41ab4ee6bc145cbe00b503_2",
"binder_x_d9f194af42fcfbf66c0386a698f525e8_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Arch.HeapImpl.ValeHeap",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Interop.Base.create_memtaint",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"equation_Vale.X64.Memory.valid_taint_bufs",
"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.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Interop.Base.write_taint",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"kinding_Vale.X64.Machine_s.taint@tok", "l_or-interp",
"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_BarBar", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_src",
"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_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_583a50db1a2cdcdfc370343c05be25c6",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_aba125c2fdf18c30de849e118ca1f35e",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_kinding_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"subterm_ordering_Prims.Cons", "typing_FStar.Ghost.reveal",
"typing_FStar.Map.const", "typing_FStar.Map.domain",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_FStar.Set.mem", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"4c6a007af0a65de724f751c9200d65b8"
]
]
]
Computing file changes ...
