Commit ec399a74 authored by Robbert Krebbers's avatar Robbert Krebbers

Make distinction between malloced memory and local variables.

- Have a version of bind that allocates a local variable, and
  automatically frees it at the end.
- Only malloced memory can be freed manually.
parent 2224eaf2
......@@ -67,7 +67,7 @@ Section a_wp.
Definition flock_resources (γ : flock_name) (I : gmap prop_id lock_res) :=
([ map] i X I, flock_res amonadN γ i X)%I.
(** DF: The outer `WP` here is needed to be able to preform some reductions inside a heap_lang context.
(** DF: The outer `WP` here is needed to be able to perform some reductions inside a heap_lang context.
Without this, the `a_wp_awp` rule is not provable.
My intuitive explanation: we want to preform some reductions to `e` until it is actually a value that is a monadic computation.
......
......@@ -12,7 +12,7 @@ Definition a_alloc : val := λ: "x1" "x2",
let: "n" := Fst "vv" in
let: "v" := Snd "vv" in
assert: (#0 < "n");;
a_atomic_env (λ: <>, SOME (ref (SOME (lreplicate "n" "v")), #0)).
a_atomic_env (λ: <>, SOME (ref (SOME (#true, lreplicate "n" "v")), #0)).
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
Definition a_free_check : val :=
......@@ -32,7 +32,11 @@ Definition a_free : val := λ: "x",
let: "i" := Snd "li" in
match: !"l" with
NONE => assert: #false (* location already freed, double free *)
| SOME "ll" =>
| SOME "kll" =>
let: "k" := Fst "kll" in
let: "ll" := Snd "kll" in
(* Make sure its not a block scoped variable *)
assert: ("k" = #true);;
(* We need to make sure `i = 0` and that all `0 ... length of block`
are unlocked. *)
assert: ("i" = #0);;
......@@ -56,7 +60,7 @@ Definition a_store : val := λ: "x1" "x2",
mset_add ("l", "i") "env" ;;
match: !"l" with
NONE => assert: #false (* store after free *)
| SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
| SOME "kll" => "l" <- SOME (Fst "kll", linsert "i" "v" (Snd "kll")) ;; "v"
end
end
).
......@@ -73,7 +77,7 @@ Definition a_load : val := λ: "x",
assert: (mset_member ("l", "i") "env" = #false);;
match: !"l" with
NONE => assert: #false (* load after free *)
| SOME "ll" => llookup "i" "ll"
| SOME "kll" => llookup "i" (Snd "kll")
end
end
).
......@@ -94,6 +98,16 @@ Notation "e1 ;ᶜ e2" :=
(at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;ᶜ ']' '/' e2 ']'") : expr_scope.
Definition a_mut_bind : val := λ: "x" "f",
"v" ←ᶜ "x" ;
"l" ←ᶜ a_atomic_env (λ: <>, ref (SOME (#false, lreplicate #1 "v"))) ;;
"b" ←ᶜ "f" (SOME ("l", #0)) ;;
a_atomic_env (λ: <>, "l" <- NONE) ;;
a_ret "b".
Notation "x ←mutᶜ e1 ;ᶜ e2" :=
(a_mut_bind e1 (λ: x, e2))%E
(at level 100, e1 at next level, e2 at level 200, right associativity) : expr_scope.
Definition a_if : val := λ: "cnd" "e1" "e2",
(* sequenced binds needed here; there should be sequence point after the conditional *)
"c" ←ᶜ "cnd" ;
......@@ -208,7 +222,7 @@ Section proofs.
AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - n : nat,
v1 = #n n 0%nat
cl, block_info cl n - cl C replicate n v2 - Φ (cloc_to_val cl)) -
cl, block_info cl true n - cl C replicate n v2 - Φ (cloc_to_val cl)) -
AWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -237,7 +251,7 @@ Section proofs.
Lemma a_free_spec R Φ e :
AWP e @ R {{ v, cl ws, v = cloc_to_val cl
block_info cl (length ws) cl C ws Φ #() }} -
block_info cl true (length ws) cl C ws Φ #() }} -
AWP free(e) @ R {{ Φ }}.
Proof.
iIntros "H".
......@@ -254,8 +268,9 @@ Section proofs.
iMod (full_locking_heap_free_upd with "Hσ Hinfo Hcl")
as (ll Hoff Hl) "[Hl Hclose]".
wp_load. wp_pures. rewrite Hoff.
wp_apply wp_assert; wp_pures; iSplit; first done.
iNext; wp_pures. wp_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
wp_apply wp_assert; wp_pures; iSplit; first done. iNext.
wp_apply wp_assert; wp_pures; iSplit; first done. iNext.
wp_pures. wp_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
iAssert ( Ψ (n : nat), n length ws
(is_mset env X - Ψ #()) - WP a_free_check env #(cloc_base cl) #n {{ Ψ }})%I
with "[Hlocks]" as "Hcheck".
......@@ -300,11 +315,11 @@ Section proofs.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_pures.
wp_load; wp_match.
wp_load; wp_pures.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
iApply wp_fupd. wp_store.
......@@ -329,7 +344,7 @@ Section proofs.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
iMod (full_locking_heap_load_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
rewrite bool_decide_false //.
......@@ -384,6 +399,53 @@ Section proofs.
iApply (awp_wand with "H"); iIntros (v) "H !>". by awp_lam.
Qed.
(* Internal spec: breaks the abstraction/notation *)
Lemma a_mut_bind_spec' R Φ e (f: val) :
AWP e @ R {{ v, U ( cl,
cl C v -
AWP f (cloc_to_val cl) @ R {{ w, v', cl C v' Φ w }}) }} -
AWP a_mut_bind e f @ R {{ Φ }}.
Proof.
iIntros "H".
awp_apply (a_wp_awp with "H"); iIntros (ev) "H". awp_lam. awp_pures.
iApply a_seq_bind_spec'; iApply (awp_wand with "H"); iIntros (v) "H !>".
awp_pures. iApply awp_bind.
awp_apply awp_atomic_env; iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". wp_pures.
wp_apply (lreplicate_spec 1 with "[//]"); iIntros (ll Hll).
wp_alloc l as "Hl".
iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "(Hσ & Hinfo & Hl)"=> //=.
iDestruct "Hl" as "[Hl _]".
iIntros "!> !>". iSplitL "Hlocks Hσ".
{ iExists X, _. iFrame.
iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
exists cl; split; first done. by rewrite locked_locs_alloc_unlocked. }
iSpecialize ("H" with "Hl"). rewrite cloc_to_val_eq /=.
awp_pures. iApply awp_bind. awp_pures. iApply (awp_wand with "H").
iIntros (w). iDestruct 1 as (v') "[Hl H]". awp_pures. iApply awp_bind.
awp_apply awp_atomic_env; iIntros (env') "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X' σ' HX') "[Hlock Hσ]". wp_pures.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
iMod (full_locking_heap_free_upd _ _ [_] with "Hσ Hinfo [$Hl //]")
as (ll' _ _) "[Hll Hclose] /=".
wp_store. iIntros "!> !>". iSplitL "Hlock Hll Hclose".
{ iExists X', _. iFrame "Hlock". iSplit; last by iApply "Hclose".
iPureIntro; intros w' Hw'. destruct (HX' _ Hw') as (cl'&Hcl&Hin).
exists cl'; split; first done. rewrite locked_locs_delete. set_solver. }
awp_pures. iApply awp_ret. by iApply wp_value.
Qed.
Lemma a_mut_bind_spec R Φ x e1 e2 :
AWP e1 @ R {{ v, U ( cl,
cl C v -
AWP subst' x (cloc_to_val cl) e2 @ R {{ w, v', cl C v' Φ w }}) }} -
AWP x mut e1 ; e2 @ R {{ Φ }}.
Proof.
iIntros "H". awp_pures. iApply a_mut_bind_spec'.
iApply (awp_wand with "H"); iIntros (v) "H !>"; iIntros (cl) "Hcl".
awp_lam. by iApply "H".
Qed.
Lemma a_if_spec R Φ c e1 e2 :
AWP c @ R {{ v, (v = #true U (AWP e1 @ R {{ Φ }}))
(v = #false U (AWP e2 @ R {{ Φ }})) }} -
......
......@@ -84,7 +84,7 @@ Instance cloc_inhabited : Inhabited cloc | 0 :=
Definition locking_heapUR : ucmraT :=
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
Definition heap_block_infoUR : ucmraT :=
gmapUR loc (agreeR natC).
gmapUR loc (agreeR (prodC boolC natC)).
(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
......@@ -112,21 +112,23 @@ Section definitions.
fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ.
Inductive heap_block :=
| ActiveBlock : list (lvl * val) heap_block
| FreedBlock : nat heap_block.
Definition heap_block_length (b : heap_block) : nat :=
(* true = alloc, false = local *)
| ActiveBlock : bool list (lvl * val) heap_block
| FreedBlock : bool nat heap_block.
Definition heap_block_info (b : heap_block) : bool * nat :=
match b with
| ActiveBlock lvvs => length lvvs
| FreedBlock n => n
| ActiveBlock b lvvs => (b,length lvvs)
| FreedBlock b n => (b,n)
end.
Global Instance maybe_active_block : Maybe ActiveBlock := λ b,
match b with ActiveBlock lvvs => Some lvvs | _ => None end.
Global Instance maybe_active_block : Maybe2 ActiveBlock := λ b,
match b with ActiveBlock k lvvs => Some (k,lvvs) | _ => None end.
Definition to_heap_block_info (τ : gmap loc heap_block) : heap_block_infoUR :=
to_agree heap_block_length <$> τ.
to_agree heap_block_info <$> τ.
Definition heap_blocks_lookup (τ : gmap loc heap_block) (cl : cloc) : option (lvl * val) :=
b τ !! cloc_base cl;
lvvs maybe ActiveBlock b;
''(_, lvvs) maybe2 ActiveBlock b;
lvvs !! Z.to_nat (cloc_offset cl).
(* σ^{-1}(L) *)
......@@ -157,10 +159,10 @@ Section definitions.
own lheap_name ( (to_locking_heap σ))
own lheap_block_info_name ( (to_heap_block_info τ))
[ map] lb τ, match b with
| ActiveBlock lvvs => lv,
l SOMEV lv
| ActiveBlock k lvvs => lv,
l SOMEV (#k,lv)
is_list lv (snd <$> lvvs)
| FreedBlock _ => l NONEV
| FreedBlock _ _ => l NONEV
end)%I.
Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
......@@ -172,9 +174,9 @@ Section definitions.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
Definition block_info_def (cl : cloc) (n : nat) : iProp Σ :=
Definition block_info_def (cl : cloc) (k : bool) (n : nat) : iProp Σ :=
( cloc_offset cl = 0 n 0
own lheap_block_info_name ( {[ cloc_base cl := to_agree n ]}))%I.
own lheap_block_info_name ( {[ cloc_base cl := to_agree (k,n) ]}))%I.
Definition block_info_aux : seal (@block_info_def). by eexists. Qed.
Definition block_info := unseal block_info_aux.
Definition block_info_eq : @block_info = @block_info_def := seal_eq block_info_aux.
......@@ -305,9 +307,9 @@ Section properties.
cl C{q} (v :: vs) cl C{q} v (cl + 1) C{q} vs.
Proof. by rewrite (mapsto_list_app _ _ [_]) mapsto_list_singleton. Qed.
Global Instance block_info_persistent cl n : Persistent (block_info cl n).
Global Instance block_info_persistent cl k n : Persistent (block_info cl k n).
Proof. rewrite block_info_eq. apply _. Qed.
Global Instance block_info_timeless cl n : Timeless (block_info cl n).
Global Instance block_info_timeless cl k n : Timeless (block_info cl k n).
Proof. rewrite block_info_eq. apply _. Qed.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, SOMEV (#(cloc_base cl), #(cloc_offset cl))%V.
......@@ -372,9 +374,9 @@ Section properties.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
Qed.
Lemma block_info_singleton_included τ l n :
{[l := to_agree n]} to_heap_block_info τ
b, τ !! l = Some b heap_block_length b = n.
Lemma block_info_singleton_included τ l k n :
{[l := to_agree (k,n)]} to_heap_block_info τ
b, τ !! l = Some b heap_block_info b = (k,n).
Proof.
rewrite singleton_included=> -[mn].
rewrite /to_heap_block_info lookup_fmap fmap_Some_equiv=> -[[b [-> ->]]] /=.
......@@ -412,20 +414,20 @@ Section properties.
Qed.
Lemma full_locking_heap_load_upd cl lv q v σ :
full_locking_heap σ - cl C[lv]{q} v == ll vs,
full_locking_heap σ - cl C[lv]{q} v == (k : bool) ll vs,
is_list ll vs
vs !! Z.to_nat (cloc_offset cl) = Some v
cloc_base cl SOMEV ll
(cloc_base cl SOMEV ll - full_locking_heap σ cl C[lv]{q} v).
cloc_base cl SOMEV (#k,ll)
(cloc_base cl SOMEV (#k,ll) - full_locking_heap σ cl C[lv]{q} v).
Proof.
iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ). rewrite Hτ; last by eauto.
intros ([lvvs|?]&?&Hi)%bind_Some; simplify_eq/=.
intros ([k lvvs|?]&?&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_lookup_acc with "H") as "[H Hclose]"; first done.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists k, ll, lvvs.*2.
repeat iSplit; eauto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "H"; eauto.
......@@ -434,13 +436,13 @@ Section properties.
Qed.
Lemma full_locking_heap_store_upd cl lv v σ :
full_locking_heap σ - cl C[lv] v == ll vs,
full_locking_heap σ - cl C[lv] v == (k : bool) ll vs,
is_list ll vs
vs !! Z.to_nat (cloc_offset cl) = Some v
cloc_base cl SOMEV ll
cloc_base cl SOMEV (#k, ll)
( ll' lv' v',
is_list ll' (<[Z.to_nat (cloc_offset cl):=v']>vs) -
cloc_base cl SOMEV ll' ==
cloc_base cl SOMEV (#k, ll') ==
full_locking_heap (<[cl:=(lv',v')]>σ) cl C[lv'] v').
Proof.
iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
......@@ -448,9 +450,9 @@ Section properties.
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ). rewrite Hτ; last by eauto.
intros ([lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
iDestruct "Hcl" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
iDestruct "Hcl" as (ll) "[Hll %]". iModIntro. iExists k, ll, lvvs.*2.
repeat iSplit; eauto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll}" (ll' lv''' v' ?) "Hll".
......@@ -459,7 +461,8 @@ Section properties.
(exclusive_local_update _ (1%Qp, lv''', to_agree v'));
first by apply to_locking_heap_lookup_Some. }
iModIntro. iSplitL "Hσ Hτ H Hll"; last auto.
iExists (<[cloc_base cl:=ActiveBlock (<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
iExists (<[cloc_base cl:=
ActiveBlock k (<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
destruct cl as [l i]=> -[l' i'] ?; simpl in *.
......@@ -525,12 +528,12 @@ Section properties.
rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia.
Qed.
Lemma full_locking_heap_alloc_upd l ll vs σ :
Lemma full_locking_heap_alloc_upd l (k : bool) ll vs σ :
is_list ll vs vs []
full_locking_heap σ - l SOMEV ll ==
full_locking_heap σ - l SOMEV (#k,ll) ==
i, σ !! CLoc l i = None
full_locking_heap (alloc_heap σ l vs O)
block_info (CLoc l 0) (length vs) CLoc l 0 C vs.
block_info (CLoc l 0) k (length vs) CLoc l 0 C vs.
Proof.
intros Hll Hnil. iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ &H)". iIntros "Hll".
iAssert τ !! l = None %I as %Hτi.
......@@ -557,14 +560,14 @@ Section properties.
apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. }
iModIntro.
rewrite -to_locking_heap_insert /=. iFrame "Hσ Hl".
iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?".
iApply (big_sepL_impl with "Hls"); iIntros "!>" (k' w _) "?".
by rewrite Nat2Z.inj_succ Z.add_succ_r -Z.add_succ_l -Nat2Z.inj_succ. }
iMod (own_update with "Hτ") as "[Hτ Hinfo]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ l (to_agree (length vs)))=> //.
(alloc_singleton_local_update _ l (to_agree (k, length vs)))=> //.
by rewrite /to_heap_block_info lookup_fmap Hτi. }
iModIntro. iSplit; first done. iSplitL "Hσ H Hτ Hll".
{ iExists (<[l:=ActiveBlock ((ULvl,) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iExists (<[l:=ActiveBlock k ((ULvl,) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iPureIntro. split.
{ clear -Hnat. generalize 0. induction vs as [|v vs IH]=> j //=.
apply map_Forall_insert_2; simpl; eauto with lia. }
......@@ -626,13 +629,13 @@ Section properties.
by rewrite lookup_delete_ne; last (destruct cl; naive_solver).
Qed.
Lemma full_locking_heap_free_upd cl vs σ :
Lemma full_locking_heap_free_upd cl k vs σ :
full_locking_heap σ -
block_info cl (length vs) -
block_info cl k (length vs) -
cl C vs == ll,
cloc_offset cl = 0
is_list ll vs
cloc_base cl SOMEV ll
cloc_base cl SOMEV (#k, ll)
(cloc_base cl NONEV -
full_locking_heap (free_heap σ (cloc_base cl) (length vs))).
Proof.
......@@ -642,7 +645,7 @@ Section properties.
iDestruct (own_valid_2 with "Hτ Hinfo")
as %[(b&Hb&?)%block_info_singleton_included _]%auth_valid_discrete_2.
iDestruct (big_sepM_delete with "H") as "[Hb H]"; first done.
destruct b as [lvvs|n]; simpl in *; last first.
destruct b as [k' lvvs|k' n]; simplify_eq/=; last first.
{ destruct vs as [|v vs]; simplify_eq/=.
rewrite /mapsto_list mapsto_eq /mapsto_def; iDestruct "Hcl" as "[Hcl _]".
iDestruct "Hcl" as (lv' _ _) "Hcl". rewrite cloc_plus_0.
......@@ -673,7 +676,7 @@ Section properties.
apply auth_update_dealloc, delete_singleton_local_update, _. }
rewrite fmap_length.
iModIntro. iExists _. do 2 (iSplit; first done). iIntros "{$Hll} Hll".
iExists (<[cloc_base cl:=FreedBlock (length lvvs.*2)]> τ). iSplit.
iExists (<[cloc_base cl:=FreedBlock k (length lvvs.*2)]> τ). iSplit.
{ iPureIntro; split.
{ generalize (length lvvs); intros n.
induction n; simpl; eauto. by apply map_Forall_delete. }
......@@ -702,7 +705,7 @@ Section properties.
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ); rewrite Hτ; last by eauto.
intros ([lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
iDestruct "Hcl" as (ll) "[Hll %]".
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
......@@ -711,7 +714,8 @@ Section properties.
first by apply to_locking_heap_lookup_Some.
intros h Hh. fold_leibniz. intros ->. split; eauto. }
iModIntro. iSplitR "Hl"; last by eauto with iFrame.
iExists (<[cloc_base cl:=ActiveBlock (<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).
iExists (<[cloc_base cl:=
ActiveBlock k (<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
destruct cl as [l i]=> -[l' i'] ?; simpl in *.
......
From iris_c.vcgen Require Import proofmode.
Definition memcpy : val := λ: "arg",
"p" a_alloc 1 (a_ret (Fst "arg"));
"q" a_alloc 1 (a_ret (Fst (Snd "arg")));
"p" mut a_ret (Fst "arg");
"q" mut a_ret (Fst (Snd "arg"));
"n" ←ᶜ a_ret (Snd (Snd "arg"));
"pend" ←ᶜ ∗ᶜ (a_ret "p") +∗ᶜ (a_ret "n");
while (∗ᶜ (a_ret "p") <∗ᶜ a_ret "pend") {
......@@ -15,15 +15,15 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R :
lxs C xs - lys C ys -
AWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys lys C ys }}.
Proof.
iIntros (Hlen <-) "Hxs Hys". awp_lam. vcg.
iIntros (p) "_ _"; iIntros (q) "_ _ Hp Hq".
iApply (awp_wand _ (λ _, lxs C ys lys C ys)%I with "[-]");
[|iIntros (v) "H"; by vcg_continue].
iIntros (Hlen <-) "Hxs Hys". awp_lam. vcg. iIntros (p q) "Hp Hq".
iApply (awp_wand _ (λ _, p' q', p C p' q C q'
lxs C ys lys C ys)%I with "[-]"); last first.
{ iIntros (v). iDestruct 1 as (p' q') "[??]". by vcg_continue. }
iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);
destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto.
destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame.
vcg; iIntros "!> !> !> Hx Hy Hp Hq".
iSpecialize ("IH" $! (lxs + 1) (lys + 1) with "[//] [$] [$] [$] [$]").
rewrite !cloc_plus_plus -(Nat2Z.inj_add 1).
iApply (awp_wand with "IH").
iIntros (v) "[??]"; vcg_continue; eauto with iFrame.
iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; eauto with iFrame.
Qed.
......@@ -63,6 +63,7 @@ Inductive dexpr : Type :=
Inductive dcexpr : Type :=
| dCRet : dexpr dcexpr
| dCSeqBind : binder dcexpr dcexpr dcexpr
| dCMutBind : binder dcexpr dcexpr dcexpr
| dCAlloc : dcexpr dcexpr dcexpr
| dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr
......@@ -78,7 +79,7 @@ Inductive dcexpr : Type :=
Fixpoint dcexpr_size (de : dcexpr) : nat :=
match de with
| dCRet _ | dCUnknown _ => 1
| dCSeqBind _ de1 de2 | dCAlloc de1 de2 | dCStore de1 de2
| dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 |dCAlloc de1 de2 | dCStore de1 de2
| dCBinOp _ de1 de2 | dCPreBinOp _ de1 de2 | dCPar de1 de2
| dCWhile de1 de2 | dCWhileV de1 de2 => S (dcexpr_size de1 + dcexpr_size de2)
| dCLoad de | dCUnOp _ de | dCCall _ de => S (dcexpr_size de)
......@@ -142,7 +143,7 @@ Fixpoint dexpr_wf (E : known_locs) (de : dexpr) : bool :=
Fixpoint dcexpr_wf (E : known_locs) (de : dcexpr) : bool :=
match de with
| dCRet de => dexpr_wf E de
| dCSeqBind x de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
| dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
| dCLoad de1 | dCUnOp _ de1 | dCCall _ de1 => dcexpr_wf E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCWhile de1 de2 | dCWhileV de1 de2 | dCPar de1 de2 =>
......@@ -243,6 +244,7 @@ Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr :=
match de with
| dCRet de => a_ret (dexpr_interp E de)
| dCSeqBind x de1 de2 => x ←ᶜ (dcexpr_interp E de1) ; (dcexpr_interp E de2)
| dCMutBind x de1 de2 => x mut (dcexpr_interp E de1) ; (dcexpr_interp E de2)
| dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCLoad de1 => a_load (dcexpr_interp E de1)
| dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
......@@ -765,6 +767,10 @@ Fixpoint dce_subst (E: known_locs) (x: string) (dv : dval) (dce : dcexpr) : dcex
if decide (BNamed x = y)
then dCSeqBind y (dce_subst E x dv de1) de2
else dCSeqBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCMutBind y de1 de2 =>
if decide (BNamed x = y)
then dCMutBind y (dce_subst E x dv de1) de2
else dCMutBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCLoad de1 => dCLoad (dce_subst E x dv de1)
| dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
......@@ -798,8 +804,8 @@ Lemma dcexpr_interp_subst' E mx de dv :
dcexpr_interp E (dce_subst' E mx dv de) = subst' mx (dval_interp E dv) (dcexpr_interp E de).
Proof. destruct mx; simpl; auto using dcexpr_interp_subst. Qed.
Lemma de_subst_wf E s dv1 de2 :
dval_wf E dv1 dexpr_wf E de2 dexpr_wf E (de_subst E s dv1 de2).
Lemma de_subst_wf E x dv1 de2 :
dval_wf E dv1 dexpr_wf E de2 dexpr_wf E (de_subst E x dv1 de2).
Proof.
induction de2; intros; repeat (simplify_eq /= || case_decide); naive_solver.
Qed.
......@@ -814,3 +820,24 @@ Qed.
Lemma dce_subst_wf' E mx dv1 de2 :
dval_wf E dv1 dcexpr_wf E de2 dcexpr_wf E (dce_subst' E mx dv1 de2).
Proof. destruct mx; simpl; auto using dce_subst_wf. Qed.
Lemma de_subst_mono E E' x dv1 de2 :
dval_wf E dv1 dexpr_wf E de2 E `prefix_of` E'
de_subst E x dv1 de2 = de_subst E' x dv1 de2.
Proof.
induction de2; intros; repeat (simplify_eq /= || case_decide);
naive_solver eauto using dval_interp_mono with f_equal.
Qed.
Lemma dce_subst_mono E E' x dv1 de2 :
dval_wf E dv1 dcexpr_wf E de2 E `prefix_of` E'
dce_subst E x dv1 de2 = dce_subst E' x dv1 de2.
Proof.
induction de2; intros; repeat (simplify_eq /= || case_decide);
naive_solver eauto using de_subst_mono, dval_interp_mono with f_equal.
Qed.
Lemma dce_subst_mono' E E' mx dv1 de2 :
dval_wf E dv1 dcexpr_wf E de2 E `prefix_of` E'
dce_subst' E mx dv1 de2 = dce_subst' E' mx dv1 de2.
Proof. destruct mx; simpl; auto using dce_subst_mono. Qed.