Revision 2fd16cc5351310efaa66a178d904ce978ad78b23 authored by Bryan Parno on 01 April 2019, 15:28:33 UTC, committed by Bryan Parno on 01 April 2019, 15:28:33 UTC
Test.Vale_memcpy.fst.hints
[
"kkta_��upT�,[",
[
[
"Test.Vale_memcpy.va_req_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.l_imp",
"equation_Prims.squash", "equation_Prims.subtype_of",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"4323c0389a7f677cf02e7d0e6012849c"
],
[
"Test.Vale_memcpy.va_ens_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of", "equation_X64.Vale.Decls.va_state_eq",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"4b18639aef5696a9ea7d6efb62033b54"
],
[
"Test.Vale_memcpy.va_lemma_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "constructor_distinct_Interop.Types.TUInt64",
"eq2-interp", "equality_tok_Interop.Types.TUInt64@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.eq2",
"equation_Prims.l_imp", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Prop_s.prop0", "equation_Types_s.quad32",
"equation_Words_s.nat64",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer64",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.valid_stack_slots",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
"l_and-interp", "l_imp-interp", "l_not-interp",
"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_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_FStar.Seq.Base.seq",
"typing_FStar.Seq.Base.upd",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.eq2", "typing_Prims.l_and",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
"typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies", "typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_Interop.Types.TUInt64@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
],
0,
"28966e5cf3c39198bb14c110d0609b1d"
],
[
"Test.Vale_memcpy.va_wpMonotone_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_Test.Vale_memcpy.va_wp_memcpy",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"c3c63e45f998fc6061de9b6a028ae6f1"
],
[
"Test.Vale_memcpy.va_wpCompute_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Test.Vale_memcpy.va_wp_memcpy",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"30284008d060d27b15b794f99a7f5e29"
],
[
"Test.Vale_memcpy.va_wpProof_memcpy",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"387a0eea8e31f53054cf16c1b429c5c5"
],
[
"Test.Vale_memcpy.va_wpProof_memcpy",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_Test.Vale_memcpy.va_wpCompute_memcpy",
"equation_Test.Vale_memcpy.va_wp_memcpy",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Test.Vale_memcpy.va_wpCompute_memcpy",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"57ed53f9d2314f2d14bc16aea2b75e15"
]
]
]
Computing file changes ...