Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.Arch.HeapImpl.fst.hints
[
"�\u0007���T���3ͳ��P",
[
[
"Vale.Arch.HeapImpl.buffer",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"c6afc22fde99d5e1109b756deab9c040"
],
[
"Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_buffer",
1,
1,
0,
[
"@query", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ"
],
0,
"a2cba72650ef3b8e815dc08fc9cde87d"
],
[
"Vale.Arch.HeapImpl.__proj__ValeHeap__item__ih",
1,
1,
0,
[
"@query", "proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_mh"
],
0,
"ae0a93e09cb2787bf97e7bcd884efe4f"
],
[
"Vale.Arch.HeapImpl.mi_heap_upd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0",
"Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.down_mem_t",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_mh",
"refinement_interpretation_Tm_refine_1d91a1ccb8ed3b9c6990d1f08f8c1332",
"refinement_interpretation_Tm_refine_2688fdb7e84bdee1cf9ca4c017aaa352",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"typing_FStar.Map.domain",
"typing_Vale.Arch.HeapImpl.__proj__ValeHeap__item__ih",
"typing_Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh",
"typing_Vale.Interop.down_mem"
],
0,
"0236db4d67502bb139347095054c26e0"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...