fact: Definition dijk_forloop_inv (g: @DijkGG size inf) sh src keys dist_ptr prev_ptr keys_ptr priq_ptr graph_ptr temp_ptr addresses := EX prev : list V, EX dist : list Z, EX popped : list V, EX h : heap, PROP ( dijkstra_correct g src popped prev dist; Znth src dist = 0; Znth src prev = src; popped <> [] -> In src popped; heap_capacity h = size; forall i, vvalid g i -> keys_dist_linked_correctly i keys (map Int.repr dist) h; src_picked_first h src popped; in_heap_or_popped popped h; @inrange_prev size inf prev; @inrange_dist size inf dist; @inrange_popped size popped; NoDup popped; forall i, vvalid g i -> ~ In i popped -> In (Znth i keys) (proj_keys h); Forall (fun item => 0 <= Int.signed (heap_item_payload item) < size) (heap_items h); NoDup (map heap_item_payload (heap_items h)); forall some_item, In some_item (heap_items h) -> Znth (Int.signed (heap_item_payload some_item)) keys = heap_item_key some_item; forall i, vvalid g i -> ~ In i popped -> exists i_item, In i_item (heap_items h) /\ i = Int.signed (heap_item_payload i_item)) LOCAL (temp _dist (pointer_val_val dist_ptr); temp _prev (pointer_val_val prev_ptr); temp _keys (pointer_val_val keys_ptr); temp _src (Vint (Int.repr src)); temp _pq priq_ptr; temp _graph (pointer_val_val graph_ptr); temp _size (Vint (Int.repr size)); temp _inf (Vint (Int.repr inf)); temp _temp (pointer_val_val temp_ptr)) SEP (valid_pq priq_ptr h; data_at Tsh (tarray tint size) (map Vint (map Int.repr prev)) (pointer_val_val prev_ptr); data_at Tsh (tarray tint size) (map Vint (map Int.repr dist)) (pointer_val_val dist_ptr); data_at Tsh (tarray tint size) (map Vint (map Int.repr keys)) (pointer_val_val keys_ptr); @SpaceAdjMatGraph size CompSpecs sh id g (pointer_val_val graph_ptr) addresses; hitem_ (pointer_val_val temp_ptr); free_tok (pointer_val_val temp_ptr) (sizeof (Tstruct _structItem noattr)); free_tok (pointer_val_val keys_ptr) (size * sizeof tint)).
imports: CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_math_proof CertiGraph.dijkstra.dijkstra_spec1