Skip to content
Snippets Groups Projects
Commit e9d18530 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make closures in coinflip consistent.

parent e82a0c75
No related branches found
No related tags found
No related merge requests found
Pipeline #29686 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/examples/coinflip.v
+ 33
− 47
View file @ e9d18530
...@@ -5,28 +5,28 @@ From reloc Require Import reloc lib.lock. ...@@ -5,28 +5,28 @@ From reloc Require Import reloc lib.lock.
From reloc.examples Require Import lateearlychoice. From reloc.examples Require Import lateearlychoice.
Definition newcoin : val := λ: <>, ref #false. Definition newcoin : val := λ: <>, ref #false.
Definition flip : val := λ: "c" <>, "c" <- rand #(). Definition flip : val := λ: "c", "c" <- rand #().
Definition read : val := λ: "c" <>, !"c". Definition read : val := λ: "c", !"c".
Definition newcoin_lazy : val := λ: <>, ref (SOME #false). Definition newcoin_lazy : val := λ: <>, ref (SOME #false).
Definition flip_lazy : val := λ: "c" <>, Definition flip_lazy : val := λ: "c",
"c" <- NONE. "c" <- NONE.
Definition flip_lazy' : val := λ: "c" "lk" "p" <>, Definition flip_lazy' : val := λ: "c" "lk" "p",
acquire "lk";; acquire "lk";;
"c" <- NONE;; "c" <- NONE;;
release "lk". release "lk".
Definition read_lazy : val := rec: "read" "c" <> := Definition read_lazy : val := rec: "read" "c" :=
match: !"c" with match: !"c" with
SOME "v" => "v" SOME "v" => "v"
| NONE => | NONE =>
let: "x" := rand #() in let: "x" := rand #() in
if: CAS "c" NONEV (SOME "x") if: CAS "c" NONEV (SOME "x")
then "x" then "x"
else "read" "c" #() else "read" "c"
end. end.
Definition read_lazy' : val := λ: "c" "lk" "p" <>, Definition read_lazy' : val := λ: "c" "lk" "p",
acquire "lk";; acquire "lk";;
let: "r" := let: "r" :=
match: !"c" with match: !"c" with
...@@ -42,15 +42,15 @@ Definition read_lazy' : val := λ: "c" "lk" "p" <>, ...@@ -42,15 +42,15 @@ Definition read_lazy' : val := λ: "c" "lk" "p" <>,
Definition coin1 : expr := Definition coin1 : expr :=
let: "c" := newcoin #() in let: "c" := newcoin #() in
(read "c", flip "c"). ((λ: <>, read "c"), (λ: <>, flip "c")).
Definition coin2 : expr := Definition coin2 : expr :=
let: "c" := newcoin_lazy #() in let: "c" := newcoin_lazy #() in
(read_lazy "c", flip_lazy "c"). ((λ: <>, read_lazy "c"), (λ: <>, flip_lazy "c")).
Definition coin2' : expr := Definition coin2' : expr :=
let: "c" := newcoin_lazy #() in let: "c" := newcoin_lazy #() in
let: "p" := NewProph in let: "p" := NewProph in
let: "lk" := newlock #() in let: "lk" := newlock #() in
(read_lazy' "c" "lk" "p", flip_lazy' "c" "lk" "p"). ((λ: <>, read_lazy' "c" "lk" "p"), (λ: <>, flip_lazy' "c" "lk" "p")).
Section proofs. Section proofs.
Context `{!relocG Σ, !lockG Σ}. Context `{!relocG Σ, !lockG Σ}.
...@@ -77,10 +77,8 @@ Section proofs. ...@@ -77,10 +77,8 @@ Section proofs.
clear vs. clear vs.
iNext. iIntros (lk γ) "#Hlk /=". do 2 rel_pure_l. iNext. iIntros (lk γ) "#Hlk /=". do 2 rel_pure_l.
iApply refines_pair. iApply refines_pair.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_apply_l (refines_acquire_l with "Hlk"). rel_apply_l (refines_acquire_l with "Hlk").
iNext. iIntros "Hlocked". iNext. iIntros "Hlocked".
iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l. iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
...@@ -96,10 +94,8 @@ Section proofs. ...@@ -96,10 +94,8 @@ Section proofs.
+ rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). + rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs. iFrame. iRight. iExists x. iFrame. } { iExists vs. iFrame. iRight. iExists x. iFrame. }
iNext. repeat rel_pure_l; rel_values. iNext. repeat rel_pure_l; rel_values.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_apply_l (refines_acquire_l with "Hlk"). rel_apply_l (refines_acquire_l with "Hlk").
iNext. iIntros "Hlocked". iNext. iIntros "Hlocked".
iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l. iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
...@@ -137,12 +133,10 @@ Section proofs. ...@@ -137,12 +133,10 @@ Section proofs.
with "[-]") as "#Hinv". with "[-]") as "#Hinv".
{ iNext. iExists false. iFrame. } { iNext. iExists false. iFrame. }
iApply refines_pair. iApply refines_pair.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose". rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose".
iModIntro. iExists _. iFrame. iNext. iIntros "Hce". iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk". rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. repeat rel_pure_r.
iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r. iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
...@@ -157,13 +151,11 @@ Section proofs. ...@@ -157,13 +151,11 @@ Section proofs.
repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_". repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
{ eauto with iFrame. } { eauto with iFrame. }
rel_values. rel_values.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_apply_l refines_rand_l. iNext. iIntros (b). rel_apply_l refines_rand_l. iNext. iIntros (b).
rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose". rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose".
iModIntro. iExists _. iFrame. iNext. iIntros "Hce". iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk". rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. repeat rel_pure_r.
iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r. iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r.
...@@ -198,10 +190,8 @@ Section proofs. ...@@ -198,10 +190,8 @@ Section proofs.
clear vs. clear vs.
iNext. iIntros (lk γ) "#Hlk /=". do 2 rel_pure_l. iNext. iIntros (lk γ) "#Hlk /=". do 2 rel_pure_l.
iApply refines_pair. iApply refines_pair.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_apply_l (refines_acquire_l with "Hlk"). rel_apply_l (refines_acquire_l with "Hlk").
iNext. iIntros "Hlocked". iNext. iIntros "Hlocked".
iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l. iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
...@@ -221,10 +211,8 @@ Section proofs. ...@@ -221,10 +211,8 @@ Section proofs.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs. iFrame. iRight. iExists x. iFrame. } { iExists vs. iFrame. iRight. iExists x. iFrame. }
iNext. repeat rel_pure_l; rel_values. iNext. repeat rel_pure_l; rel_values.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_rec_r. repeat rel_pure_r. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
iApply refines_arrow. iModIntro. iIntros (??) "_".
rel_pure_l. rel_pure_r.
rel_apply_l (refines_acquire_l with "Hlk"). rel_apply_l (refines_acquire_l with "Hlk").
iNext. iIntros "Hlocked". iNext. iIntros "Hlocked".
iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l. iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
...@@ -260,11 +248,10 @@ Section proofs. ...@@ -260,11 +248,10 @@ Section proofs.
do 2 rel_pure_r. do 2 rel_pure_r.
iApply refines_pair. iApply refines_pair.
- rel_rec_r. repeat rel_pure_r. - rel_pure_l; rel_pure_r.
rel_rec_l. repeat rel_pure_l. iApply refines_arrow. iIntros (??) "!> _". rel_pure_l; rel_pure_r.
iApply refines_arrow. iModIntro. iIntros (??) "_". rel_rec_r. repeat rel_pure_r.
rel_pure_l. rel_pure_r. iLöb as "IH". rel_rec_l.
iLöb as "IH".
rel_load_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose"; rel_load_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose";
iModIntro. iModIntro.
+ iExists _. iFrame. iNext. iIntros "Hc". + iExists _. iFrame. iNext. iIntros "Hc".
...@@ -277,7 +264,7 @@ Section proofs. ...@@ -277,7 +264,7 @@ Section proofs.
* iModIntro; iExists _. iFrame. iSplit. * iModIntro; iExists _. iFrame. iSplit.
{ iIntros (?); simplify_eq/=. } { iIntros (?); simplify_eq/=. }
iIntros (_). iNext. iIntros "Hc". iIntros (_). iNext. iIntros "Hc".
rel_pures_l. rel_apply_r (refines_acquire_r with "Hlk"). rel_pures_l. rel_pures_r. rel_apply_r (refines_acquire_r with "Hlk").
iIntros "Hlk". repeat rel_pure_r. rel_load_r. iIntros "Hlk". repeat rel_pure_r. rel_load_r.
repeat rel_pure_r. rel_apply_r (refines_rand_r b). repeat rel_pure_r. rel_apply_r (refines_rand_r b).
repeat rel_pure_r. rel_store_r. repeat rel_pure_r. rel_store_r.
...@@ -291,7 +278,7 @@ Section proofs. ...@@ -291,7 +278,7 @@ Section proofs.
iModIntro; iExists _. iFrame. iSplit; last first. iModIntro; iExists _. iFrame. iSplit; last first.
{ iIntros (?); simplify_eq/=. } { iIntros (?); simplify_eq/=. }
iIntros (_). iNext. iIntros "Hc". iIntros (_). iNext. iIntros "Hc".
rel_pures_l. rel_rec_l. do 2 rel_pure_l. rel_pures_l.
iMod ("Hclose" with "[-]") as "_". iMod ("Hclose" with "[-]") as "_".
{ eauto with iFrame. } { eauto with iFrame. }
iApply "IH". iApply "IH".
...@@ -305,10 +292,9 @@ Section proofs. ...@@ -305,10 +292,9 @@ Section proofs.
iMod ("Hclose" with "[-]") as "_". iMod ("Hclose" with "[-]") as "_".
{ eauto with iFrame. } { eauto with iFrame. }
rel_values. rel_values.
- rel_rec_l. repeat rel_pure_l. - rel_pure_l. rel_pure_r.
rel_rec_r. repeat rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
iApply refines_arrow. iModIntro. iIntros (??) "_". repeat rel_rec_l. repeat rel_rec_r. repeat rel_pure_l. repeat rel_pure_r.
repeat rel_pure_l. rel_pure_r.
rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose"; rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose";
iModIntro. iModIntro.
+ iExists _. iFrame. iNext. iIntros "Hc". + iExists _. iFrame. iNext. iIntros "Hc".
......
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