Commit cec300fc authored by Amin Timany's avatar Amin Timany

Add arrays to heap_lang

parent 78ee4940
......@@ -91,6 +91,7 @@ theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/locations.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
......
......@@ -144,6 +144,16 @@ Section tests.
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
Lemma wp_alloc_array n : 0 < n
{{{ True }}}
AllocN #n #0
{{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}%I.
Proof.
iIntros (? ?) "!# _ HΦ".
wp_alloc l as "?"; first done.
by iApply "HΦ".
Qed.
End tests.
Section printing_tests.
......
......@@ -142,6 +142,22 @@ Section gen_heap.
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
Lemma gen_heap_alloc_gen σ σ' :
σ ## σ' gen_heap_ctx σ == gen_heap_ctx (σ σ') [ map] l v σ', l v.
Proof.
revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
iIntros (σ Hσdisj) "Hσ".
- by rewrite right_id big_opM_empty; iFrame.
- iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_r.
rewrite big_opM_insert //; iFrame.
assert (σ !! l = None).
{ eapply map_disjoint_Some_r; first by eauto.
rewrite lookup_insert //. }
rewrite -insert_union_r //.
iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
apply lookup_union_None; split; auto.
Qed.
Lemma gen_heap_dealloc σ l v :
gen_heap_ctx σ - l v == gen_heap_ctx (delete l σ).
Proof.
......
This diff is collapsed.
......@@ -53,7 +53,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
......@@ -67,7 +67,7 @@ Local Ltac solve_atomic :=
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
......@@ -184,24 +184,101 @@ Proof.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
Definition array (l : loc) (vs : list val) : iProp Σ :=
([ list] i v vs, loc_add l i v)%I.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
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 (loc_add 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] i v heap_array l vs, i v)%I - l ↦∗ vs.
Proof.
iIntros "Hvs".
iInduction vs as [|v vs] "IH" forall (l); simpl.
{ by rewrite big_opM_empty /array big_opL_nil. }
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;
apply loc_add_inj in Hjl; lia. }
rewrite array_cons.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
by iApply "IH".
Qed.
(** Heap *)
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) }}}.
Proof.
iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
{ symmetry.
apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; iSplit; auto.
iFrame. iApply "HΦ".
by iApply heap_array_to_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) }]].
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.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
{ symmetry.
apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; iSplit; auto.
iFrame; iSplit; auto. iApply "HΦ".
by iApply heap_array_to_array.
Qed.
Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
iIntros (Φ) "_ HΦ".
iApply wp_allocN; auto with lia.
iNext; iIntros (l) "H".
iApply "HΦ".
by rewrite array_singleton.
Qed.
Lemma twp_alloc s E v :
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l v }]].
Proof.
iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
iIntros (Φ) "_ HΦ".
iApply twp_allocN; auto with lia.
iIntros (l) "H".
iApply "HΦ".
by rewrite array_singleton.
Qed.
Lemma wp_load s E l q v :
......@@ -336,3 +413,6 @@ Proof.
Qed.
End lifting.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
From iris.algebra Require Import base.
From stdpp Require Import countable numbers gmap.
Record loc := { loc_car : Z }.
Instance loc_eq_decision : EqDecision loc.
Proof. solve_decision. Qed.
Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. 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).
Lemma loc_add_assoc l i j : l + i + j = l + (i + j).
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
Lemma loc_add_0 l : l + 0 = l.
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
Instance loc_add_inj l : Inj eq eq (loc_add l).
Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
Definition fresh_locs (g : gset loc) (n : Z) : loc :=
{| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z g |}.
Lemma fresh_locs_fresh g n i :
(0 i)%Z (i < n)%Z (fresh_locs g n) + i g.
Proof.
rewrite /fresh_locs /loc_add /=; intros Hil _ Hf; clear n.
cut ( x, x g
loc_car x < set_fold (λ k r, ((1 + loc_car k) `max` r)%Z) 1%Z g)%Z.
{ intros Hlem; apply Hlem in Hf; simpl in *; lia. }
clear Hf.
eapply (set_fold_ind_L
(λ z g, x : loc, x g (loc_car x < z)%Z));
try set_solver by eauto with lia.
Qed.
Global Opaque fresh_locs.
......@@ -10,9 +10,9 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
| Val v => is_closed_val v
| Var x => bool_decide (x X)
| Rec f x e => is_closed_expr (f :b: x :b: X) e
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
is_closed_expr X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2
| ResolveProph e1 e2 =>
is_closed_expr X e1 && is_closed_expr X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
......@@ -85,6 +85,41 @@ Lemma subst_rec_ne' f y e x v :
subst' x v (Rec f y e) = Rec f y (subst' x v e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma bin_op_eval_closed op v1 v2 v':
is_closed_val v1 is_closed_val v2 bin_op_eval op v1 v2 = Some v'
is_closed_val v'.
Proof.
rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int;
repeat case_match; by naive_solver.
Qed.
Lemma heap_closed_alloc σ l n w :
0 < n
is_closed_val w
map_Forall (λ _ v, is_closed_val v) (heap σ)
( i : Z, 0 i i < n heap σ !! (l + i) = None)
map_Forall (λ _ v, is_closed_val v)
(heap σ heap_array l (replicate (Z.to_nat n) w)).
Proof.
intros Hn Hw Hσ Hl.
eapply (map_Forall_ind
(λ k v, ((heap σ heap_array l (replicate (Z.to_nat n) w))
!! k = Some v))).
- apply map_Forall_empty.
- intros m i x Hi Hix Hkwm Hm.
apply map_Forall_insert_2; auto.
apply lookup_union_Some in Hix; last first.
{ symmetry; eapply heap_array_map_disjoint;
rewrite replicate_length Z2Nat.id; auto with lia. }
destruct Hix as [[j Hj]%elem_of_map_to_list%elem_of_list_lookup_1|
(?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup].
{ apply map_Forall_to_list in Hσ.
by eapply Forall_lookup in Hσ; eauto; simpl in *. }
rewrite !Z2Nat.id in Hlt; eauto with lia.
- apply map_Forall_to_list, Forall_forall.
intros [? ?]; apply elem_of_map_to_list.
Qed.
(* The stepping relation preserves closedness *)
Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
is_closed_expr [] e1
......@@ -99,7 +134,8 @@ Proof.
try apply map_Forall_insert_2; try by naive_solver.
- subst. repeat apply is_closed_subst'; naive_solver.
- unfold un_op_eval in *. repeat case_match; naive_solver.
- unfold bin_op_eval, bin_op_eval_bool in *. repeat case_match; naive_solver.
- eapply bin_op_eval_closed; eauto; naive_solver.
- by apply heap_closed_alloc.
Qed.
(* Parallel substitution with maps of values indexed by strings *)
......@@ -131,7 +167,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
| InjR e => InjR (subst_map vs e)
| Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
| Fork e => Fork (subst_map vs e)
| Alloc e => Alloc (subst_map vs e)
| AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
| Load e => Load (subst_map vs e)
| Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
| CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
......
......@@ -177,6 +177,35 @@ Implicit Types Δ : envs (uPredI (iResUR Σ)).
Implicit Types v : val.
Implicit Types z : Z.
Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
0 < n
MaybeIntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (AllocN #n v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? ? HΔ.
rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
Qed.
Lemma tac_twp_allocN Δ s E j K v n Φ :
0 < n
( l, Δ',
envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ
= Some Δ'
envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (AllocN #n v) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=> ? HΔ.
rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
rewrite left_id. apply forall_intro=> l.
destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
Qed.
Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
......@@ -404,18 +433,43 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
[pm_reflexivity || fail "wp_alloc:" H "not fresh"
|iDestructHyp Htmp as H; wp_finish] in
wp_pures;
(** The code first tries to use allocation lemma for a single reference,
ie, [tac_wp_alloc] (respectively, [tac_twp_alloc]).
If that fails, it tries to use the lemma [tac_wp_allocN]
(respectively, [tac_twp_allocN]) for allocating an array.
Notice that we could have used the array allocation lemma also for single
references. However, that would produce the resource l ↦∗ [v] instead of
l ↦ v for single references. These are logically equivalent assertions
but are not equal. *)
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
[iSolveTC
|finish ()]
let process_single _ :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
[iSolveTC
|finish ()]
in
let process_array _ :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
[idtac|iSolveTC
|finish ()]
in (process_single ()) || (process_array ())
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
finish ()
let process_single _ :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
finish ()
in
let process_array _ :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
finish ()
in (process_single ()) || (process_array ())
| _ => fail "wp_alloc: not a 'wp'"
end.
......
......@@ -22,7 +22,8 @@ Ltac reshape_expr e tac :=
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
| Alloc ?e => go (AllocCtx :: K) e
| AllocN ?e (Val ?v) => go (AllocNLCtx v :: K) e
| AllocN ?e1 ?e2 => go (AllocNRCtx e1 :: K) e2
| Load ?e => go (LoadCtx :: K) e
| Store ?e (Val ?v) => go (StoreLCtx v :: K) e
| Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
......
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