proposition: Lemma body_getCell: semax_body Vprog Gprog f_getCell getCell_spec.
proof: Proof. start_function. rewrite (SpaceAdjMatGraph_unfold' _ _ _ addresses u); trivial. assert ((Zlength (map Int.repr (Znth u (@graph_to_symm_mat size g)))) = size). { unfold graph_to_symm_mat, graph_to_mat, vert_to_list. rewrite Znth_map; repeat rewrite Zlength_map. all: rewrite nat_inc_list_Zlength, Z2Nat.id; lia. } assert (0 <= i < Zlength (map Int.repr (Znth u (@graph_to_symm_mat size g)))) by lia. assert (0 <= i < Zlength (Znth u (@graph_to_symm_mat size g))). { rewrite Zlength_map in H2. lia. } Intros. freeze FR := (iter_sepcon _ _) (iter_sepcon _ _). unfold list_rep. assert_PROP (force_val (sem_add_ptr_int tint Signed (force_val (sem_add_ptr_int (tarray tint size) Signed (pointer_val_val graph_ptr) (Vint (Int.repr u)))) (Vint (Int.repr i))) = field_address (tarray tint size) [ArraySubsc i] (@list_address size CompSpecs (pointer_val_val graph_ptr) u)). { entailer!. unfold list_address. simpl. rewrite field_address_offset. 1: { rewrite offset_offset_val; simpl; f_equal. rewrite Z.add_0_l. f_equal. lia. } destruct H6 as [? [? [? [? ?]]]]. unfold field_compatible; split3; [| | split3]; simpl; auto. } forward. forward. thaw FR. rewrite (SpaceAdjMatGraph_unfold' _ _ _ addresses u); trivial. entailer!. Qed.
imports: CertiGraph.prim.prim_env CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.graph.MathUAdjMatGraph CertiGraph.prim.prim_constants CertiGraph.graph.SpaceUAdjMatGraph3 CertiGraph.prim.noroot_prim_spec