proposition: Lemma body_create_heap: semax_body Vprog Gprog f_create_heap create_heap_spec.
proof: Proof. start_function. forward_call (heap_type, gv). Intros h. if_tac. - subst h; forward_if False; [| first [exfalso; now apply H | inversion H ]]. unfold all_string_constants; Intros. forward_call. contradiction. - Intros. forward_if True; [contradiction | forward; entailer!! |]. Intros. assert_PROP (isptr h) by entailer!. remember (Vundef, (Vundef, (Vundef,Vundef))) as vn. assert_PROP (field_compatible heap_type [StructField _spaces] h) by entailer!. replace_SEP 2 (data_at Ews heap_type (default_val heap_type) h) by entailer!!. change (default_val heap_type) with (repeat (Vundef, (Vundef, (Vundef,Vundef))) (Z.to_nat MAX_SPACES)). rewrite <- Heqvn. rewrite data_at_heaptype_eq; auto. rewrite (split2_data_at_Tarray_space_type Ews MAX_SPACES 1); [| rep_lia | rewrite Zlength_repeat; rep_lia]. rewrite sublist_repeat by rep_lia. simpl repeat at 1. rewrite space_array_1_eq. Intros. forward_call (Ews, h, Z.shiftl 1 LOG_NURSERY_SIZE, gv, sh). + compute; split; auto; discriminate. + Intros p0. freeze [0;1;2;3;5] FR. rewrite <- space_array_1_eq. rewrite sublist_repeat by rep_lia. gather_SEP (data_at Ews (tarray space_type 1) _ h) (data_at Ews (tarray space_type (MAX_SPACES - 1)) _ _). remember (p0, (p0, (offset_val (WORD_SIZE * Z.shiftl 1 LOG_NURSERY_SIZE) p0, offset_val (WORD_SIZE * Z.shiftl 1 LOG_NURSERY_SIZE) p0))) as vh. remember (vh :: repeat vn (Z.to_nat (MAX_SPACES-1))) as vl. replace [vh] with (sublist 0 1 vl). 2: { subst vl; rewrite sublist_one; try lia. - rewrite Znth_0_cons; auto. - rewrite Zlength_cons, Zlength_repeat; rep_lia. } replace (repeat vn (Z.to_nat (MAX_SPACES-1))) with (sublist 1 MAX_SPACES vl) by (rewrite Heqvl, sublist_1_cons, sublist_repeat by rep_lia; auto). rewrite <- split2_data_at_Tarray_space_type; [| rep_lia | rewrite Heqvl, Zlength_cons, Zlength_repeat; rep_lia]. set (v0 := (nullval,(nullval,(nullval,nullval)))). subst vl. rewrite <- data_at_heaptype_eq; auto. forward_for_simple_bound MAX_SPACES (EX i: Z, PROP ( ) LOCAL (temp _h h; gvars gv) SEP (data_at Ews heap_type (vh :: repeat v0 (Z.to_nat (i - 1)) ++ repeat vn (Z.to_nat (MAX_SPACES - i))) h; FRZL FR))%assert. * entailer!!. * Opaque Znth. forward; [apply prop_right; rep_lia | ]. rewrite (repeat_cons (MAX_SPACES - i)) at 2 by rep_lia. rewrite Znth_repeat_app by apply (proj1 H2). rewrite Heqvn at 2. rewrite (repeat_cons (MAX_SPACES - i)) by lia. rewrite upd_Znth_repeat_app by apply (proj1 H2). forward; [apply prop_right; rep_lia | ]. rewrite Znth_repeat_app by apply (proj1 H2). rewrite upd_Znth_repeat_app by apply (proj1 H2). forward; [apply prop_right; rep_lia | ]. rewrite Znth_repeat_app by apply (proj1 H2). rewrite upd_Znth_repeat_app by apply (proj1 H2). forward; [apply prop_right; rep_lia | ]. rewrite Znth_repeat_app by apply (proj1 H2). rewrite upd_Znth_repeat_app by apply (proj1 H2). simpl fst; simpl snd. replace (i + 1 - 1) with i by lia. rewrite !Int.signed_repr by rep_lia. change (Vlong _, _) with v0. replace (MAX_SPACES - i - 1) with (MAX_SPACES - (i + 1)) by lia. change (v0 :: repeat vn (Z.to_nat (MAX_SPACES - (i + 1)))) with ([v0] ++ repeat vn (Z.to_nat (MAX_SPACES - (i + 1)))). rewrite app_assoc. replace (repeat v0 (Z.to_nat (i - 1)) ++ [v0]) with (repeat v0 (Z.to_nat i)). 1: entailer!!. replace [v0] with (repeat v0 (Z.to_nat 1)) by (simpl; auto). rewrite <- repeat_app. f_equal. rewrite <- Z2Nat.inj_add by lia. f_equal. lia. * replace (MAX_SPACES - MAX_SPACES) with 0 by lia. simpl repeat at 2. rewrite app_nil_r. thaw FR. change (Z.shiftl 1 LOG_NURSERY_SIZE) with NURSERY_SIZE in *. assert (v0 = zero_triple) by (subst v0; unfold zero_triple; reflexivity). rewrite H2. forward. Exists h p0. entailer!!. Transparent Znth. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)