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.AsLowStar.Test.fst.hints
[
"&@�\u0006�\u0015\u0011���w����H",
[
[
"Vale.AsLowStar.Test.as_t",
1,
1,
0,
[ "@query" ],
0,
"1becb897196046a82b902a643fba1301"
],
[
"Vale.AsLowStar.Test.as_normal_t",
1,
1,
0,
[ "@query" ],
0,
"23386513330ac58b120d68c512100c1f"
],
[
"Vale.AsLowStar.Test.dom",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"3b0801ff3ee73246e543f42ca7631618"
],
[
"Vale.AsLowStar.Test.call_c_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"148526c35cee54062499f3b84e64e368"
],
[
"Vale.AsLowStar.Test.call_c",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"32ad6e097cb268b89282f540aa06b459"
],
[
"Vale.AsLowStar.Test.vm_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.vm_post",
"equation_Vale.AsLowStar.Test.vm_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Test.X64.Vale_memcpy.va_ens_memcpy",
"equation_Vale.Test.X64.Vale_memcpy.va_req_memcpy",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_0bd493576e8c93a6a32769ac846e5c65",
"interpretation_Tm_abs_d43e6408a16a67640d4931d293ef5308",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"b34bae07dd6766c6ff946f48dc0c80bc"
],
[
"Vale.AsLowStar.Test.vm_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.b64",
"equation_Vale.AsLowStar.Test.vm_post",
"equation_Vale.AsLowStar.Test.vm_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Test.X64.Vale_memcpy.va_ens_memcpy",
"equation_Vale.Test.X64.Vale_memcpy.va_req_memcpy",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_0bd493576e8c93a6a32769ac846e5c65",
"interpretation_Tm_abs_d43e6408a16a67640d4931d293ef5308",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.MemoryAdapters.as_vale_buffer",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"c61d97211928f99f03d4dc1382cca29f"
],
[
"Vale.AsLowStar.Test.lowstar_memcpy_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.AsLowStar.Test.vm_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"ebdacffd7696142dcdf1d8c2c117ec0d"
],
[
"Vale.AsLowStar.Test.lowstar_memcpy",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.AsLowStar.Test.vm_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"176f2db27dbd9f529c5bd89295825ee7"
],
[
"Vale.AsLowStar.Test.test",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.pos",
"equation_Vale.AsLowStar.Test.b64",
"equation_Vale.Interop.Types.view_n", "int_inversion",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Interop.Types.view_n",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"d9935a86942ded621bb1e941483c93ef"
],
[
"Vale.AsLowStar.Test.itest",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.pos",
"equation_Vale.AsLowStar.Test.ib64",
"equation_Vale.Interop.Types.view_n", "int_inversion",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_immbuffer_len",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Interop.Types.view_n",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"a457e18f66c6e2eefdab88c7373a0b93"
],
[
"Vale.AsLowStar.Test.memcpy_test",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"constructor_distinct_Vale.Interop.Base.TD_Buffer",
"constructor_distinct_Vale.Interop.Base.TD_ImmBuffer",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.ImmutableBuffer.ibuffer",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.LowStarSig.arg_as_nat64",
"equation_Vale.AsLowStar.Test.code_memcpy",
"equation_Vale.AsLowStar.Test.t64_imm",
"equation_Vale.AsLowStar.Test.t64_mod",
"equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.coerce",
"equation_Vale.Interop.Base.default_bq",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.X64.arg_reg_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.register_of_arg_i",
"equation_Vale.Test.X64.Vale_memcpy.va_req_memcpy",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Words_s.nat64",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"int_inversion", "int_typing",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_immbuffer_len",
"lemma_Vale.AsLowStar.MemoryHelpers.loc_disjoint_sym",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Interop.X64.Rel_of_arg",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__2",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__2",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2",
"projection_inverse_Vale.Interop.X64.Rel_of_arg",
"refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_276eccb33523dc1414bb9a7bcc29f524",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"refinement_interpretation_Tm_refine_a9ef6a967104113b0ce5e80bff4ad89c",
"refinement_interpretation_Tm_refine_d693411ac8c269021ada5215b4077250",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_arg",
"token_correspondence_Vale.Interop.X64.register_of_arg_i",
"typing_FStar.Seq.Base.length",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Prims.pow2",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.MemoryAdapters.as_vale_buffer",
"typing_Vale.X64.MemoryAdapters.as_vale_immbuffer",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"25faa78bf8b8a14e163d89931bf54319"
],
[
"Vale.AsLowStar.Test.empty_list",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"projection_inverse_Prims.Nil_a"
],
0,
"16b812be6be5903d7578d73fb4386f9f"
],
[
"Vale.AsLowStar.Test.aesni_dom",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Prims.nat",
"equation_Vale.Interop.X64.max_stdcall",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"kinding_Vale.Interop.Base.td@tok", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Interop.X64.max_stdcall"
],
0,
"70c788cbd330984447abb310623d8a9a"
],
[
"Vale.AsLowStar.Test.with_len",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.List.Tot.Base.length"
],
0,
"a6694b53c96caa4ab850a680cf30dad9"
],
[
"Vale.AsLowStar.Test.aesni_lemma'",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp",
"equation_Vale.AsLowStar.Test.aesni_post",
"equation_Vale.AsLowStar.Test.aesni_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8c094393c9c948dad8330534aa6d28dc",
"token_correspondence_Vale.AsLowStar.Test.aesni_post",
"token_correspondence_Vale.AsLowStar.Test.aesni_pre",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_aesni_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"bdbd65936380940a7275cedb0a7b6a50"
],
[
"Vale.AsLowStar.Test.aesni_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AsLowStar.Test.aesni_post",
"equation_Vale.AsLowStar.Test.aesni_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.Interop.Assumptions.win"
],
0,
"3312d63da46ea3d0b8888e5cdf0603d5"
],
[
"Vale.AsLowStar.Test.lowstar_aesni_t",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.aesni_dom",
"equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_636ac37489fe4d6466df30f4834f34eb",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.AsLowStar.Test.aesni_dom"
],
0,
"515079c42e9cdb8616b7d5ce2789a2a4"
],
[
"Vale.AsLowStar.Test.lowstar_aesni",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.aesni_dom",
"equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.AsLowStar.Test.aesni_dom",
"typing_Vale.AsLowStar.Test.empty_list"
],
0,
"91ef6f80afc36e07bef8b0b41fc0d300"
],
[
"Vale.AsLowStar.Test.aesni_test",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.squash",
"equation_Vale.AsLowStar.Test.code_aesni",
"equation_Vale.Interop.Base.coerce",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.X64.MemoryAdapters.mem_eq",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.Interop.Assumptions.win"
],
0,
"b7466b1c23db48269beb5badbf0cf745"
],
[
"Vale.AsLowStar.Test.ta_dom",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"390eec1c11a017501c629356ec82a0ac"
],
[
"Vale.AsLowStar.Test.ta_lemma'",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.ta_post",
"equation_Vale.AsLowStar.Test.ta_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Test.X64.Args.va_ens_test",
"equation_Vale.Test.X64.Args.va_req_test",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_6b5a63314305fe66308648aac7ec35ea",
"interpretation_Tm_abs_dbd0f2aae0b8e33479a9baefe87dd839",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"97a22960a3ac7ef9ab4fb87be1c4b3fd"
],
[
"Vale.AsLowStar.Test.ta_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.ta_post",
"equation_Vale.AsLowStar.Test.ta_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Test.X64.Args.va_ens_test",
"equation_Vale.Test.X64.Args.va_req_test",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"interpretation_Tm_abs_6b5a63314305fe66308648aac7ec35ea",
"interpretation_Tm_abs_dbd0f2aae0b8e33479a9baefe87dd839",
"lemma_Vale.X64.Memory.loc_includes_none",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"cfd8995aca042c33cc4fa2fa6efd8900"
],
[
"Vale.AsLowStar.Test.lowstar_ta_t",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.AsLowStar.Test.ta_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"typing_Vale.AsLowStar.Test.empty_list",
"typing_Vale.AsLowStar.Test.ta_dom"
],
0,
"1fcd2f46f3d9f3fb720f76b238879b6f"
],
[
"Vale.AsLowStar.Test.lowstar_ta",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.AsLowStar.Test.ta_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"typing_Vale.AsLowStar.Test.empty_list",
"typing_Vale.AsLowStar.Test.ta_dom"
],
0,
"f43fdba41005e0d5bd67364dddfb5605"
],
[
"Vale.AsLowStar.Test.as_t",
2,
1,
0,
[ "@query" ],
0,
"08d10eb33441f97cf1324e37138dff85"
],
[
"Vale.AsLowStar.Test.as_normal_t",
2,
1,
0,
[ "@query" ],
0,
"e66948dc5241823dd342bb9d332a6764"
],
[
"Vale.AsLowStar.Test.dom",
2,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"1867c020e1fdea7d56187a9dcb7ea879"
],
[
"Vale.AsLowStar.Test.call_c_t",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"dc44d90a80f3691ae2ba259ec7e45460"
],
[
"Vale.AsLowStar.Test.call_c",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"6ea2ef77a3164c5b48721f8e0b7fe074"
],
[
"Vale.AsLowStar.Test.vm_lemma'",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"constructor_distinct_Vale.Interop.Base.TD_Buffer",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.b64",
"equation_Vale.AsLowStar.Test.t64_mod",
"equation_Vale.AsLowStar.Test.vm_post",
"equation_Vale.AsLowStar.Test.vm_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.Base.arg", "equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.td_as_type",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Test.X64.Vale_memcpy.va_ens_memcpy",
"equation_Vale.Test.X64.Vale_memcpy.va_req_memcpy",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_0bd493576e8c93a6a32769ac846e5c65",
"interpretation_Tm_abs_d43e6408a16a67640d4931d293ef5308",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__2",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"d7d4185510b37d0ffe382cd89073cfa5"
],
[
"Vale.AsLowStar.Test.vm_lemma",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.b64",
"equation_Vale.AsLowStar.Test.vm_post",
"equation_Vale.AsLowStar.Test.vm_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Test.X64.Vale_memcpy.va_ens_memcpy",
"equation_Vale.Test.X64.Vale_memcpy.va_req_memcpy",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_0bd493576e8c93a6a32769ac846e5c65",
"interpretation_Tm_abs_d43e6408a16a67640d4931d293ef5308",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.MemoryAdapters.as_vale_buffer",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"af38ad2b821d4adb0e06b0c39f270fb6"
],
[
"Vale.AsLowStar.Test.lowstar_memcpy_t",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.AsLowStar.Test.vm_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"ed9aaf008f979dc4d53215c734f7e949"
],
[
"Vale.AsLowStar.Test.lowstar_memcpy",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.dom",
"equation_Vale.AsLowStar.Test.vm_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"typing_Vale.AsLowStar.Test.dom"
],
0,
"d1f3d06b9e7cfe7aa720ab0c08f66e52"
],
[
"Vale.AsLowStar.Test.test",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.pos", "equation_Vale.AsLowStar.Test.b64",
"equation_Vale.Interop.Types.view_n",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Interop.Types.view_n",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"4307add39ce5fc8335d9a70a847bea1b"
],
[
"Vale.AsLowStar.Test.itest",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.pos", "equation_Vale.AsLowStar.Test.ib64",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"lemma_Vale.AsLowStar.MemoryHelpers.as_vale_immbuffer_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Interop.Types.view_n",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"7d60a283ecdd682097f7cefa988494ae"
],
[
"Vale.AsLowStar.Test.empty_list",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"projection_inverse_Prims.Nil_a"
],
0,
"37ccf70eac0e0c3ebd208e4f258136d1"
],
[
"Vale.AsLowStar.Test.aesni_dom",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Prims.nat",
"equation_Vale.Interop.X64.max_stdcall",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"kinding_Vale.Interop.Base.td@tok", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Interop.X64.max_stdcall"
],
0,
"f48f039f2627b65eed62a8d86acc0b80"
],
[
"Vale.AsLowStar.Test.with_len",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.List.Tot.Base.length"
],
0,
"485e2a80fe7bc46940245058f4c5d4d1"
],
[
"Vale.AsLowStar.Test.aesni_lemma'",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp",
"equation_Vale.AsLowStar.Test.aesni_post",
"equation_Vale.AsLowStar.Test.aesni_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_edf341de0fd48b153ad2841ecf110c4c",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_aesni_stdcall"
],
0,
"213e0bd5d264a09b6d9b4d0325f98590"
],
[
"Vale.AsLowStar.Test.aesni_lemma",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AsLowStar.Test.aesni_post",
"equation_Vale.AsLowStar.Test.aesni_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.Interop.Assumptions.win"
],
0,
"47e848fae539ab28fa2ecc1dfca2abeb"
],
[
"Vale.AsLowStar.Test.lowstar_aesni_t",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.aesni_dom",
"equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_636ac37489fe4d6466df30f4834f34eb",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.AsLowStar.Test.aesni_dom"
],
0,
"ed2add75477e3b32f46e20049954ab24"
],
[
"Vale.AsLowStar.Test.lowstar_aesni",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.aesni_dom",
"equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.AsLowStar.Test.aesni_dom",
"typing_Vale.AsLowStar.Test.empty_list"
],
0,
"5bfc468e2eb3a9ed8e0a23216ac0f4df"
],
[
"Vale.AsLowStar.Test.ta_dom",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"bf0f8dae3b1e2c096e71a4b5013984b4"
],
[
"Vale.AsLowStar.Test.ta_lemma'",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.ta_post",
"equation_Vale.AsLowStar.Test.ta_pre",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Test.X64.Args.va_ens_test",
"equation_Vale.Test.X64.Args.va_req_test",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_6b5a63314305fe66308648aac7ec35ea",
"interpretation_Tm_abs_dbd0f2aae0b8e33479a9baefe87dd839",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"19deb9f50a747b70e1246f280a2adfad"
],
[
"Vale.AsLowStar.Test.ta_lemma",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.AsLowStar.Test.ta_post",
"equation_Vale.AsLowStar.Test.ta_pre",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Test.X64.Args.va_ens_test",
"equation_Vale.Test.X64.Args.va_req_test",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"interpretation_Tm_abs_6b5a63314305fe66308648aac7ec35ea",
"interpretation_Tm_abs_dbd0f2aae0b8e33479a9baefe87dd839",
"lemma_Vale.X64.Memory.loc_includes_none",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.Memory.loc_union",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"78d388dc0207cc9c86b6be7609253c99"
],
[
"Vale.AsLowStar.Test.lowstar_ta_t",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.AsLowStar.Test.ta_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"typing_Vale.AsLowStar.Test.empty_list",
"typing_Vale.AsLowStar.Test.ta_dom"
],
0,
"7231bbb5d5bc89cbd76054a6d08de1cd"
],
[
"Vale.AsLowStar.Test.lowstar_ta",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Vale.AsLowStar.Test.empty_list",
"equation_Vale.AsLowStar.Test.ta_dom",
"equation_Vale.Interop.Base.arg",
"equation_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b",
"refinement_interpretation_Tm_refine_a23f344253b4e5d4db610ee3662a1798",
"typing_Vale.AsLowStar.Test.empty_list",
"typing_Vale.AsLowStar.Test.ta_dom"
],
0,
"f954e85433c5237b2afcc1f923a9f8d9"
]
]
]
Computing file changes ...
