From 1276d31516d3987306fb38a9e9524c0f2d57194a Mon Sep 17 00:00:00 2001 From: William Mansky Date: Wed, 10 Apr 2024 07:13:21 -0500 Subject: [PATCH] Update verif_incr_gen.v --- progs64/verif_incr_gen.v | 287 ++++++++++++++++++--------------------- 1 file changed, 135 insertions(+), 152 deletions(-) diff --git a/progs64/verif_incr_gen.v b/progs64/verif_incr_gen.v index c313e2716d..3f43e719cf 100644 --- a/progs64/verif_incr_gen.v +++ b/progs64/verif_incr_gen.v @@ -3,49 +3,33 @@ Require Import VST.concurrency.conclib. Require Import VST.concurrency.lock_specs. +Require Import VST.atomics.SC_atomics. Require Import VST.atomics.verif_lock. -Require Import VST.concurrency.ghosts. +Require Import iris_ora.algebra.frac_auth. +Require Import iris.algebra.numbers. +Require Import VST.zlist.sublist. Require Import VST.progs64.incrN. #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined. Definition Vprog : varspecs. mk_varspecs prog. Defined. -Definition spawn_spec := DECLARE _spawn spawn_spec. +Section proofs. -#[local] Program Instance sum_ghost : Ghost := - { G := nat; valid g := True; Join_G a b c := c = (a + b)%nat }. -Next Obligation. -Proof. - exists (fun _ => O). - - intros; hnf; auto. - - intros; eexists; hnf; eauto. - - auto. -Defined. -Next Obligation. -Proof. - constructor. - - intros; hnf in *. - subst; auto. - - intros; hnf in *. - exists (b + c)%nat; split; hnf; lia. - - intros; hnf in *. - lia. - - intros; hnf in *. - lia. -Qed. +Context `{!VSTGS unit Σ, !cinvG Σ, !atomic_int_impl (Tstruct _atom_int noattr), !inG Σ (frac_authR natR)}. +#[local] Instance concurrent_ext_spec : ext_spec _ := concurrent_ext_spec _ (ext_link_prog prog). -#[local] Instance ctr_ghost : Ghost := ref_PCM sum_ghost. +Definition spawn_spec := DECLARE _spawn spawn_spec. -Definition ghost_ref n g := ghost_reference(P := sum_ghost) n g. -Definition ghost_part sh n g := ghost_part(P := sum_ghost) sh n g. -Definition ghost_both sh n1 n2 g := ghost_part_ref(P := sum_ghost) sh n1 n2 g. +Definition ghost_ref n g := own g (●F n : frac_authR _). +Definition ghost_part sh n g := own g (◯F{sh} n : frac_authR _). +Definition ghost_both sh n1 n2 g := own g (●F n1 ⋅ ◯F{sh} n2 : frac_authR _). Definition t_counter := Tstruct _counter noattr. Definition cptr_lock_inv g ctr := - EX z : nat, field_at Ews t_counter [StructField _ctr] (Vint (Int.repr (Z.of_nat z))) ctr * ghost_ref z g. + ∃ z : nat, field_at Ews t_counter [StructField _ctr] (Vint (Int.repr (Z.of_nat z))) ctr ∗ ghost_ref z g. -Definition ctr_handle sh h g ctr n := lock_inv sh h (cptr_lock_inv g ctr) * ghost_part sh n g. +Definition ctr_handle sh h g ctr n := lock_inv sh h (cptr_lock_inv g ctr) ∗ ghost_part sh n g. Definition init_ctr_spec := DECLARE _init_ctr @@ -56,12 +40,12 @@ Definition init_ctr_spec := GLOBALS (gv) SEP (library.mem_mgr gv; data_at_ Ews t_counter (gv _c)) POST [ tvoid ] - EX h : lock_handle, EX g : gname, + ∃ h : lock_handle, ∃ g : gname, PROP () LOCAL () SEP (library.mem_mgr gv; field_at Ews t_counter [StructField _lock] (ptr_of h) (gv _c); spacer Ews 4 8 (gv _c); - ctr_handle Tsh h g (gv _c) O). + ctr_handle 1 h g (gv _c) O). Definition dest_ctr_spec := DECLARE _dest_ctr @@ -71,7 +55,7 @@ Definition dest_ctr_spec := PARAMS () GLOBALS (gv) SEP (field_at Ews t_counter [StructField _lock] (ptr_of h) (gv _c); spacer Ews 4 8 (gv _c); - ctr_handle Tsh h g (gv _c) v) + ctr_handle 1 h g (gv _c) v) POST [ tvoid ] PROP () LOCAL () @@ -79,9 +63,9 @@ Definition dest_ctr_spec := Definition incr_spec := DECLARE _incr - WITH sh1 : share, sh : share, h : lock_handle, g : gname, n : nat, gv: globals + WITH sh1 : share, sh : Qp, h : lock_handle, g : gname, n : nat, gv: globals PRE [ ] - PROP (readable_share sh1; sh <> Share.bot) + PROP (readable_share sh1) PARAMS () GLOBALS (gv) SEP (field_at sh1 t_counter [StructField _lock] (ptr_of h) (gv _c); @@ -94,17 +78,17 @@ Definition incr_spec := Definition thread_lock_R sh1 sh g ctr lockc := - field_at sh1 t_counter [StructField _lock] (ptr_of lockc) ctr * ctr_handle sh lockc g ctr 1%nat. + field_at sh1 t_counter [StructField _lock] (ptr_of lockc) ctr ∗ ctr_handle sh lockc g ctr 1%nat. Definition thread_lock_inv sh1 tsh sh g ctr lockc lockt := selflock (thread_lock_R sh1 sh g ctr lockc) tsh lockt. Definition thread_func_spec := DECLARE _thread_func - WITH y : val, x : share * share * lock_handle * share * lock_handle * gname * globals + WITH y : val, x : share * Qp * lock_handle * Qp * lock_handle * gname * globals PRE [ tptr tvoid ] let '(sh1, tsh, ht, sh, h, g, gv) := x in - PROP (readable_share sh1; tsh <> Share.bot; sh <> Share.bot; ptr_of ht = y) + PROP (readable_share sh1; ptr_of ht = y) PARAMS (y) GLOBALS (gv) SEP (field_at sh1 t_counter [StructField _lock] (ptr_of h) (gv _c); @@ -128,39 +112,45 @@ Lemma ctr_inv_exclusive : forall lg p, exclusive_mpred (cptr_lock_inv lg p). Proof. intros; unfold cptr_lock_inv. - eapply derives_exclusive, exclusive_sepcon1 with (Q := EX z : nat, _), - field_at__exclusive with (sh := Ews)(t := t_counter); auto; simpl; try lia. - Intro z; apply sepcon_derives; [cancel|]. - Exists z; apply derives_refl. + iIntros "((% & ? & ?) & (% & ? & ?))". + rewrite !field_at_field_at_; iApply (field_at__conflict with "[$]"); auto. + { simpl; lia. } +Qed. +#[local] Hint Resolve ctr_inv_exclusive : core. + +Lemma thread_inv_exclusive : forall sh1 sh g p l, + sh1 <> Share.bot -> exclusive_mpred (thread_lock_R sh1 sh g p l). +Proof. + intros; unfold thread_lock_R. + iIntros "((? & ? & ?) & (? & ? & ?))". + rewrite !field_at_field_at_; iApply (field_at__conflict with "[$]"); auto. { simpl; lia. } Qed. -#[export] Hint Resolve ctr_inv_exclusive : core. +#[local] Hint Resolve thread_inv_exclusive : core. -Lemma ctr_handle_share_join : forall sh1 sh2 sh h g ctr v1 v2, sh1 <> Share.bot -> sh2 <> Share.bot -> sepalg.join sh1 sh2 sh -> - ctr_handle sh1 h g ctr v1 * ctr_handle sh2 h g ctr v2 = ctr_handle sh h g ctr (v1 + v2)%nat. +Lemma ctr_handle_share_join : forall sh1 sh2 h g ctr v1 v2, + ctr_handle sh1 h g ctr v1 ∗ ctr_handle sh2 h g ctr v2 ⊣⊢ ctr_handle (sh1 ⋅ sh2) h g ctr (v1 + v2)%nat. Proof. intros; unfold ctr_handle. - erewrite (sepcon_comm (lock_inv _ _ _)), <- sepcon_assoc, (sepcon_assoc (ghost_part _ _ _)), lock_inv_share_join by eauto. - unfold ghost_part; erewrite (sepcon_comm (ghosts.ghost_part _ _ _)), sepcon_assoc, ghost_part_join; eauto. - reflexivity. + rewrite -lock_inv_share_join /ghost_part frac_auth_frag_op own_op. + apply bi.equiv_entails_2; cancel. Qed. Lemma body_init_ctr: semax_body Vprog Gprog f_init_ctr init_ctr_spec. Proof. start_function. forward. - ghost_alloc (ghost_both Tsh O O). - { split; auto. - apply (@self_completable sum_ghost). } + ghost_alloc (ghost_both 1 O O). + { by apply frac_auth_valid. } Intros g. forward_call (gv, fun _ : lock_handle => cptr_lock_inv g (gv _c)). Intros h. forward. forward. - forward_call release_simple (Tsh, h, cptr_lock_inv g (gv _c)). + forward_call release_simple (1%Qp, h, cptr_lock_inv g (gv _c)). { lock_props. unfold cptr_lock_inv. - unfold ghost_both; rewrite <- ghost_part_ref_join. + rewrite /ghost_both own_op. unfold_data_at (data_at _ _ _ _). unfold ghost_ref; Exists O; entailer!. } unfold ctr_handle, ghost_part; Exists h g; entailer!. @@ -171,17 +161,17 @@ Proof. start_function. unfold ctr_handle; Intros. forward. - forward_call (Tsh, h, cptr_lock_inv g (gv _c)). + forward_call (1%Qp, h, cptr_lock_inv g (gv _c)). forward. forward_call freelock_simple (h, cptr_lock_inv g (gv _c)). - { lock_props. } + { lock_props; cancel. } unfold cptr_lock_inv. Intros z. entailer!. - unfold ghost_part, ghost_ref; sep_apply (ref_sub(P := sum_ghost)). - rewrite eq_dec_refl; Intros; subst. - unfold_data_at (data_at _ _ _ _); cancel. - rewrite <- sepcon_emp; apply sepcon_derives; apply own_dealloc. + iIntros "(? & ref & ? & ? & part)". + iDestruct (own_valid_2 with "ref part") as %Hv%frac_auth_agree. + inv Hv. + unfold_data_at (data_at _ _ _ _); iFrame. Qed. Lemma body_incr: semax_body Vprog Gprog f_incr incr_spec. @@ -196,11 +186,11 @@ Proof. forward. forward. gather_SEP (ghost_part _ _ _) (ghost_ref _ _). - viewshift_SEP 0 (ghost_part sh (S n) g * ghost_ref (S z) g). - { go_lower. - unfold ghost_part, ghost_ref; rewrite !ghost_part_ref_join. - eapply derives_trans, bupd_fupd. - apply ref_add with (b := 1%nat); try (hnf; lia). } + viewshift_SEP 0 (ghost_part sh (S n) g ∗ ghost_ref (S z) g). + { go_lowerx. + iIntros "((part & ref) & _)". + iMod (own_update_2 with "ref part") as "($ & $)"; last done. + apply frac_auth_update, nat_local_update; lia. } Intros; forward_call release_simple (sh, h, cptr_lock_inv g (gv _c)). { lock_props. unfold cptr_lock_inv; Exists (S z). @@ -217,11 +207,19 @@ Proof. forward. forward_call (sh1, sh, h, g, O, gv). forward_call release_self (tsh, ht, thread_lock_R sh1 sh g (gv _c) h). - { unfold thread_lock_inv, selflock, thread_lock_R; cancel. } + { lock_props. + unfold thread_lock_inv, selflock, thread_lock_R; cancel. } forward. Qed. +Local Open Scope Z. + Definition N := 5. +Definition N_frac := (/ pos_to_Qp (Z.to_pos (N + 1)))%Qp. + +Global Instance namespace_inhabitant : Inhabitant namespace := nroot. + +Opaque Qp.div Qp.mul. Lemma body_main: semax_body Vprog Gprog f_main main_spec. Proof. @@ -233,143 +231,126 @@ Proof. (* need to split off shares for the locks and ghost here *) destruct split_Ews as (sh1 & sh2 & ? & ? & Hsh). destruct (split_shares (Z.to_nat N) Ews) as (sh0 & shs & ? & ? & ? & Hshs); auto. - destruct (split_shares (Z.to_nat N) Tsh) as (gsh0 & gshs & ? & ? & ? & Hgshs); auto. - rewrite Z2Nat.id in * by (unfold N; computable). + rewrite -> Z2Nat.id in * by (unfold N; lia). assert_PROP (field_compatible (tarray (tptr t_lock) N) [] v_thread_lock) by entailer!. assert (N <= Int.max_signed) by computable. - forward_for_simple_bound N (EX i : Z, EX sh : share, EX gsh : share, EX ll : list lock_handle, + forward_for_simple_bound N (∃ i : Z, ∃ sh : share, ∃ ll : list lock_handle, PROP (sepalg_list.list_join sh0 (sublist i N shs) sh; - sepalg_list.list_join gsh0 (sublist i N gshs) gsh; Zlength ll = i; Forall isptr (map ptr_of ll)) LOCAL (lvar _thread_lock (tarray (tptr t_lock) N) v_thread_lock; gvars gv) SEP (library.mem_mgr gv; field_at sh t_counter (DOT _lock) (ptr_of h) (gv _c); - spacer Ews 4 8 (gv _c); ctr_handle gsh h g (gv _c) O; - iter_sepcon (fun j => lock_inv gsh1 (Znth j ll) - (thread_lock_inv (Znth j shs) gsh2 (Znth j gshs) g (gv _c) h (Znth j ll))) - (upto (Z.to_nat i)); + spacer Ews 4 8 (gv _c); ctr_handle (pos_to_Qp (Z.to_pos (N - i + 1)) * N_frac)%Qp h g (gv _c) O; + [∗ list] j ∈ seq 0 (Z.to_nat i), lock_inv (1/2) (Znth (Z.of_nat j) ll) + (thread_lock_inv (Znth (Z.of_nat j) shs) (1/2) N_frac g (gv _c) h (Znth (Z.of_nat j) ll)); data_at Tsh (tarray (tptr t_lock) N) (map ptr_of ll ++ repeat Vundef (Z.to_nat (N - i))) v_thread_lock; has_ext tt))%assert. - { Exists Ews Tsh (@nil lock_handle). - rewrite !sublist_same by auto; entailer!. - rewrite data_at__eq; apply derives_refl. } + { Exists Ews (@nil lock_handle). + rewrite -> !sublist_same by auto; rewrite Qp.mul_inv_r; entailer!. } { (* first loop *) - forward_call (gv, fun ht => thread_lock_inv (Znth i shs) gsh2 (Znth i gshs) g (gv _c) h ht). + forward_call (gv, fun ht => thread_lock_inv (Znth i shs) (1/2) N_frac g (gv _c) h ht). Intros ht. forward. assert_PROP (0 <= i < Zlength (map ptr_of ll ++ repeat Vundef (Z.to_nat (N - i)))) as Hi. - { entailer!. rewrite Zlength_app, Zlength_map, Zlength_repeat, Zplus_minus by lia; auto. } + { entailer!. rewrite -> Zlength_app, Zlength_map, Zlength_repeat, Zplus_minus by lia; auto. } forward. - { rewrite upd_Znth_same by auto; entailer!. } - rewrite upd_Znth_same by auto. + { rewrite -> upd_Znth_same by auto; entailer!. } + rewrite -> upd_Znth_same by auto. assert (readable_share (Znth (Zlength ll) shs)) as Hshi by (apply Forall_Znth; auto; lia). - rewrite sublist_next in H10, H11 by lia. - inv H10; inv H11. - destruct (sepalg_list.list_join_assoc1 (sepalg.join_comm H17) H19) as (sh' & ? & Hsh'). - destruct (sepalg_list.list_join_assoc1 (sepalg.join_comm H15) H18) as (gsh' & ? & Hgsh'). - assert (Znth (Zlength ll) gshs <> Share.bot). - { intro X; contradiction bot_unreadable. - rewrite <- X; apply Forall_Znth; auto; lia. } - assert (gsh' <> Share.bot). - { intro X; contradiction bot_unreadable. - rewrite <- X; eapply readable_share_list_join; eauto. } + rewrite -> sublist_next in H7 by lia; inv H7. + destruct (sepalg_list.list_join_assoc1 (sepalg.join_comm H13) H15) as (sh' & ? & Hsh'). sep_apply lock_inv_isptr; Intros. - forward_spawn _thread_func (ptr_of ht) (Znth (Zlength ll) shs, gsh2, ht, Znth (Zlength ll) gshs, h, g, gv). - { erewrite <- lock_inv_share_join; try apply gsh1_gsh2_join; auto. + forward_spawn _thread_func (ptr_of ht) (Znth (Zlength ll) shs, (1/2)%Qp, ht, N_frac, h, g, gv). + { rewrite -{1}Qp.half_half -frac_op -lock_inv_share_join. erewrite <- field_at_share_join; try apply Hsh'. - change O with (O + O)%nat. - erewrite <- ctr_handle_share_join; try apply Hgsh'; auto; simpl. - entailer!. } + replace (pos_to_Qp (Z.to_pos _)) with (1 + pos_to_Qp (Z.to_pos (N - Zlength ll)))%Qp. + rewrite Qp.mul_add_distr_r Qp.mul_1_l -frac_op. + rewrite -(ctr_handle_share_join _ _ _ _ _ O O). + entailer!. + { rewrite -> (Z2Pos.inj_add _ 1) by lia. + rewrite !pos_to_Qp_add; f_equal; lia. } } { simpl; auto. } - Exists sh' gsh' (ll ++ [ht]); entailer!. - { split; [autorewrite with sublist; auto | rewrite map_app, Forall_app; repeat constructor; auto]. } - apply sepcon_derives. - - rewrite Z2Nat.inj_add, upto_app by lia. - rewrite iter_sepcon_app; simpl. - rewrite Z2Nat.id, Z.add_0_r, app_Znth2, Zminus_diag, Znth_0_cons by (tauto || lia); cancel. - rewrite Zlength_correct, Nat2Z.id; apply iter_sepcon_derives; intros ??%In_upto. - rewrite <- Zlength_correct in *; autorewrite with sublist; auto. - - rewrite upd_complete_gen' by tauto; autorewrite with sublist; apply derives_refl. } - rewrite !sublist_nil, Zminus_diag; Intros shx gshx ll. - inv H9; inv H10. - forward_for_simple_bound N (EX i : Z, EX sh : share, EX gsh : share, - PROP (sepalg_list.list_join shx (sublist 0 i shs) sh; - sepalg_list.list_join gshx (sublist 0 i gshs) gsh) + Exists sh' (ll ++ [ht]); entailer!. + { split; [autorewrite with sublist; auto | rewrite map_app Forall_app; repeat constructor; auto]. } + rewrite !sep_assoc; apply bi.sep_mono. + - unfold ctr_handle. + replace (Z.to_pos (N - (Zlength ll + 1) + 1)) with (Z.to_pos (N - Zlength ll)) by lia; cancel. + rewrite -> Z2Nat.inj_add by lia. rewrite Nat.add_comm seq_S big_sepL_app /=. + rewrite -> Z2Nat.id, app_Znth2, Zminus_diag, Znth_0_cons by (tauto || lia); cancel. + rewrite Zlength_correct Nat2Z.id; apply big_sepL_mono; intros ?? (-> & ?)%lookup_seq. + assert (Z.of_nat k < Zlength ll) by (rewrite Zlength_correct; apply inj_lt; auto). + rewrite app_Znth1 //. + - rewrite -> upd_complete_gen' by tauto; autorewrite with sublist; apply derives_refl. } + rewrite !sublist_nil Zminus_diag; Intros shx ll. + inv H6. + forward_for_simple_bound N (∃ i : Z, ∃ sh : share, + PROP (sepalg_list.list_join shx (sublist 0 i shs) sh) LOCAL (lvar _thread_lock (tarray (tptr t_lock) N) v_thread_lock; gvars gv) SEP (library.mem_mgr gv; field_at sh t_counter (DOT _lock) (ptr_of h) (gv _c); - spacer Ews 4 8 (gv _c); ctr_handle gsh h g (gv _c) (Z.to_nat i); - iter_sepcon (fun j => lock_inv gsh1 (Znth j ll) - (thread_lock_inv (Znth j shs) gsh2 (Znth j gshs) g (gv _c) h (Znth j ll))) - (sublist i N (upto (Z.to_nat N))); + spacer Ews 4 8 (gv _c); ctr_handle (pos_to_Qp (Z.to_pos (i + 1)) * N_frac)%Qp h g (gv _c) (Z.to_nat i); + [∗ list] j ∈ seq (Z.to_nat i) (Z.to_nat N - Z.to_nat i), lock_inv (1/2) (Znth (Z.of_nat j) ll) + (thread_lock_inv (Znth j shs) (1/2) N_frac g (gv _c) h (Znth j ll)); data_at Tsh (tarray (tptr t_lock) N) (map ptr_of ll) v_thread_lock; has_ext tt))%assert. - { rewrite !sublist_nil, sublist_same, app_nil_r by (auto; lia). - Exists shx gshx; entailer!. - { split; constructor. } + { rewrite -> !sublist_nil, app_nil_r by (auto; lia). + Exists shx; entailer!. + { constructor. } apply derives_refl. } { (* second loop *) forward. { entailer!. apply isptr_is_pointer_or_null, Forall_Znth; auto. rewrite Zlength_map; simpl in *; replace (Zlength ll) with N; auto. } Opaque N. - rewrite sublist_next; auto; simpl. - rewrite Znth_upto by auto. - forward_call (gsh1, Znth i ll, thread_lock_inv (Znth i shs) gsh2 (Znth i gshs) g (gv _c) h (Znth i ll)). - { rewrite Znth_map by (simpl in *; lia); entailer!. } + destruct (Z.to_nat N - Z.to_nat i)%nat eqn: Hsub; [lia|]. + rewrite -cons_seq /= Z2Nat.id; last lia. + forward_call ((1/2)%Qp, Znth i ll, thread_lock_inv (Znth i shs) (1/2) N_frac g (gv _c) h (Znth i ll)). + { rewrite -> Znth_map by (simpl in *; lia); entailer!. } { cancel. } unfold thread_lock_inv at 2; unfold thread_lock_R, selflock; Intros. forward. unfold thread_lock_inv. - forward_call freelock_self (gsh1, gsh2, Znth i ll, thread_lock_R (Znth i shs) (Znth i gshs) g (gv _c) h). - { rewrite Znth_map by (simpl in *; lia); entailer!. } + forward_call freelock_self ((1/2)%Qp, (1/2)%Qp, Znth i ll, thread_lock_R (Znth i shs) N_frac g (gv _c) h). + { rewrite -> Znth_map by (simpl in *; lia); entailer!. } { unfold selflock; cancel. } + { apply Qp.half_half. } erewrite <- sublist_same with (al := shs) in Hshs by eauto. - erewrite <- sublist_same with (al := gshs) in Hgshs by eauto. - rewrite sublist_split with (mid := i) in Hshs, Hgshs by lia. - rewrite sublist_next with (i := i) in Hshs by lia. - rewrite sublist_next with (i := i) in Hgshs by lia. - rewrite app_cons_assoc in Hshs, Hgshs. + rewrite -> sublist_split with (mid := i) in Hshs by lia. + rewrite -> sublist_next with (i := i) in Hshs by lia. + rewrite app_cons_assoc in Hshs. apply sepalg_list.list_join_unapp in Hshs as (sh' & Hshs1 & ?). - apply sepalg_list.list_join_unapp in Hgshs as (gsh' & Hgshs1 & ?). apply sepalg_list.list_join_unapp in Hshs1 as (? & J & J1). - apply sepalg_list.list_join_unapp in Hgshs1 as (? & Jg & Jg1). - apply list_join_eq with (c := sh) in J; auto; subst. - apply list_join_eq with (c := gsh) in Jg; auto; subst. - rewrite <- sepalg_list.list_join_1 in J1, Jg1. - rewrite !(sublist_split 0 i (i + 1)), !sublist_len_1 by lia. - Exists sh' gsh'; entailer!. - { split; eapply sepalg_list.list_join_app; eauto; econstructor; eauto; constructor. } + apply sepalg_list.list_join_eq with (c := sh) in J; auto; subst. + rewrite <- sepalg_list.list_join_1 in J1. + rewrite -> !(sublist_split 0 i (i + 1)), !sublist_len_1 by lia. + Exists sh'; entailer!. + { eapply sepalg_list.list_join_app; eauto; econstructor; eauto; constructor. } unfold thread_lock_R. - sep_eapply field_at_share_join; [apply sepalg.join_comm; eauto|]. - sep_eapply ctr_handle_share_join; try (apply sepalg.join_comm; eauto). - { intros X; contradiction unreadable_bot; rewrite <- X; apply Forall_Znth; auto; lia. } - { intros X; contradiction unreadable_bot; rewrite <- X. - eapply readable_share_list_join; eauto. } - rewrite Z2Nat.inj_add, plus_comm by lia; simpl; unfold thread_lock_inv, thread_lock_R, selflock; cancel. - { rewrite Zlength_upto; lia. } } - Intros sh' gsh'. - eapply list_join_eq in Hshs; [|erewrite <- (sublist_same 0 N shs) by auto; eauto]. - eapply list_join_eq in Hgshs; [|erewrite <- (sublist_same 0 N gshs) by auto; eauto]. + rewrite -(field_at_share_join _ _ sh') //. + replace (pos_to_Qp (Z.to_pos (i + 1 + 1))) with (pos_to_Qp (Z.to_pos (i + 1)) + 1)%Qp. + rewrite Qp.mul_add_distr_r Qp.mul_1_l -frac_op Z2Nat.inj_add; [|lia..]. + rewrite -ctr_handle_share_join Nat.add_comm /=. + replace (Z.to_nat N - S (Z.to_nat i))%nat with n by lia. + cancel; apply derives_refl. + { rewrite pos_to_Qp_add; f_equal; lia. } } + Intros sh'. + eapply sepalg_list.list_join_eq in Hshs; [|erewrite <- (sublist_same 0 N shs) by auto; eauto]. subst. + rewrite Nat.sub_diag Qp.mul_inv_r. forward_call (h, g, Z.to_nat N, gv). forward. - rewrite Z2Nat.id by auto. + rewrite -> Z2Nat.id by auto. (* We've proved that t is N! *) forward. { repeat sep_apply data_at_data_at_; cancel. } Qed. -Definition extlink := ext_link_prog prog. -Definition Espec := add_funspecs (Concurrent_Espec unit _ extlink) extlink Gprog. -#[export] Existing Instance Espec. - Lemma prog_correct: semax_prog prog tt Vprog Gprog. Proof. prove_semax_prog. semax_func_cons_ext. { simpl. - Intros h. - unfold PROPx, LOCALx, SEPx, local, lift1; simpl; unfold liftx; simpl; unfold lift; Intros. + destruct x. + unfold PROPx, LOCALx, SEPx, local, lift1; monPred.unseal; simpl; unfold_lift; Intros h. destruct ret; unfold eval_id in H0; simpl in H0; subst; simpl; [|contradiction]. - saturate_local; apply prop_right; auto. } + saturate_local; apply bi.pure_intro; auto. } do 4 semax_func_cons_ext. semax_func_cons body_init_ctr. semax_func_cons body_dest_ctr. @@ -377,3 +358,5 @@ semax_func_cons body_incr. semax_func_cons body_thread_func. semax_func_cons body_main. Qed. + +End proofs.