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.MemoryAdapters.fst.hints
[
"�vg\u0019�sO��`\u001d\u0019��\n",
[
[
"Vale.X64.MemoryAdapters.as_vale_buffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.pos", "equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.mut_to_b8",
"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.Interop.Views.down_view128",
"equation_Vale.Interop.Views.down_view16",
"equation_Vale.Interop.Views.down_view32",
"equation_Vale.Interop.Views.down_view64",
"equation_Vale.Interop.Views.down_view8",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"function_token_typing_FStar.UInt8.t",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"proj_equation_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_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Down.View_n",
"projection_inverse_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_Vale.Interop.Types.Buffer_rel",
"projection_inverse_Vale.Interop.Types.Buffer_rrel",
"projection_inverse_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"typing_LowStar.BufferView.Down.__proj__View__item__n",
"typing_LowStar.BufferView.Down.get_view",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n"
],
0,
"ff7c40fc5c1f2563242d79758d118de4"
],
[
"Vale.X64.MemoryAdapters.as_vale_immbuffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_Prims.eqtype", "equation_Prims.pos",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Base.imm_to_b8",
"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.Interop.Views.down_view128",
"equation_Vale.Interop.Views.down_view16",
"equation_Vale.Interop.Views.down_view32",
"equation_Vale.Interop.Views.down_view64",
"equation_Vale.Interop.Views.down_view8",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"function_token_typing_FStar.UInt8.t",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"proj_equation_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_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Down.View_n",
"projection_inverse_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_Vale.Interop.Types.Buffer_rel",
"projection_inverse_Vale.Interop.Types.Buffer_rrel",
"projection_inverse_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_LowStar.BufferView.Down.__proj__View__item__n",
"typing_LowStar.BufferView.Down.get_view",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n"
],
0,
"8df224fbc71d0112660a0e43c4f3bfaf"
],
[
"Vale.X64.MemoryAdapters.stack_eq",
1,
1,
0,
[ "@query", "equation_Vale.X64.Stack_i.vale_stack" ],
0,
"29edcea89c2845197753ca6228cea4d3"
],
[
"Vale.X64.MemoryAdapters.as_vale_stack",
1,
1,
0,
[ "@query", "equation_Vale.X64.Stack_i.vale_stack" ],
0,
"a59358acd3ad337aa609c4b94672325b"
],
[
"Vale.X64.MemoryAdapters.buffer_addr_is_nat64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_typing", "lemma_FStar.UInt.pow2_values",
"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",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Arch.HeapImpl._ih",
"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_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"67ce9ff641e708b296c1a6b5293b65ea"
],
[
"Vale.X64.MemoryAdapters.code_equiv",
1,
1,
0,
[
"@query", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp"
],
0,
"d8c7bb0c21f12bb0e2d3e2fd4787e7d1"
],
[
"Vale.X64.MemoryAdapters.ins_equiv",
1,
1,
0,
[ "@query", "equation_Vale.X64.Decls.ins" ],
0,
"58e1c92cc84b6a5451ff3f692a47d19a"
],
[
"Vale.X64.MemoryAdapters.ocmp_equiv",
1,
1,
0,
[ "@query", "equation_Vale.X64.Decls.ocmp" ],
0,
"7b1fea3b4492d6c159d378b4d78508be"
]
]
]
Computing file changes ...
