fact: Definition dijk_setup_loop_inv g sh src dist_ptr prev_ptr priq_ptr keys_ptr temp_ptr arr addresses := EX i : Z, EX h : heap, EX keys: list key_type, EX dist_and_prev : list int, PROP (heap_capacity h = size; heap_size h = i; forall j, 0 <= j < i -> keys_dist_linked_correctly j keys dist_and_prev h; dist_and_prev = repeat (Int.repr inf) (Z.to_nat i); Zlength keys = i; forall j, 0 <= j < i -> In (Znth j keys) (proj_keys h); Permutation (map heap_item_payload (heap_items h)) (map Int.repr (nat_inc_list (Z.to_nat i))); Forall (fun item => heap_item_priority item = Int.repr inf) (heap_items h); NoDup (map heap_item_payload (heap_items h)); forall j, 0 <= j < i -> In (Znth j keys, Int.repr inf, Int.repr j) (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 j, 0 <= j < i -> exists j_item, In j_item (heap_items h) /\ j = Int.signed (heap_item_payload j_item); NoDup keys; (Permutation keys (map heap_item_key (heap_items h)))) LOCAL (temp _dist (pointer_val_val dist_ptr); temp _prev (pointer_val_val prev_ptr); temp _src (Vint (Int.repr src)); temp _pq priq_ptr; temp _graph (pointer_val_val arr); temp _size (Vint (Int.repr size)); temp _keys (pointer_val_val keys_ptr); temp _inf (Vint (Int.repr inf)); temp _temp (pointer_val_val temp_ptr)) SEP (valid_pq priq_ptr h; hitem_ (pointer_val_val temp_ptr); data_at Tsh (tarray tint size) (map Vint (map Int.repr keys) ++ (repeat Vundef (Z.to_nat (size-i)))) (pointer_val_val keys_ptr); data_at Tsh (tarray tint size) (map Vint dist_and_prev ++ (repeat Vundef (Z.to_nat (size-i)))) (pointer_val_val prev_ptr); data_at Tsh (tarray tint size) (map Vint dist_and_prev ++ (repeat Vundef (Z.to_nat (size-i)))) (pointer_val_val dist_ptr); @SpaceAdjMatGraph size CompSpecs sh id g (pointer_val_val arr) addresses; free_tok (pointer_val_val keys_ptr) (size * sizeof tint); free_tok (pointer_val_val temp_ptr) (sizeof (Tstruct _structItem noattr))).
imports: CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_math_proof CertiGraph.dijkstra.dijkstra_spec1