mailbox fixes

PrincetonUniversity · Apr 3, 2024 · a66d8d0 · a66d8d0
1 parent 9b9f40f
commit a66d8d0
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/mailbox/verif_mailbox_read.v b/mailbox/verif_mailbox_read.v
@@ -49,7 +49,7 @@ Proof.
       (∃ v : Z, data_at sh tbuffer (vint v) (Znth b' bufs)) ∗ ghost_frag (vint b') g0).
   { unfold comm_loc; entailer!.
     rewrite <- bi.emp_sep at 1; apply bi.sep_mono; last cancel.
-    rewrite /AE_spec.
+    rewrite /AE_spec -sep_exist_r.
     iIntros "_" (???? (? & ? & Hincl)) "(>comm & (% & %) & buf & g0)".
     rewrite /comm_R.
     rewrite !rev_app_distr /= !last_two_reads_cons prev_taken_cons.
@@ -63,16 +63,16 @@ Proof.
     lapply (repable_buf b); auto; intro.
     rewrite Hlast.
     iIntros "!>". rewrite -bi.later_intro.
-    rewrite bi.sep_exist_r; iExists (-1).
-    rewrite bi.sep_exist_r; iExists (if eq_dec (vint b) Empty then b0 else b).
-    rewrite bi.sep_exist_r; iExists (if eq_dec (vint b) Empty then b2 else b0).
+    rewrite sep_exist_r; iExists (-1).
+    rewrite sep_exist_r; iExists (if eq_dec (vint b) Empty then b0 else b).
+    rewrite sep_exist_r; iExists (if eq_dec (vint b) Empty then b2 else b0).
     iStopProof; entailer!.
     { split; [rewrite Forall_app; repeat constructor; auto|].
       { exists b, (-1); split; [|split]; auto; lia. }
       split; last by if_tac.
       if_tac; last done.
       if_tac; auto. }
-    rewrite -!bi.sep_exist_l -!bi.sep_exist_r.
+    rewrite -!bi.sep_exist_l -!sep_exist_r.
     setoid_rewrite (if_true (Empty = Empty)); [|done..].
     Exists (if eq_dec (vint b) Empty then b0 else b); cancel.
     apply hist_incl_lt in Hincl; last done.

diff --git a/mailbox/verif_mailbox_write.v b/mailbox/verif_mailbox_write.v
@@ -461,7 +461,7 @@ Proof.
 intros. destruct al; reflexivity.
 Qed.
 
-Lemma upd_Znth_sep : forall {B : bi} i l (P : B), 0 <= i < Zlength l ->
+Lemma upd_Znth_sep : forall i l (P : mpred), 0 <= i < Zlength l ->
   P ∗ [∗] (upd_Znth i l emp) ⊣⊢ [∗] (upd_Znth i l P).
 Proof.
   intros; iSplit.
@@ -977,6 +977,7 @@ Proof.
       * iIntros "($ & ? & ? & H)".
         iSpecialize ("H" $! emp with "[]"); first done.
         rewrite list_insert_upd //.
+        rewrite -and_exist_l.
         replace (Zlength t') with (Zlength h') in *; by iApply (upd_write_shares with "[$]").
   - Intros t' h'.
     forward.