Skip to content

GitLab

Commit 545272f2 authored by Dan Frumin's avatar Dan Frumin
Browse files

[stack] Initial work on the module refinement

parent 28dcb4a3
Hide whitespace changes
Inline Side-by-side
Showing with 279 additions and 11 deletions
theories/examples/stack/CG_stack.v
View file @ 545272f2
......@@ -54,16 +54,81 @@ Definition CG_snap_iter : val := λ: "st" "l" "f",
Definition CG_stack_body : val := λ: "st" "l",
(CG_locked_push "st" "l", CG_locked_pop "st" "l", CG_snap_iter "st" "l").
(* stack :=
Λα. (λ(l : lock) (s : stack α). stack_body s l) (ref nil) newlock *)
(* TODO: I want `solve_closed` to solve this so that I can use newlock in the program *)
(* Instance: Closed ∅ ((λ: "l", #()) newlock). *)
(* Proof. solve_closed. Qed *)
Definition CG_stack : val :=
Λ: let: "l" := ref #♭ false in
let: "st" := ref Nile in
CG_stack_body "st" "l".
(** Coarse-grained stack presented as a module *)
(* type s α := (ref (list α), lockτ) *)
Definition sτ α := TProd (Tref (CG_StackType α)) LockType.
(* newStack : ∀ α, s α *)
Definition newStack : val := Λ: λ: <>,
(ref Nile, ref #false)%E.
(* popStack : ∀ α, s α → MAYBE α *)
Definition popStack : val := Λ: λ: "x",
CG_locked_pop (Fst "x") (Snd "x") #().
(* pushStack : ∀ α, s α → α → () *)
Definition pushStack : val := Λ: λ: "x" "a",
CG_locked_push (Fst "x") (Snd "x") "a".
Definition stackmod : val := Λ:
Pack (TApp newStack, TApp popStack, TApp pushStack).
Section typing.
Hint Unfold sτ : typeable.
Lemma newStack_typed Γ :
Γ ⊢ₜ newStack : TForall (TArrow TUnit (sτ (TVar 0))).
Proof.
unlock sτ newStack. (* TODO need to explicitly unlock newStack here *)
solve_typed.
Qed.
Hint Resolve newStack_typed : typeable.
Lemma popStack_typed Γ :
Γ ⊢ₜ popStack : TForall $ TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0)).
Proof.
unlock sτ popStack. (* TODO need to explicitly unlock newStack here *)
unlock CG_locked_pop CG_pop.
repeat (econstructor; solve_typed).
Qed.
Hint Resolve popStack_typed : typeable.
Lemma pushStack_typed Γ :
Γ ⊢ₜ pushStack : TForall $ TArrow (sτ (TVar 0)) (TArrow (TVar 0) TUnit).
Proof.
unlock sτ pushStack. (* TODO need to explicitly unlock newStack here *)
unlock CG_locked_push CG_push.
repeat (econstructor; solve_typed).
Qed.
Hint Resolve pushStack_typed : typeable.
Lemma stackmod_typed Γ :
Γ ⊢ₜ stackmod : TForall $ TExists $ TProd (TProd
(TArrow TUnit (TVar 0))
(TArrow (TVar 0) (TSum TUnit (TVar 1))))
(TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
Proof.
unlock stackmod.
econstructor.
eapply TPack with (sτ (TVar 0)).
econstructor; [econstructor | ].
- simpl.
replace (TArrow TUnit (sτ (TVar 0))) with (TArrow TUnit (sτ (TVar 0))).[TVar 0/]; last first.
{ autosubst. }
solve_typed.
- simpl.
replace (TArrow (sτ (TVar 0)) (TSum TUnit (ids 0)))
with (TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0))).[TVar 0/]; last first.
{ autosubst. }
solve_typed.
- simpl.
replace (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit))
with (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit)).[TVar 0/] by autosubst.
solve_typed.
Qed.
Hint Resolve stackmod_typed.
End typing.
Section CG_Stack.
Context `{logrelG Σ}.
......@@ -78,7 +143,6 @@ Section CG_Stack.
Hint Resolve CG_push_type : typeable.
(* Lemma steps_CG_push E ρ j K st v w : *)
(* nclose specN ⊆ E → *)
(* spec_ctx ρ -∗ st ↦ₛ v -∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w)) *)
......
theories/examples/stack/FG_stack.v
View file @ 545272f2
......@@ -59,6 +59,70 @@ Definition FG_stack : val :=
Λ: let: "st" := ref Nile in
FG_stack_body "st".
Definition sτ (α : type) : type := Tref (FG_StackType α).
Definition newStack : val := Λ: λ: <>, ref Nile.
Definition popStack : val := Λ: λ: "st", FG_pop "st" #().
Definition pushStack : val := Λ: FG_push.
Definition stackmod : val := Λ:
Pack (TApp newStack, TApp popStack, TApp pushStack).
Section typing.
Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
Hint Unfold sτ : typeable.
Lemma newStack_typed Γ :
Γ ⊢ₜ newStack : TForall (TArrow TUnit (sτ (TVar 0))).
Proof.
unlock sτ newStack. (* TODO need to explicitly unlock newStack here *)
solve_typed.
Qed.
Hint Resolve newStack_typed : typeable.
Lemma popStack_typed Γ :
Γ ⊢ₜ popStack : TForall $ TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0)).
Proof.
unlock sτ popStack. (* TODO need to explicitly unlock newStack here *)
unlock FG_pop.
repeat (econstructor; eauto 10 with typeable).
Qed.
Hint Resolve popStack_typed : typeable.
Lemma pushStack_typed Γ :
Γ ⊢ₜ pushStack : TForall $ TArrow (sτ (TVar 0)) (TArrow (TVar 0) TUnit).
Proof.
unlock sτ pushStack. (* TODO need to explicitly unlock newStack here *)
unlock FG_push.
solve_typed.
Qed.
Hint Resolve pushStack_typed : typeable.
Lemma stackmod_typed Γ :
Γ ⊢ₜ stackmod : TForall $ TExists $ TProd (TProd
(TArrow TUnit (TVar 0))
(TArrow (TVar 0) (TSum TUnit (TVar 1))))
(TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
Proof.
unlock stackmod.
econstructor.
eapply TPack with (sτ (TVar 0)).
econstructor; [econstructor | ].
- simpl.
replace (TArrow TUnit (sτ (TVar 0))) with ((TArrow TUnit (sτ (TVar 0))).[TVar 0/]); last first.
{ autosubst. }
solve_typed.
- simpl.
replace (TArrow (sτ (TVar 0)) (TSum TUnit (ids 0)))
with (TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0))).[TVar 0/]; last first.
{ autosubst. }
solve_typed.
- simpl.
replace (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit))
with (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit)).[TVar 0/] by autosubst.
solve_typed.
Qed.
Hint Resolve stackmod_typed.
End typing.
Section FG_stack.
(* Fine-grained push *)
......
theories/examples/stack/module_refinement.v 0 → 100644
View file @ 545272f2
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
CG_stack FG_stack stack_rules refinement.
Section Mod_refinement.
Context `{logrelG Σ, stackG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Import lang.
Program Definition sint `{logrelG Σ, stackG Σ} τi : prodC valC valC -n> iProp Σ := λne vv,
(∃ (l stk stk' : loc), ⌜(vv.2) = (# stk', # l)%V⌝ ∗ ⌜(vv.1) = #stk⌝
∗ inv stackN (sinv τi stk stk' l))%I.
Next Obligation. solve_proper. Qed.
Instance sint_persistent τi vv : PersistentP (sint τi vv).
Proof. apply _. Qed.
Lemma interp_subst_up_2 Δ1 Δ2 τ τi :
⟦ τ ⟧ (Δ1 ++ Δ2) ≡ ⟦ τ.[upn (length Δ1) (ren (+1))] ⟧ (Δ1 ++ τi :: Δ2).
Proof.
revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto.
- intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
- intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
- unfold interp_expr. intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τ' ww /=.
properness; auto. apply (IHτ (_ :: _)).
- intros vv; simpl.
rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..].
assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
{ lia. }
rewrite Hwat. simpl. done.
- unfold interp_expr.
intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros vv; simpl; properness; auto. by apply IHτ.
Qed.
Lemma interp_subst_2 τ τi Δ :
⟦ τ ⟧ Δ ≡ ⟦ τ.[ren (+1)] ⟧ (τi :: Δ).
Proof. by apply (interp_subst_up_2 []). Qed.
Lemma bin_log_weaken_2 τi Δ Γ e1 e2 τ :
{⊤,⊤;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
{⊤,⊤;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
Proof.
rewrite bin_log_related_eq /bin_log_related_def.
iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
iSpecialize ("Hlog" $! vvs with "Hs [HΓ]").
{ by rewrite interp_env_ren. }
unfold interp_expr.
iIntros (j K) "Hj /=".
iMod ("Hlog" with "Hj") as "Hlog".
iApply (wp_mono with "Hlog").
iIntros (v). simpl.
iDestruct 1 as (v') "[Hj Hτ]".
iExists v'. iFrame.
by rewrite -interp_subst_2.
Qed.
Lemma module_refinmenet Δ Γ :
{⊤,⊤;Δ;Γ} ⊨ FG_stack.stackmod ≤log≤ CG_stack.stackmod : TForall $ TExists $ TProd (TProd
(TArrow TUnit (TVar 0))
(TArrow (TVar 0) (TSum TUnit (TVar 1))))
(TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
Proof.
unlock FG_stack.stackmod CG_stack.stackmod.
iApply bin_log_related_tlam; auto.
iIntros (τi Hτi) "!#".
iApply (bin_log_related_pack _ (sint τi)).
do 3 rel_tlam_l.
do 3 rel_tlam_r.
repeat iApply bin_log_related_pair.
- iApply bin_log_related_arrow; eauto.
iAlways. iIntros (? ?) "_".
rel_seq_l.
rel_seq_r.
rel_alloc_l as istk "Histk". simpl.
rel_alloc_l as stk "Hstk".
rel_alloc_r as stl' "Hstk'".
rel_alloc_r as l "Hl".
rel_vals.
admit.
- iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "#Hvv /=".
iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
simplify_eq/=.
rel_let_l.
rel_let_r.
Transparent FG_pop CG_locked_pop.
rel_rec_l.
rel_proj_r; rel_rec_r.
unlock CG_locked_pop. simpl_subst/=.
rel_proj_r.
rel_let_r.
replace (#();; acquire # l ;; let: "v" := (CG_pop #stk') #() in release # l ;; "v")%E with ((CG_locked_pop $/ LitV (Loc stk') $/ LitV (Loc l)) #())%E; last first.
{ unlock CG_locked_pop. simpl_subst/=. reflexivity. }
replace (TSum TUnit (TVar 1))
with (TSum TUnit (TVar 0)).[ren (+1)] by done.
iApply bin_log_weaken_2.
by iApply FG_CG_pop_refinement'.
- iApply bin_log_related_arrow_val; eauto.
{ unlock FG_push. done. }
iAlways. iIntros (? ?) "#Hvv /=".
iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
simplify_eq/=.
rel_let_r.
Transparent FG_push.
rel_rec_l.
iApply bin_log_related_arrow_val; eauto.
{ unlock FG_push. simpl_subst/=. done. }
{ unlock FG_push. simpl_subst/=. solve_closed. }
iAlways. iIntros (v v') "#Hτi /=".
rel_let_r.
rel_proj_r; rel_rec_r.
unlock CG_locked_push. simpl_subst/=.
rel_proj_r; rel_let_r.
replace (let: "x" := v' in acquire # l ;; (CG_push #stk') "x" ;; release # l)%E
with ((CG_locked_push $/ LitV stk' $/ LitV l) v')%E; last first.
{ unlock CG_locked_push. simpl_subst/=. done. }
change TUnit with (TUnit.[ren (+1)]).
iApply (FG_CG_push_refinement with "Hinv Hτi").
Admitted.
End Mod_refinement.
theories/examples/stack/refinement.v
View file @ 545272f2
......@@ -80,18 +80,16 @@ Section Stack_refinement.
by iApply "IH".
Qed.
Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
Lemma FG_CG_pop_refinement' st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
inv stackN (sinv τi st st' l) -∗
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LitV (Loc st))%E ≤log≤ (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E : TArrow TUnit (TSum TUnit (TVar 0)).
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LitV (Loc st)) #() ≤log≤ (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
Proof.
iIntros "#Hinv".
Transparent CG_locked_pop FG_pop CG_pop.
unfold FG_pop, CG_locked_pop. unlock.
simpl_subst/=.
iApply bin_log_related_arrow; eauto.
iAlways. iIntros (? ?) "ZZ". simplify_eq/=. iClear "ZZ".
rel_rec_r.
rel_rec_l.
rel_rec_r.
iLöb as "IH".
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
......@@ -197,6 +195,20 @@ Section Stack_refinement.
by iApply "IH".
Qed.
Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
inv stackN (sinv τi st st' l) -∗
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LitV (Loc st))%E ≤log≤ (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E : TArrow TUnit (TSum TUnit (TVar 0)).
Proof.
iIntros "#Hinv".
iApply bin_log_related_arrow_val; eauto.
{ unlock FG_pop CG_locked_pop. reflexivity. }
{ unlock FG_pop CG_locked_pop. reflexivity. }
{ unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
{ unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
by iApply FG_CG_pop_refinement'.
Qed.
Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ:
inv stackN (sinv τi st st' l) -∗
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_read_iter $/ LitV (Loc st))%E ≤log≤ (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E : TArrow (TArrow (TVar 0) TUnit) TUnit.
......@@ -298,6 +310,7 @@ Section Stack_refinement.
iApply (related_ret with "[Hff]").
done.
Qed.
End Stack_refinement.
Section Full_refinement.
......
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