Commit 55f1dc10 authored by Dan Frumin's avatar Dan Frumin

Assorted modifications to the stack example

- Still does not compile
parent 9dc07689
This diff is collapsed.
From iris_logrel.F_mu_ref_conc Require Import typing.
From iris_logrel.F_mu_ref_conc Require Import typing reflection.
(* stack τ = μ x. ref (Unit + τ * x) *)
Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
(* push st = λ x.
(λ stv. if (CAS(st, stv, ref (cons x stv)))
#()
(push st x)) (load st) *)
Definition FG_push (st : expr) : expr :=
Rec (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Definition FG_pushV (st : expr) : val :=
RecV (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Notation Conse h t := (Fold (Alloc (InjR (Pair h t)))).
Notation Nile := (Fold (Alloc (InjL Unit))).
Definition FG_push : val := rec: "push" "st" := λ: "x",
let: "stv" := !"st" in
if: (CAS "st" "stv" (Conse "x" "stv"))
then #()
else "push" "st" "x".
(* pop st = λ (),
(λ str.
......@@ -43,110 +24,43 @@ Definition FG_pushV (st : expr) : val :=
(pop st ()))
(load str))
(load st)*)
Definition FG_pop (st : expr) : expr :=
Rec (App (Rec
(App
(Rec
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Definition FG_popV (st : expr) : val :=
RecV
(App
(Rec
( App
(Rec
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Definition FG_pop : val := rec: "pop" "st" := λ: <>,
let: "stv" := !"st" in
let: "x" := !(Unfold "stv") in
case: "x" of
InjL => λ: <>, InjL #()
| InjR => λ: "x", let: "y" := Fst "x" in let: "ys" := Snd "x" in
if: (CAS "st" "stv" "ys")
then (InjR "y")
else "pop" "st" #()
end.
(* iter f = λ st.
case (load st) of
| nil => #()
| cons y ys => f y ;; iter f ys *)
Definition FG_iter (f : expr) : expr :=
Rec
(Case (Load (Unfold (Var 1)))
Unit
(App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Definition FG_iterV (f : expr) : val :=
RecV
(Case (Load (Unfold (Var 1)))
Unit
(App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
(* read_iter st := λf. iter f (load st) *)
Definition FG_read_iter (st : expr) : expr :=
Rec (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
(* stack_body st = push st, pop st, read_iter st *)
Definition FG_stack_body (st : expr) : expr :=
Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
Definition FG_iter : val := rec: "iter" "f" := λ: "st",
case: !(Unfold "st") of
InjL => λ: <>, #()
| InjR => λ: "x",
let: "y" := Fst "x" in
let: "ys" := Snd "x" in
"f" "y";; "iter" "f" "ys"
end.
Definition FG_read_iter : val := λ: "st" "f",
FG_iter "f" (!"st").
Definition FG_stack_body : val := λ: "st",
(FG_push "st", FG_pop "st", FG_read_iter "st").
(* stack = Λα. (λ (s : stack α). stack_body s) (ref (ref nil)) *)
Definition FG_stack : expr :=
TLam (App (Rec (FG_stack_body (Var 1)))
(Alloc (Fold (Alloc (InjL Unit))))).
Definition FG_stack : val :=
Λ: let: "st" := ref Nile in
FG_stack_body "st".
Section FG_stack.
(* Fine-grained push *)
Lemma FG_push_folding (st : expr) :
FG_push st =
Rec (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Proof. trivial. Qed.
Section FG_push_type.
(* The following assumption is simply ** WRONG ** *)
......@@ -156,166 +70,64 @@ Section FG_stack.
equality, we need this for compare-and-swap *)
Context (HEQTP : τ, EqType (FG_StackType τ)).
Lemma FG_push_type st Γ τ :
typed Γ st (Tref (FG_StackType τ))
typed Γ (FG_push st) (TArrow τ TUnit).
Lemma FG_push_type Γ τ :
typed Γ FG_push (TArrow (Tref (FG_StackType τ)) (TArrow τ TUnit)).
Proof.
intros H1. repeat (econstructor; eauto using HEQTP).
- eapply (context_weakening [_; _; _; _]); eauto.
- by asimpl.
- eapply (context_weakening [_; _]); eauto.
unfold FG_push. unlock.
repeat (econstructor; eauto with typeable).
asimpl. eauto with typeable.
Qed.
End FG_push_type.
Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st).
Proof. trivial. Qed.
Lemma FG_push_of_val st : of_val (FG_pushV st) = FG_push st.
Proof. trivial. Qed.
Global Opaque FG_pushV.
Lemma FG_push_closed (st : expr) :
( f, st.[f] = st) f, (FG_push st).[f] = FG_push st.
Proof. intros H f. asimpl. unfold FG_push. rewrite ?H; trivial. Qed.
End FG_push_type.
Lemma FG_push_subst (st : expr) f : (FG_push st).[f] = FG_push st.[f].
Proof. unfold FG_push. by asimpl. Qed.
Hint Resolve FG_push_type : typeable.
Global Opaque FG_push.
(* Fine-grained push *)
Lemma FG_pop_folding (st : expr) :
FG_pop st =
Rec (App (Rec
( App
(Rec
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Proof. trivial. Qed.
(* Fine-grained pop *)
Section FG_pop_type.
(* The following assumption is simply ** WRONG ** *)
(* We assume it though to just be able to prove that the
stack we are implementing is /type-sane/ so to speak! *)
Context (HEQTP : τ, EqType (FG_StackType τ)).
Lemma FG_pop_type st Γ τ :
typed Γ st (Tref (FG_StackType τ))
typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)).
Lemma FG_pop_type Γ τ :
typed Γ FG_pop (TArrow (Tref (FG_StackType τ)) (TArrow TUnit (TSum TUnit τ))).
Proof.
intros H1. repeat (econstructor; eauto using HEQTP).
- eapply (context_weakening [_; _; _; _; _; _; _]); eauto.
- asimpl; trivial.
- eapply (context_weakening [_; _]); eauto.
unfold FG_pop. unlock.
repeat (econstructor; eauto 10 with typeable).
cbn. asimpl. eauto 20 with typeable.
Qed.
End FG_pop_type.
Lemma FG_pop_to_val st : to_val (FG_pop st) = Some (FG_popV st).
Proof. trivial. Qed.
Lemma FG_pop_of_val st : of_val (FG_popV st) = FG_pop st.
Proof. trivial. Qed.
Global Opaque FG_popV.
Lemma FG_pop_closed (st : expr) :
( f, st.[f] = st) f, (FG_pop st).[f] = FG_pop st.
Proof. intros H f. asimpl. unfold FG_pop. rewrite ?H; trivial. Qed.
Lemma FG_pop_subst (st : expr) f : (FG_pop st).[f] = FG_pop st.[f].
Proof. unfold FG_pop. by asimpl. Qed.
End FG_pop_type.
Hint Resolve FG_pop_type : typeable.
Global Opaque FG_pop.
(* Fine-grained iter *)
Lemma FG_iter_folding (f : expr) :
FG_iter f =
Rec
(Case (Load (Unfold (Var 1)))
Unit
(App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Proof. trivial. Qed.
Lemma FG_iter_type f Γ τ :
typed Γ f (TArrow τ TUnit)
typed Γ (FG_iter f) (TArrow (FG_StackType τ) TUnit).
Lemma FG_iter_type Γ τ :
typed Γ FG_iter (TArrow (TArrow τ TUnit) (TArrow (FG_StackType τ) TUnit)).
Proof.
intros H1.
econstructor.
eapply (Case_typed _ _ _ _ TUnit);
[| repeat constructor
| repeat econstructor; eapply (context_weakening [_; _; _]); eauto].
econstructor.
replace (Tref (TSum TUnit (TProd τ (FG_StackType τ)))) with
((Tref (TSum TUnit (TProd τ.[ren(+1)] (TVar 0)))).[(FG_StackType τ)/])
by (by asimpl).
repeat econstructor.
unfold FG_iter. unlock.
repeat (econstructor; eauto 10 with typeable).
asimpl. eauto with typeable.
Qed.
Lemma FG_iter_to_val st : to_val (FG_iter st) = Some (FG_iterV st).
Proof. trivial. Qed.
Lemma FG_iter_of_val st : of_val (FG_iterV st) = FG_iter st.
Proof. trivial. Qed.
Global Opaque FG_popV.
Lemma FG_iter_closed (f : expr) :
( g, f.[g] = f) g, (FG_iter f).[g] = FG_iter f.
Proof. intros H g. asimpl. unfold FG_iter. rewrite ?H; trivial. Qed.
Lemma FG_iter_subst (f : expr) g : (FG_iter f).[g] = FG_iter f.[g].
Proof. unfold FG_iter. by asimpl. Qed.
Hint Resolve FG_iter_type : typeable.
Global Opaque FG_iter.
Lemma FG_read_iter_type st Γ τ :
typed Γ st (Tref (FG_StackType τ))
typed Γ (FG_read_iter st)
(TArrow (TArrow τ TUnit) TUnit).
Lemma FG_read_iter_type Γ τ :
typed Γ FG_read_iter
(TArrow (Tref (FG_StackType τ)) (TArrow (TArrow τ TUnit) TUnit)).
Proof.
intros H1; repeat econstructor.
- eapply FG_iter_type; by constructor.
- by eapply (context_weakening [_;_]).
unfold FG_read_iter. unlock.
eauto 20 with typeable.
Qed.
Transparent FG_iter.
Lemma FG_read_iter_closed (st : expr) :
( f, st.[f] = st)
f, (FG_read_iter st).[f] = FG_read_iter st.
Proof.
intros H1 f. unfold FG_read_iter, FG_iter. asimpl.
by rewrite ?H1.
Qed.
Lemma FG_read_iter_subst (st : expr) g :
(FG_read_iter st).[g] = FG_read_iter st.[g].
Proof. by unfold FG_read_iter; asimpl. Qed.
Hint Resolve FG_read_iter_type : typeable.
Global Opaque FG_iter.
......@@ -325,32 +137,20 @@ Section FG_stack.
stack we are implementing is /type-sane/ so to speak! *)
Context (HEQTP : τ, EqType (FG_StackType τ)).
Lemma FG_stack_body_type st Γ τ :
typed Γ st (Tref (FG_StackType τ))
typed Γ (FG_stack_body st)
Lemma FG_stack_body_type Γ τ :
typed Γ FG_stack_body (TArrow (Tref (FG_StackType τ))
(TProd
(TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ)))
(TArrow (TArrow τ TUnit) TUnit)
).
(TArrow (TArrow τ TUnit) TUnit))).
Proof.
intros H1.
repeat (econstructor; eauto using FG_push_type,
FG_pop_type, FG_read_iter_type).
unfold FG_stack_body. unlock.
eauto 20 with typeable.
Qed.
End FG_stack_body_type.
Hint Resolve FG_stack_body_type : typeable.
Opaque FG_read_iter.
Lemma FG_stack_body_closed (st : expr) :
( f, st.[f] = st)
f, (FG_stack_body st).[f] = FG_stack_body st.
Proof.
intros H1 f. unfold FG_stack_body. asimpl.
rewrite FG_push_closed; trivial.
rewrite FG_pop_closed; trivial.
by rewrite FG_read_iter_closed.
Qed.
Section FG_stack_type.
(* The following assumption is simply ** WRONG ** *)
(* We assume it though to just be able to prove that the
......@@ -368,18 +168,11 @@ Section FG_stack.
(TArrow (TArrow (TVar 0) TUnit) TUnit)
)).
Proof.
repeat econstructor.
- eapply FG_push_type; try constructor; simpl; eauto.
- eapply FG_pop_type; try constructor; simpl; eauto.
- eapply FG_read_iter_type; constructor; by simpl.
- asimpl. repeat constructor.
unfold FG_stack. unlock.
eauto 20 with typeable.
Qed.
End FG_stack_type.
Lemma FG_stack_closed f : FG_stack.[f] = FG_stack.
Proof.
unfold FG_stack.
asimpl; rewrite ?FG_push_subst ?FG_pop_subst.
asimpl. rewrite ?FG_read_iter_subst. by asimpl.
Qed.
Hint Resolve FG_stack_type : typeable.
End FG_stack.
From iris.algebra Require Import auth.
From iris.program_logic Require Import adequacy ectxi_language.
From iris_logrel.F_mu_ref_conc Require Import lang tactics soundness_binary notation.
From iris_logrel.F_mu_ref_conc Require Import lang tactics rel_tactics soundness_binary notation relational_properties hax.
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
From iris_logrel.F_mu_ref_conc.examples.stack Require Import
CG_stack FG_stack stack_rules.
......@@ -24,148 +24,184 @@ Section Stack_refinement.
iMod (Hcl with asn) as "_";
[iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.
Definition CG_snap_iterV (st l : expr) : val :=
RecV (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
Definition FG_read_iterV (st : expr) : val :=
RecV (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
Lemma FG_CG_iter_refinement ρ st st' (τi : D) l Δ {τP : ww, PersistentP (τi ww)} {SH : stackG Σ}:
spec_ctx ρ - inv stackN (sinv τi st st' l) -
TArrow (TArrow (TVar 0) TUnit) TUnit (τi::Δ) (FG_read_iterV (#st)%E, (CG_snap_iterV #st' #l)%E).
Lemma FG_CG_push_refinement ρ st st' (τi : D) (v v' : val) l {τP : ww, PersistentP (τi ww)} {SH : stackG Σ} Γ :
spec_ctx ρ - inv stackN (sinv τi st st' l) - τi (v,v') -
Γ ((FG_push $/ (LocV st)) v)%E log ((CG_locked_push $/ (LocV st') $/ (LocV l)) v')%E : TUnit.
Proof.
iIntros "#Hs #Hinv".
iAlways. iIntros ([f1 f2]) "#Hff /=".
iIntros (j K) "Hj /=".
iApply wp_rec; auto using to_of_val.
iNext. simpl. rewrite FG_iter_subst. simpl.
replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) by (rewrite FG_iter_of_val; done).
wp_bind (Load #st)%E.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hst"). iNext. iIntros "Hst".
tp_rec j; auto using to_of_val.
tp_normalise j.
rewrite CG_iter_subst CG_snap_subst.
Opaque coPset_difference.
asimpl.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done).
tp_bind j (App (CG_snap _ _) ())%E.
tp_apply j steps_CG_snap with "Hst' Hl" as "[Hst' Hl]".
tp_normalise j.
close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".
iLöb as "IH" forall (istk v) "HLK".
iApply wp_rec; auto. iNext. asimpl.
wp_bind (Unfold _). iApply wp_fold; auto. iNext.
iModIntro. wp_bind (Load _).
clear h.
iInv stackN as (istk2 v' h) "[Hoe [Hst' [Hst [HLK' Hl]]]]" "Hclose".
rewrite StackLink_unfold.
iDestruct "HLK" as (istkl w) "[% [Histk HLK]]". simplify_eq/=.
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histkl Hoe]".
iApply (wp_load with "Histkl"). iNext. iIntros "Histkl".
iSpecialize ("Hoe" with "Histkl").
close_sinv "Hclose" "[Hoe Hst Hst' HLK' Hl]".
iDestruct "HLK" as "[[% %]|HLK]"; subst.
+ (* the stack is empty *)
iApply wp_case_inl; auto.
iNext.
iApply fupd_wp.
rewrite CG_iter_of_val /=.
tp_apply j steps_CG_iter_end.
iIntros "#Hs #Hinv #Hvv'".
Transparent FG_push.
unfold CG_locked_push. unlock. simpl_subst/=.
rel_rec_r.
unfold FG_push. unlock. simpl_subst/=.
iLöb as "IH".
rel_rec_l.
rel_load_l under stackN as "Hst" "Hclose". simpl.
iDestruct "Hst" as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]".
iExists (FoldV #istk). iFrame.
iModIntro. iNext. iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
rel_rec_l.
rel_alloc_l as nstk "Hnstk". solve_to_val. (* TODO: rel_tactics *) simpl.
rel_cas_l under stackN as "Hst" "Hclose". simpl.
iDestruct "Hst" as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]".
iExists (FoldV #istk'). iFrame.
iModIntro.
iApply wp_value; auto.
iExists UnitV. iFrame. eauto.
+ iDestruct "HLK" as (y1 z1 y2 z2) "[% [% [Hy Hsl]]]". subst.
simpl.
iApply wp_case_inr; first by rewrite /= ?to_of_val /=.
iNext. asimpl.
wp_bind (Fst _). iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=).
iNext. iModIntro.
wp_bind (App (of_val f1) _).
rewrite CG_iter_of_val.
tp_apply j steps_CG_iter.
rewrite CG_iter_subst.
tp_bind j (App (of_val f2) _).
iSpecialize ("Hff" $! (y1, y2) with "[Hy]"); first by iFrame.
iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
iApply fupd_wp. iMod "Hff". iModIntro.
iApply (wp_wand with "Hff").
iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
tp_normalise j. asimpl.
iApply fupd_wp. tp_rec j; auto using to_of_val.
asimpl.
rewrite CG_iter_subst. asimpl.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val).
tp_snd j; auto using to_of_val.
tp_normalise j.
destruct (decide (istk' = istk)) as [e | nestk]; subst.
- (* CAS succeeds *) iRight.
iSplitR; first done.
iNext. iIntros "Hst".
rel_bind_r (acquire #l)%E. iApply (bin_log_related_acquire_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
unfold CG_push. unlock. do 2 rel_rec_r.
rel_load_r.
rel_store_r. solve_to_val. (* TODO rel_tactics *) simpl.
rel_rec_r.
rel_bind_r (release #l)%E. iApply (bin_log_related_release_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
iModIntro.
iPoseProof "Hsl" as "Hsl'".
rewrite {2}StackLink_unfold.
iDestruct "Hsl'" as (zl w') "[% [Hzl Hsl']]". simplify_eq/=.
iSpecialize ("IH" $! zl z2).
iPoseProof (persistentP ((StackLink τi) (#zl, z2)) with "Hsl") as "Hsl_box".
iSpecialize ("IH" with "Hsl_box").
iSpecialize ("IH" with "Hj").
iApply wp_rec; auto. iNext. asimpl.
wp_bind (Snd _). iApply wp_snd; auto using to_of_val.
iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
{ iNext. rewrite {2}/sinv. iExists _,_,_.
iFrame "Hoe Hst' Hst Hl".
rewrite (StackLink_unfold _ ((LocV nstk), _)).
iExists _, _. iSplitR; auto.
iFrame "Hnstk".
iRight. iExists _, _, _, _. auto. }
rel_if_true_l. simpl.
by rel_vals.
- (* CAS fails *) iLeft.
iSplitR; first by (iPureIntro; congruence).
iNext. iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
rel_if_false_l. simpl.
rel_rec_l.
by iApply "IH".
Qed.
Lemma FG_CG_push_refinement ρ st st' (τi : D) l Δ {τP : ww, PersistentP (τi ww)} {SH : stackG Σ}: