proposition: Lemma body_getCell: semax_body Vprog Gprog f_getCell getCell_spec.
proof: Proof. start_function. unfold SpaceAdjMatGraph'. assert (0 <= size) by lia. assert (Forall (fun list : list Z => Zlength list = size) (@graph_to_mat size g eformat)). { rewrite Forall_forall. intros. unfold graph_to_mat in H3. apply list_in_map_inv in H3. destruct H3 as [? [? _]]. subst x. unfold vert_to_list. apply Zlength_map. } assert ((0 <= u * 8 + i < Zlength (map Int.repr (@graph_to_list size g eformat)))). { rewrite Zlength_map, (graph_to_list_Zlength _ _ size); trivial. rewrite <- size_eq. split; [lia|]. replace size with (size - 1 + 1) at 2 by lia. rewrite Z.mul_add_distr_r, Z.mul_1_l. apply Z.add_le_lt_mono; try lia. apply Zmult_le_compat_r; lia. } rewrite Zlength_map, (graph_to_list_Zlength _ _ size) in H4; trivial. forward. forward. entailer!. f_equal. f_equal. apply graph_to_list_to_mat; trivial; lia. Qed.
imports: CertiGraph.prim.prim_env CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.graph.MathUAdjMatGraph CertiGraph.prim.prim_constants CertiGraph.graph.SpaceUAdjMatGraph2 CertiGraph.prim.prim_spec2