Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Vale.Arch.Heap.fst.hints
[
"��\u0003�E��cH\u0000�{\u007f+%�",
[
[
"Vale.Arch.Heap.heaplet_upd_f",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapImpl_interpretation_Tm_arrow_8891fc688091edcbfb9fd01cb7e859aa",
"bool_inversion", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"kinding_Vale.Arch.HeapImpl.vale_heap@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomConcat",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_SelConcat2",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_intersect",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_inner",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"token_correspondence_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout_inner__item__vl_heaplet_sets",
"typing_FStar.Map.concat", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Set.intersect", "typing_FStar.Set.mem",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout_inner__item__vl_heaplet_sets",
"typing_Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh",
"typing_Vale.Lib.Map16.sel"
],
0,
"efeaa74ba315f3764f6a71b2470c8ffe"
],
[
"Vale.Arch.Heap.heap_upd",
1,
1,
0,
[
"@query", "equation_Vale.Arch.Heap.heap_get",
"equation_Vale.Arch.Heap.heap_taint",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint"
],
0,
"fb645833eb98b8899be5cdef38f7f13a"
],
[
"Vale.Arch.Heap.heap_create_machine",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0",
"equation_Vale.Interop.Heap_s.down_mem_t",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"typing_Vale.Interop.down_mem"
],
0,
"1a41afee5721538e6e09c6739ba5c0b2"
],
[
"Vale.Arch.Heap.one_heaplet",
1,
1,
0,
[
"@query", "kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Ghost.reveal_hide"
],
0,
"2d82424bf1b40cab8bde92c054377a65"
],
[
"Vale.Arch.Heap.heap_create_impl",
1,
1,
0,
[
"@query", "equation_Vale.Arch.Heap.heap_create_machine",
"equation_Vale.Arch.Heap.heap_get",
"equation_Vale.Arch.Heap.heap_taint",
"equation_Vale.Arch.Heap.one_heaplet",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_mh"
],
0,
"d10ecd01c1680aee5c0e169b909d5423"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...