proposition: Lemma body_makeSet: semax_body Vprog Gprog f_makeSet makeSet_spec.
proof: Proof. start_function. forward_call (sh, Z.mul V 8). - assert (Int.min_signed <= 8 <= Int.max_signed) by rep_lia. assert (Int.min_signed <= V <= Int.max_signed). { split; rewrite Z.le_lteq; left. - rep_lia. - apply Z.le_lt_trans with (Int.max_signed / 8); [intuition | apply Z.div_lt; lia]. } rewrite !Int.signed_repr; auto. split. 1: lia. assert (Z.mul 8 (Int.max_signed /8) <= Int.max_signed) by (apply Z_mult_div_ge; intuition). rep_lia. - split. 1: lia. assert (Z.mul 8 (Int.max_signed /8) <= Int.max_signed) by (apply Z_mult_div_ge; intuition). rep_lia. - Intros rt. assert (memory_block sh (V * 8) (pointer_val_val rt) = data_at_ sh (tarray vertex_type V) (pointer_val_val rt)). { assert (memory_block sh (V * 8) (pointer_val_val rt) = memory_block sh (sizeof (tarray vertex_type V)) (pointer_val_val rt)). { simpl sizeof. rewrite Zmax0r. 2: intuition. assert (V * 8 = 8 * V)%Z by lia. rewrite H1. auto. } rewrite <- memory_block_data_at_; auto. apply malloc_compatible_field_compatible; auto. unfold malloc_compatible in *. destruct (pointer_val_val rt); auto. destruct H0. split; auto. simpl sizeof. rewrite Zmax0r; intuition. } rewrite H1. clear H1. assert (data_at_ sh (tarray vertex_type V) (pointer_val_val rt) = data_at sh (tarray vertex_type V) (progressive_list O (Z.to_nat V)) (pointer_val_val rt)). { unfold data_at_, field_at_, data_at. assert (default_val (nested_field_type (tarray vertex_type V) []) = list_repeat (Z.to_nat V) (Vundef, Vundef)) by reflexivity. rewrite H1. rewrite progressive_list_repeat. auto. } rewrite H1. clear H1. forward_for_simple_bound V (EX i: Z, PROP () LOCAL (temp _subsets (pointer_val_val rt); temp _V (Vint (Int.repr V))) SEP (progressive_array sh i V rt)); unfold progressive_array. + destruct H. apply Z.le_trans with (Int.max_signed / 8); auto. rewrite Z.lt_eq_cases. left. apply Z_div_lt; intuition. + entailer. + Opaque Znth. forward. remember (Znth i (progressive_list (Z.to_nat i) (Z.to_nat V))) as lll. destruct lll. forward. assert (0 <= i < Zlength (progressive_list (Z.to_nat i) (Z.to_nat V))) by (split; [|rewrite Zlength_correct, progressive_list_length, Z2Nat.id]; lia). rewrite upd_Znth_same, upd_Znth_twice; [|auto ..]. unfold progressive_array, data_at. rewrite upd_Znth_progressive_list. 2: rewrite Z2Nat.id; lia. entailer. Transparent Znth. + forward. Exists (makeSet_discrete_Graph (Z.to_nat V)) rt. entailer!. * intros. simpl. rewrite makeSet_vvalid. rewrite Z2Nat.id; lia. * unfold whole_graph, full_graph_at. simpl. Exists (Z.to_nat V). apply andp_right; intros; [apply andp_right; apply prop_right|]. -- intros. rewrite makeSet_vvalid. intuition. -- rewrite Z2Nat.id; lia. -- simpl. unfold vcell_array_at, SAG_VST. rewrite map_length, nat_inc_list_length. rewrite Z2Nat.id. 2: intuition. assert (map (fun x : Z => vgamma (makeSet_discrete_LabeledGraph (Z.to_nat V)) x) (nat_inc_list (Z.to_nat V)) = map (fun x => (0%nat, x)) (nat_inc_list (Z.to_nat V))). { apply list_map_exten. intros. unfold vgamma, UnionFindGraph.vgamma. simpl. rewrite makeSet_dst. simpl. auto. } rewrite H6. clear H6. rewrite list_map_compose. unfold vgamma2cdata. simpl. rewrite <- progressive_nat_inc_list; intuition. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.sample_mark.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.sample_mark.spatial_array_graph Coq.Lists.List