Skip to content
Snippets Groups Projects
Commit 966bf03d authored by Janno's avatar Janno
Browse files

Port sc_stack.v.

parent 7cd72123
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/examples/sc_stack.v
+ 89
− 96
View file @ 966bf03d
...@@ -10,6 +10,7 @@ Import uPred. ...@@ -10,6 +10,7 @@ Import uPred.
Section SCStack. Section SCStack.
Open Scope Z_scope.
Local Notation next := 0. Local Notation next := 0.
Local Notation data := 1. Local Notation data := 1.
...@@ -42,166 +43,158 @@ Section SCStack. ...@@ -42,166 +43,158 @@ Section SCStack.
Section proof. Section proof.
Context `{fG : foundationG Σ}. Context `{fG : foundationG Σ}.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Notation vPred := (@vPred Σ). Notation vPred := (vProp Σ).
Context (P: Z → vPred). Context (P: Z → vPred).
Local Open Scope VP. Definition SCStack': (loc -c> list Z -c> vProp Σ)
-c> loc -c> list Z -c> vProp Σ
Definition SCStack': (loc -c> list Z -c> @vPred_ofe Σ)
-c> loc -c> list Z -c> @vPred_ofe Σ
:= (fun F l A => := (fun F l A =>
∃ l', ZplusPos next l ↦ l' ∗ ∃ l', ZplusPos next l ↦ l' ∗
match A with match A with
| nil => l' = 0 | nil => ⌜l' = 0⌝
| v::A' => ■ (0 < l') ∗ Z.to_pos (l' + data) ↦ v ∗ P v | v::A' => ⌜0 < l'⌝ ∗ Z.to_pos (l' + data) ↦ v ∗ P v
∗ ▷ F (Z.to_pos l') A' ∗ ▷ F (Z.to_pos l') A'
end). end)%I.
Close Scope VP. Instance SCStack'_inhabited: Inhabited (loc -c> list Z -c> vProp Σ)
Instance SCStack'_inhabited: Inhabited (loc -c> list Z -c> @vPred_ofe Σ) := populate (λ _ _, True)%I.
:= populate (λ _ _, True%VP).
Instance SCStack'_contractive: Instance SCStack'_contractive:
Contractive (SCStack'). Contractive (SCStack').
Proof. Proof.
intros ? ? ? H ? A ?. intros ? ? ? H ? A.
repeat (apply uPred.exist_ne => ?). repeat (apply bi.exist_ne => ?).
apply uPred.sep_ne; [done|]. apply bi.sep_ne; [done|].
destruct A as [|v A]; [done|]. destruct A as [|v A]; [done|].
repeat (apply uPred.sep_ne; [done|]). repeat (apply bi.sep_ne; [done|]).
apply later_contractive. destruct n => //. by apply (H). apply later_contractive. destruct n => //. by apply (H).
Qed. Qed.
Definition SCStack := fixpoint (SCStack'). Definition SCStack := fixpoint (SCStack').
Lemma newStack_spec: Lemma newStack_spec:
{{{{ True }}}} {{{ ⎡PSCtx⎤ }}}
newStack #() newStack #()
{{{{ (s: loc), RET #s; SCStack s nil }}}}. {{{ (s: loc), RET #s; SCStack s nil }}}.
Proof. Proof.
intros. iViewUp. iIntros "#kI kS _ Post". iIntros (Φ) "#kI Post".
wp_seq. iNext. wp_bind Alloc. wp_seq. wp_bind Alloc.
iApply (alloc with "[%] kI kS []"); [done|done|done|]. wp_apply (alloc with "kI"); [done|].
iNext. iViewUp. iIntros (x) "kS os". iIntros (x) "os".
wp_seq. iNext. wp_seq.
wp_bind ([_]_na <-_)%E. wp_bind ([_]_na <-_)%E.
iApply (na_write with "[%] kI kS [$os]"); [done|done|]. wp_apply (na_write with "[$kI $os]"); [done|].
iNext. iViewUp; iIntros "kS os". iIntros "os".
wp_seq. iNext. wp_value. wp_seq.
iApply ("Post" with "[%] kS [os]"); first done. iApply ("Post" with "[os]").
rewrite (fixpoint_unfold (SCStack') _ _ _ ). rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
iExists _. by iFrame "os". iExists _. by iFrame "os".
Qed. Qed.
Lemma push_spec s v A: Lemma push_spec s v A:
{{{{ SCStack s A ∗ P v }}}} {{{ ⎡PSCtx⎤ ∗ SCStack s A ∗ P v }}}
push #s #v push #s #v
{{{{ RET #(); SCStack s (v :: A) }}}}. {{{ RET #(); SCStack s (v :: A) }}}.
Proof. Proof.
intros. iViewUp. iIntros "#kI kS (Stack & P) Post". intros. iIntros "[#kI (Stack & P)] Post".
wp_lam. iNext. wp_value. wp_let. iNext. wp_lam. wp_let.
wp_bind (malloc _). wp_bind (malloc _).
iApply (wp_mask_mono); first auto. iApply (wp_mask_mono); first auto.
iApply (malloc_spec with "[%] kI kS []"); [omega|done|done|]. wp_apply (malloc_spec with "kI []"); [omega|done|].
iNext. iViewUp. iIntros (n) "kS oLs". iIntros (n) "oLs".
rewrite -bigop.vPred_big_opL_fold iDestruct "oLs" as "(ol & od & _)".
big_op.big_sepL_cons big_op.big_opL_singleton. wp_let. wp_bind ([_]_na <- _)%E. wp_op.
iDestruct "oLs" as "(ol & od)". wp_apply (na_write with "[$kI $od]"); [done|].
wp_let. iNext. wp_bind ([_]_na <- _)%E. wp_op. iNext. iIntros "od".
iApply (na_write with "[%] kI kS od"); [done|done|]. wp_seq. wp_bind ([_]_na)%E.
iNext. iViewUp. iIntros "kS od".
wp_seq. iNext. wp_bind ([_]_na)%E. rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
rewrite (fixpoint_unfold (SCStack') _ _ _ ).
iDestruct "Stack" as (h) "[oH oT]". iDestruct "Stack" as (h) "[oH oT]".
iApply (na_read with "[%] kI kS oH"); [done|done|]. wp_apply (na_read with "[$kI $oH]"); [done|].
iNext. iViewUp. iIntros (z) "kS [% oH]". subst z. iIntros (z) "[% oH]". subst z.
wp_seq. iNext. wp_bind ([_]_na <- _)%E. wp_op. iNext. wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
iApply (na_write with "[%] kI kS ol"); [done|done|]. wp_apply (na_write with "[$kI $ol]"); [done|].
iNext. iViewUp. iIntros "kS ol". iIntros "ol".
wp_seq. iNext. wp_op. iNext. wp_seq. wp_op.
iApply (na_write with "[%] kI kS [$oH]"); [done|done|]. wp_apply (na_write with "[$kI $oH]"); [done|].
iNext. iViewUp. iIntros "kS oH". iIntros "oH".
iApply ("Post" with "[%] kS"); first done. iApply ("Post").
rewrite (fixpoint_unfold (SCStack') _ _ _ ). rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
iExists _. iFrame "oH P". iSplitL ""; first (iPureIntro; lia). iExists _. iFrame "oH P". iSplitL ""; first (iPureIntro; lia).
iSplitL "od". iSplitL "od".
- rewrite (_: Z.to_pos (Z.pos n + data) = ZplusPos data n); first done. - rewrite (_: Z.to_pos (Z.pos n + data) = ZplusPos data n); first done.
rewrite /ZplusPos. f_equal. omega. rewrite /ZplusPos. f_equal. omega.
- iNext. rewrite (fixpoint_unfold (SCStack') _ _ _ ). - iNext. rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
iExists h. iFrame "oT ol". iExists h. iFrame "oT ol".
Qed. Qed.
Lemma pop_spec s A: Lemma pop_spec s A:
{{{{ SCStack s A }}}} {{{ ⎡PSCtx⎤ ∗ SCStack s A }}}
pop #s pop #s
{{{{ (z: Z), RET #z; {{{ (z: Z), RET #z;
match A with match A with
| nil => ■ (z = 0) ∗ SCStack s A | nil => ⌜z = 0⌝ ∗ SCStack s A
| v :: A' => ■ (z = v) ∗ SCStack s A' ∗ P v | v :: A' => ⌜z = v⌝ ∗ SCStack s A' ∗ P v
end }}}}. end }}}.
Proof. Proof.
intros. iViewUp. iIntros "#kI kS Stack Post". intros. iIntros "[#kI Stack] Post".
wp_lam. iNext. wp_lam.
wp_bind ([_]_na)%E. wp_bind ([_]_na)%E.
rewrite (fixpoint_unfold (SCStack') _ _ _ ). rewrite {1}/SCStack (fixpoint_unfold (SCStack') _ _).
iDestruct "Stack" as (h) "[oH oT]". iDestruct "Stack" as (h) "[oH oT]".
iApply (na_read with "[%] kI kS oH"); [done|done|]. wp_apply (na_read with "[$kI $oH]"); [done|].
iNext. iViewUp. iIntros (z) "kS [% oH]". subst z. iIntros (z) "[% oH]". subst z.
wp_seq. iNext. wp_seq.
destruct A as [|v A']. destruct A as [|v A'].
- iDestruct "oT" as "%". subst h. - iDestruct "oT" as "%". subst h.
wp_op => [_|//]. iNext. wp_op. wp_if.
iApply wp_if_true. iNext. iApply ("Post").
wp_value.
iApply ("Post" with "[%] kS"); first done.
iSplitL ""; first done. iSplitL ""; first done.
rewrite (fixpoint_unfold (SCStack') _ _ _ ). iExists _. by iFrame "oH". rewrite /SCStack (fixpoint_unfold (SCStack') _ _). iExists _. by iFrame "oH".
- iDestruct "oT" as "(% & od & P & oT)". - iDestruct "oT" as "(% & od & P & oT)".
wp_op => [?|_]; first omega. iNext. wp_op. case_bool_decide; first omega.
iApply wp_if_false. iNext. wp_if.
wp_bind ([_]_na)%E. wp_op. iNext. wp_op. iNext. wp_bind ([_]_na)%E. wp_op. wp_op.
rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + 1)); last first. rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + 1)); last first.
{ rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. } { rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. }
iApply (na_read with "[%] kI kS od"); [done|done|]. wp_apply (na_read with "[$kI $od]"); [done|].
iNext. iViewUp. iIntros (z) "kS [% od]". subst z. iIntros (z) "[% od]". subst z.
wp_seq. iNext. wp_seq.
wp_bind ([_]_na)%E. wp_op. iNext. wp_op. iNext. wp_bind ([_]_na)%E. wp_op. wp_op.
rewrite (fixpoint_unfold (SCStack') _ _ _ ). rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
iDestruct "oT" as (h') "[oP oT]". iDestruct "oT" as (h') "[oP oT]".
iApply (na_read with "[%] kI kS oP"); [done|done|]. wp_apply (na_read with "[$kI $oP]"); [done|].
iNext. iViewUp. iIntros (z) "kS [% oP]". subst z. iIntros (z) "[% oP]". subst z.
wp_seq. iNext. wp_bind ([_]_na <- _)%E. wp_seq. wp_bind ([_]_na <- _)%E.
iApply (na_write with "[%] kI kS [$oH]"); [done|done|..]. wp_apply (na_write with "[$kI $oH]"); [done|].
iNext. iViewUp. iIntros "kS oH". iIntros "oH".
wp_seq. iNext. wp_seq.
wp_bind (Dealloc _). wp_op. iNext. wp_op. iNext. wp_bind (Dealloc _). wp_op. wp_op.
iApply (wp_mask_mono); first auto. iApply (wp_mask_mono); first auto.
rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + data)); last first. rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + data)); last first.
{ rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. } { rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. }
iApply (dealloc with "[%] kI kS [$od]"); first done. wp_apply (dealloc with "[$kI $od]").
iNext. iViewUp. iIntros "kS _". iIntros "_".
wp_seq. iNext. wp_seq.
wp_bind (Dealloc _). wp_op. iNext. wp_op. iNext. wp_bind (Dealloc _). wp_op. wp_op.
iApply (wp_mask_mono); first auto. iApply (wp_mask_mono); first auto.
iApply (dealloc with "[%] kI kS [$oP]"); first done. wp_apply (dealloc with "[$kI $oP]").
iNext. iViewUp. iIntros "kS _". iIntros "_".
wp_seq. iNext. wp_seq.
wp_value. iApply ("Post").
iApply ("Post" with "[%] kS"); first done.
iSplitL ""; first done. iFrame "P". iSplitL ""; first done. iFrame "P".
rewrite (fixpoint_unfold (SCStack') _ _ _ ). rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
iExists _. by iFrame. iExists _. by iFrame.
Qed. Qed.
End proof. End proof.
......
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