Commit fd74b574 authored by Ralf Jung's avatar Ralf Jung

move array stuff to its own file

parent 625011cf
......@@ -100,6 +100,7 @@ theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/array.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Import tactics notation.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) v)%I.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
Section lifting.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types l : loc.
Implicit Types sz off : nat.
Lemma array_nil l : l ↦∗ [] emp.
Proof. by rewrite /array. Qed.
Lemma array_singleton l v : l ↦∗ [v] l v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l vs ws :
l ↦∗ (vs ++ ws) l ↦∗ vs (l + length vs) ↦∗ ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
by setoid_rewrite loc_add_assoc.
Qed.
Lemma array_cons l v vs : l ↦∗ (v :: vs) l v (l + 1) ↦∗ vs.
Proof.
rewrite /array big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
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.
(** Allocation *)
Lemma mapsto_seq_array l v n :
([ list] i seq 0 n, (l + (i : nat)) v) -
l ↦∗ replicate n v.
Proof.
rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
{ done. }
iIntros "[$ Hl]". rewrite -fmap_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc. iApply "IH". done.
Qed.
Lemma wp_allocN s E v n :
0 < n
{{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
{{{ l, RET LitV (LitLoc l); l ↦∗ replicate (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_seq; [done..|]. iNext.
iIntros (l) "Hlm". iApply "HΦ".
iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
by iApply mapsto_seq_array.
Qed.
Lemma twp_allocN s E v n :
0 < n
[[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
[[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }]].
Proof.
iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
iIntros (l) "Hlm". iApply "HΦ".
iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
by iApply mapsto_seq_array.
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 twp_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 twp_allocN; [ lia | done | .. ].
iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
Qed.
(** Access to array elements *)
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_cmpxchg_suc_offset s E l off vs v' v1 v2 :
vs !! off = Some v'
v' = v1
vals_compare_safe v' v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
Proof.
iIntros (Hlookup ?? Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
vs !!! off = v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
Proof.
intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
by apply vlookup_lookup.
Qed.
Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
vs !! off = Some v0
v0 v1
vals_compare_safe v0 v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v0, #false); l ↦∗ vs }}}.
Proof.
iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_cmpxchg_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_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
vs !!! off v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
Proof. intros. eapply wp_cmpxchg_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.
......@@ -31,11 +31,6 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) v)%I.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
......@@ -204,9 +199,7 @@ 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 Φ :
......@@ -225,43 +218,10 @@ Proof.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
Lemma array_nil l : l ↦∗ [] emp.
Proof. by rewrite /array. Qed.
Lemma array_singleton l v : l ↦∗ [v] l v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l vs ws :
l ↦∗ (vs ++ ws) l ↦∗ vs (l + length vs) ↦∗ ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
by setoid_rewrite loc_add_assoc.
Qed.
Lemma array_cons l v vs : l ↦∗ (v :: vs) l v (l + 1) ↦∗ vs.
Proof.
rewrite /array big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
Qed.
Lemma heap_array_to_array l vs :
([ map] l' v heap_array l vs, l' v) - l ↦∗ vs.
Proof.
iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
{ by rewrite /array. }
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite array_cons.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
by iApply "IH".
Qed.
(** Heap *)
(** The "proper" [allocN] are derived in [array]. *)
Lemma heap_array_to_seq_meta l vs n :
Lemma heap_array_to_seq_meta l vs (n : nat) :
length vs = n
([ map] l' _ heap_array l vs, meta_token l' ) -
[ list] i seq 0 n, meta_token (l + (i : nat)) .
......@@ -277,31 +237,27 @@ 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.
Lemma heap_array_to_seq_mapsto l v (n : nat) :
([ map] l' v heap_array l (replicate n v), l' v) -
[ list] i seq 0 n, (l + (i : nat)) v.
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.
iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
{ done. }
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite loc_add_0 -fmap_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
Qed.
(** Heap *)
Lemma wp_allocN s E v n :
Lemma wp_allocN_seq s E v n :
0 < n
{{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
{{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }}}.
{{{ l, RET LitV (LitLoc l); [ list] i seq 0 (Z.to_nat n),
(l + (i : nat)) v meta_token (l + (i : nat)) }}}.
Proof.
iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
......@@ -309,15 +265,16 @@ Proof.
iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
{ apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
- by iApply heap_array_to_array.
iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ".
iApply big_sepL_sep. iSplitL "Hl".
- by iApply heap_array_to_seq_mapsto.
- iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
Lemma twp_allocN s E v n :
Lemma twp_allocN_seq s E v n :
0 < n
[[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
[[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }]].
[[{ l, RET LitV (LitLoc l); [ list] i seq 0 (Z.to_nat n),
(l + (i : nat)) v meta_token (l + (i : nat)) }]].
Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
......@@ -325,24 +282,23 @@ Proof.
iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
{ apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
- by iApply heap_array_to_array.
iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ".
iApply big_sepL_sep. iSplitL "Hl".
- by iApply heap_array_to_seq_mapsto.
- iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v meta_token l }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
iIntros "!>" (l) "/= (? & ? & _)".
rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
iIntros (Φ) "_ HΦ". iApply wp_allocN_seq; auto with lia.
iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
Qed.
Lemma twp_alloc s E v :
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l v meta_token l }]].
Proof.
iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
iIntros (l) "/= (? & ? & _)".
rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; auto with lia.
iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
Qed.
Lemma wp_load s E l q v :
......@@ -569,117 +525,4 @@ Proof.
iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
(** Array lemmas *)
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_cmpxchg_suc_offset s E l off vs v' v1 v2 :
vs !! off = Some v'
v' = v1
vals_compare_safe v' v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
Proof.
iIntros (Hlookup ?? Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
vs !!! off = v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
Proof.
intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
by apply vlookup_lookup.
Qed.
Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
vs !! off = Some v0
v0 v1
vals_compare_safe v0 v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v0, #false); l ↦∗ vs }}}.
Proof.
iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_cmpxchg_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_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
vs !!! off v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
Proof. intros. eapply wp_cmpxchg_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.
......@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics lifting.
From iris.heap_lang Require Export tactics lifting array.
From iris.heap_lang Require Import notation.