Commit 06df58a9 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre

Add lifting lemmas for operations under offset (list and vector versions).

parent 97232540
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment