Merge branch 'offset_lifting' into 'master'

Lifting lemmas for working with arrays

See merge request iris/iris!267

theories/heap_lang/lifting.v

@@ -193,6 +193,10 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
 Implicit Types σ : state.
+Implicit Types v : val.
+Implicit Types vs : list val.
+Implicit Types l : loc.
+Implicit Types sz off : nat.
 
 (** Fork: Not using Texan triples to avoid some unnecessary [True] *)
 Lemma wp_fork s E e Φ :
@@ -263,6 +267,25 @@ Proof.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
+Lemma update_array l vs off v :
+  vs !! off = Some v →
+  (l ↦∗ vs -∗ ((l +ₗ off) ↦ v ∗ ∀ v', (l +ₗ off) ↦ v' -∗ l ↦∗ <[off:=v']>vs))%I.
+Proof.
+  iIntros (Hlookup) "Hl".
+  rewrite -[X in (l ↦∗ X)%I](take_drop_middle _ off v); last done.
+  iDestruct (array_app with "Hl") as "[Hl1 Hl]".
+  iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
+  assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
+  rewrite take_length min_l; last by lia. iFrame "Hl2".
+  iIntros (w) "Hl2".
+  clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
+  { apply list_lookup_insert. lia. }
+  rewrite -[in (l ↦∗ <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
+  iApply array_app. rewrite take_insert; last by lia. iFrame.
+  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
+  rewrite drop_insert; last by lia. done.
+Qed.
+
 (** Heap *)
 Lemma wp_allocN s E v n :
   0 < n →
@@ -420,7 +443,7 @@ Qed.
 Lemma wp_new_proph s E :
   {{{ True }}}
     NewProph @ s; E
-  {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
+  {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
@@ -468,11 +491,11 @@ Proof.
       apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
 Qed.
 
-Lemma wp_resolve s E e Φ p v vs :
+Lemma wp_resolve s E e Φ p v pvs :
   Atomic StronglyAtomic e →
   to_val e = None →
-  proph p vs -∗
-  WP e @ s; E {{ r, ∀ vs', ⌜vs = (r, v)::vs'⌝ -∗ proph p vs' -∗ Φ r }} -∗
+  proph p pvs -∗
+  WP e @ s; E {{ r, ∀ pvs', ⌜pvs = (r, v)::pvs'⌝ -∗ proph p pvs' -∗ Φ r }} -∗
   WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
 Proof.
   (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
@@ -496,14 +519,125 @@ Proof.
     iMod "HΦ". iModIntro. by iApply "HΦ".
 Qed.
 
-Lemma wp_resolve_proph s E p vs v :
-  {{{ proph p vs }}}
+Lemma wp_resolve_proph s E p pvs v :
+  {{{ proph p pvs }}}
     ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
-  {{{ vs', RET (LitV LitUnit); ⌜vs = (LitV LitUnit, v)::vs'⌝ ∗ proph p vs' }}}.
+  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
 Proof.
   iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
   iApply wp_pure_step_later=> //=. iApply wp_value.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
+Lemma wp_allocN_vec s E v n :
+  0 < n →
+  {{{ True }}}
+    AllocN #n v @ s ; E
+  {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
+Proof.
+  iIntros (Hzs Φ) "_ HΦ". iApply wp_allocN; [ lia | done | .. ]. iNext.
+  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
+Qed.
+
+Lemma wp_load_offset s E l off vs v :
+  vs !! off = Some v →
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗ vs }}}.
+Proof.
+  iIntros (Hlookup Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HΦ".
+  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
+  iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}.
+Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
+
+Lemma wp_store_offset s E l off vs v :
+  is_Some (vs !! off) →
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
+Proof.
+  iIntros ([w Hlookup] Φ) ">Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_store with "Hl1"). iNext. iIntros "Hl1".
+  iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
+Proof.
+  setoid_rewrite vec_to_list_insert. apply wp_store_offset.
+  eexists. by apply vlookup_lookup.
+Qed.
+
+Lemma wp_cas_suc_offset s E l off vs v1 v2 :
+  vs !! off = Some v1 →
+  vals_cas_compare_safe v1 v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CAS #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET #true; l ↦∗ <[off:=v2]> vs }}}.
+Proof.
+  iIntros (Hlookup Hcmp Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_cas_suc with "Hl1"). { left. by destruct Hcmp. }
+  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+  vs !!! off = v1 →
+  vals_cas_compare_safe v1 v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CAS #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET #true; l ↦∗ vinsert off v2 vs }}}.
+Proof.
+  intros. setoid_rewrite vec_to_list_insert. apply wp_cas_suc_offset=> //.
+  by apply vlookup_lookup.
+Qed.
+
+Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 :
+  vs !! off = Some v0 →
+  v0 ≠ v1 →
+  vals_cas_compare_safe v0 v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CAS #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET #false; l ↦∗ vs }}}.
+Proof.
+  iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_cas_fail with "Hl1"); first done.
+  { destruct Hcmp; by [ left | right ]. }
+  iIntros "!> Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
+  rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_cas_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+  vs !!! off ≠ v1 →
+  vals_cas_compare_safe (vs !!! off) v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CAS #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET #false; l ↦∗ vs }}}.
+Proof. intros. eapply wp_cas_fail_offset=> //. by apply vlookup_lookup. Qed.
+
+Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
+  vs !! off = Some #i1 →
+  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
+  {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
+Proof.
+  iIntros (Hlookup Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_faa with "Hl1").
+  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
+  vs !!! off = #i1 →
+  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
+  {{{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }}}.
+Proof.
+  intros. setoid_rewrite vec_to_list_insert. apply wp_faa_offset=> //.
+  by apply vlookup_lookup.
+Qed.
+
 End lifting.

theories/heap_lang/locations.v

@@ -18,7 +18,8 @@ Next Obligation. done. Qed.
 Definition loc_add (l : loc) (off : Z) : loc :=
   {| loc_car := loc_car l + off|}.
 
-Notation "l +ₗ off" := (loc_add l off) (at level 50, left associativity).
+Notation "l +ₗ off" :=
+  (loc_add l off) (at level 50, left associativity) : stdpp_scope.
 
 Lemma loc_add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j).
 Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.

theories/heap_lang/notation.v

@@ -32,7 +32,7 @@ Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUni
 
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)