fact: Definition dijk_inner_forloop_inv (g: @DijkGG size inf) sh src u ti min_item keys dist_ptr prev_ptr priq_ptr keys_ptr h graph_ptr := EX i : Z, EX prev' : list V, EX dist' : list Z, EX popped' : list V, EX h' : heap, PROP ( forall dst, vvalid g dst -> inv_popped g src popped' prev' dist' dst; forall dst, 0 <= dst < i -> inv_unpopped g src popped' prev' dist' dst; forall dst, i <= dst < size -> inv_unpopped_weak g src popped' prev' dist' dst u; forall dst, 0 <= dst < i -> inv_unseen g src popped' prev' dist' dst; forall dst, i <= dst < size -> inv_unseen_weak g src popped' prev' dist' dst u; Znth src dist' = 0; Znth src prev' = src; popped' <> [] -> In src popped'; src_picked_first h' src popped'; In u popped'; Zlength dist' = size; Zlength prev' = size; heap_capacity h' = size; @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'); in_heap_or_popped popped' h'; Forall (fun item => 0 <= Int.signed (heap_item_payload item) < size) (heap_items h'); forall i, vvalid g i -> keys_dist_linked_correctly i keys (map Int.repr dist') h'; NoDup (map heap_item_payload (heap_items h')); forall some_item : heap_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 _u (Vint (Int.repr u)); temp _dist (pointer_val_val dist_ptr); temp _prev (pointer_val_val prev_ptr); temp _keys keys_ptr; temp _src (Vint (Int.repr src)); temp _pq priq_ptr; temp _graph (pointer_val_val graph_ptr); temp _temp (pointer_val_val ti)) 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); @SpaceAdjMatGraph size CompSpecs sh id g (pointer_val_val graph_ptr); hitem min_item (pointer_val_val ti); data_at Tsh (tarray tint (heap_capacity h)) (map Vint (map Int.repr keys)) keys_ptr; free_tok (pointer_val_val ti) 12; free_tok keys_ptr (heap_capacity h * 4)).
imports: CertiGraph.graph.SpaceAdjMatGraph2 CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_math_proof CertiGraph.dijkstra.dijkstra_spec2 CertiGraph.dijkstra.dijkstra_constants