Skip to content
GitLab
Commit f35b6275 authored by Simcha van Collem's avatar Simcha van Collem
Browse files

tempppp

parent b27664a0
Hide whitespace changes
Inline Side-by-side
theories/chainable/implementation.v
View file @ f35b6275
......@@ -59,10 +59,10 @@ Inductive node : Set := {
prev : option node;
}.
Fixpoint node_prev_ind
(P : node -> Prop)
(Hbase : ∀ n, n.(prev) = None -> P n)
(IH : ∀ n n', n.(prev) = Some n' -> P n' -> P n)
(* Fixpoint node_prev_ind
(P : node → Prop)
(Hbase : ∀ n, n.(prev) = None → P n)
(IH : ∀ n n', n.(prev) = Some n' → P n' → P n)
(n : node)
: P n.
Proof.
......@@ -70,9 +70,24 @@ Proof.
- apply Hbase. apply Hprev.
- apply IH with n'. { apply Hprev. }
apply (node_prev_ind P Hbase IH).
Defined. *)
Fixpoint node_prev_ind
(P : node → Prop)
(Hbase : ∀ l b γrs γs, P {|location:=l; flag:=b; γrs:=γrs; γs:=γs; prev:=None|})
(IH : ∀ l b γrs γs n, P n → P {|location:=l; flag:=b; γrs:=γrs; γs:=γs; prev:=Some n|})
(n : node)
: P n.
Proof.
destruct n. destruct prev0 as [n'|]; last first.
- apply Hbase.
- apply IH.
apply (node_prev_ind P Hbase IH).
Defined.
Print node_prev_ind.
Definition sendsUR := gmapUR loc (exclR (prodO boolO gnameO)).
Canonical Structure nodeO := leibnizO node.
Definition sendsUR := gmapUR loc (exclR (prodO (prodO boolO gnameO) (optionO nodeO))).
Definition recvsUR := gmapUR loc (gset_disjR gname).
Class barrierG Σ := BarrierG {
......@@ -111,14 +126,13 @@ Section proof.
Global Instance node_chain_timeless n : Timeless (node_chain n).
Proof.
induction n as [[] H|[] n' H IH] using node_prev_ind;
simpl in *; rewrite H; apply _.
induction n as [|] using node_prev_ind; simpl in *; apply _.
Qed.
Fixpoint is_node (n : node) : iProp Σ :=
∃ (R : iProp Σ),
saved_prop_own n.(γs) DfracDiscarded R
∗ ((if n.(flag) then True else R)
∗ ▷ ((if n.(flag) then True else R)
-∗ ([∗ set] γr ∈ n.(γrs), ∃ (P : iProp Σ),
saved_prop_own γr DfracDiscarded P ∗ P))
∗ match n.(prev) with
......@@ -127,7 +141,7 @@ Section proof.
end.
Fixpoint to_sends (n : node) : sendsUR :=
<[n.(location) := Excl (n.(flag), n.(γs))]>
<[n.(location) := Excl (n.(flag), n.(γs), n.(prev))]>
match n.(prev) with
| None => ∅
| Some n' => to_sends n'
......@@ -153,19 +167,19 @@ Section proof.
let locations := to_locations n in
let sends := to_sends n in
let recvs := to_recvs n in
⌜dom sends = locations⌝
(* ⌜dom sends = locations⌝
∗ ⌜dom recvs = locations⌝
∗ ⌜∀ (m m' : node),
m.(location) = m'.(location) →
m.(location) ∈ locations →
m = m'⌝
∗ node_chain n ∗ is_node n
m = m'⌝ *)
node_chain n ∗ is_node n
∗ own γ (● sends) ∗ own γ' (● recvs).
Definition send (b : val) (R : iProp Σ) : iProp Σ :=
∃ (γ γ' : gname) (n : node),
⌜b = SOMEV #n.(location)⌝
∗ own γ (◯ {[ n.(location) := Excl (false, n.(γs)) ]})
∗ own γ (◯ {[ n.(location) := Excl (false, n.(γs), n.(prev)) ]})
∗ saved_prop_own n.(γs) DfracDiscarded R
∗ inv barrierN (barrier_inv γ γ').
......@@ -191,7 +205,7 @@ Section proof.
is_node n ⊣⊢
∃ (R : iProp Σ),
saved_prop_own n.(γs) DfracDiscarded R
∗ ((if n.(flag) then True else R)
∗ ▷ ((if n.(flag) then True else R)
-∗ ([∗ set] γr ∈ n.(γrs), ∃ (P : iProp Σ),
saved_prop_own γr DfracDiscarded P ∗ P))
∗ match n.(prev) with
......@@ -202,7 +216,7 @@ Section proof.
Lemma to_sends_eq (n : node) :
to_sends n =
<[n.(location) := Excl (n.(flag), n.(γs))]>
<[n.(location) := Excl (n.(flag), n.(γs), n.(prev))]>
match n.(prev) with
| None => ∅
| Some n' => to_sends n'
......@@ -218,6 +232,15 @@ Section proof.
end.
Proof. destruct n; done. Qed.
Lemma to_locations_eq (n : node) :
to_locations n =
{[n.(location)]} ∪
match n.(prev) with
| None => ∅
| Some n' => to_locations n'
end.
Proof. destruct n; done. Qed.
Lemma new_barrier_spec (R : iProp Σ) :
{{{ True}}} new_barrier #() {{{ b, RET b; send b R ∗ recv b R }}}.
Proof.
......@@ -228,18 +251,17 @@ Section proof.
iMod (saved_prop_alloc R DfracDiscarded) as (γr) "#Hγr"; first done.
set (n := {| location := l; flag := false; γrs := {[γr]};
γs := γs; prev := None |}).
iMod (own_alloc (● to_sends n ⋅ ◯ {[l := Excl (false, γs)]})) as (γ) "[H● H◯]".
iMod (own_alloc (● to_sends n ⋅ ◯ {[l := Excl (false, γs, None)]})) as (γ) "[H● H◯]".
{ apply auth_both_valid_discrete. simpl.
by rewrite insert_empty singleton_valid. }
iMod (own_alloc (● to_recvs n ⋅ ◯ {[l := GSet {[γr]}]})) as (γ') "[H●' H◯']".
{ apply auth_both_valid_discrete. simpl.
by rewrite insert_empty singleton_valid. }
iMod (inv_alloc barrierN _ (barrier_inv γ γ') with "[H● H●' Hl]") as "#Hinv".
{ iExists n. iFrame "H● H●'".
sdfdfdfdfdfdf (* TODO: Fix here *)
iSplitL "Hl". { iFrame. }
iExists R. simpl. iFrame "Hγs".
iSplitL; last done. iIntros "!> HR".
{ iNext. iExists n. iFrame "H● H●'".
simpl. iFrame "Hl".
iExists R. iFrame "Hγs".
iSplit; last done. iIntros "!> HR".
iApply big_sepS_singleton. iExists R. by iFrame. }
iSplitL "H◯".
- iExists γ, γ', n. auto with iFrame.
......@@ -252,79 +274,172 @@ Section proof.
iIntros "HΦ". wp_lam. wp_match. iApply "HΦ".
Qed.
(* Lemma dfdfdfdf (start n : node) (b : bool) (γ : gname) :
is_node start -∗
own γ (● to_sends start) -∗
own γ (◯ {[location n := Excl (b, n.(γs))]}) -∗
∃ v, n.(location) ↦ (#b, v).
Proof.
iIntros "Hstart H● H◯".
iInduction start as [start | start] "IH" using node_prev_ind;
destruct start as (l, flag, γrs, γs, prev); simpl in H;
subst prev; simpl.
- rewrite insert_empty.
iDestruct (own_valid_2 with "H● H◯")
as %[? _]%auth_both_valid_discrete.
pose proof (dom_included _ _ H).
rewrite !dom_singleton_L singleton_subseteq in H0. subst l.
rewrite lookup_included in H.
specialize H with (location n).
rewrite !lookup_singleton Excl_included in H.
apply leibniz_equiv in H.
injection H as -> ->.
iDestruct "Hstart" as (R) "[Hl _]".
iExists NONEV. iApply "Hl".
- rename start1 into prev.
iDestruct (own_valid_2 with "H● H◯")
as %[? _]%auth_both_valid_discrete.
rewrite lookup_included in H.
specialize H with (location n).
rewrite lookup_singleton option_included in H.
destruct H as [C | (? & ? & [= <-] & ? & ?)]; first discriminate.
rewrite lookup_insert_Some in H0.
destruct H0 as [[-> <-] | [? ?]].
+ destruct H1 as [[= -> <-]%leibniz_equiv | [c H%leibniz_equiv]].
* iDestruct "Hstart" as (R) "[Hl _]".
iExists _. iApply "Hl".
* discriminate H.
+ iDestruct "Hstart" as (R) "(Hl & #Hsp & HR & Hprev)". *)
Lemma wp_read_node (n start : node) (γ : gname) (b : bool)
(s : stuckness) (E : coPset) (Ψ : val → iProp Σ) :
own γ (● to_sends start) -∗
own γ (◯ {[location n := Excl (b, γs n)]}) -∗
own γ (◯ {[n.(location) := Excl (b, n.(γs), n.(prev))]}) -∗
node_chain start -∗
(own γ (● to_sends start) -∗
own γ (◯ {[location n := Excl (b, γs n)]}) -∗
own γ (◯ {[n.(location) := Excl (b, n.(γs), n.(prev))]}) -∗
node_chain start -∗
Ψ (#b, option_node_to_val n.(prev))%V) -∗
WP ! #(location n) @ s; E {{ v, Ψ v }}.
WP ! #(n.(location)) @ s; E {{ v, Ψ v }}.
Proof.
iIntros "H● H◯ Hstart HPost".
iDestruct (node_chain_eq with "Hstart") as "Hstart".
(* TODO: Is there a way to only rewrite in H●?
iRewrite doesn't seem to work... *)
rewrite to_sends_eq.
iInduction start as [start | start] "IH" using node_prev_ind;
rewrite H; clear H.
(* ;
destruct start as (l, flag, γrs, γs, prev); simpl in H;
subst prev; simpl. *)
- iDestruct "Hstart" as "[Hl _]".
rewrite insert_empty.
iDestruct (own_valid_2 with "H● H◯")
as %[? _]%auth_both_valid_discrete.
pose proof (dom_included _ _ H).
rewrite !dom_singleton_L singleton_subseteq in H0. subst l.
rewrite lookup_included in H.
specialize H with (location n).
rewrite !lookup_singleton Excl_included in H.
apply leibniz_equiv in H.
injection H as -> ->.
wp_load.
iDestruct "Hstart" as (R) "[Hl _]".
iExists NONEV. iApply "Hl".
Admitted.
iIntros "H● H◯ Hchain HPost".
iDestruct (own_valid_2 with "H● H◯")
as %[? _]%auth_both_valid_discrete.
iSpecialize ("HPost" with "H● H◯").
pose proof (dom_included _ _ H).
rewrite dom_singleton_L singleton_subseteq_l in H0.
rewrite lookup_included in H.
specialize H with (location n).
rewrite lookup_singleton in H.
iInduction start as [|] "IH" using node_prev_ind; simpl in *.
- iDestruct "Hchain" as "[Hl _]".
rewrite insert_empty in H, H0.
rewrite dom_singleton_L elem_of_singleton in H0.
subst l. rewrite lookup_singleton Excl_included in H.
fold_leibniz. injection H as <- <- ->.
wp_load. iApply "HPost". by iFrame.
- iDestruct "Hchain" as "[Hl Hchain]".
rewrite dom_insert_L in H0.
destruct (decide (l = n.(location))) as [-> | Hneq].
+ rewrite lookup_insert Excl_included in H.
fold_leibniz. injection H as <- <- ->.
wp_load. iApply "HPost". by iFrame.
+ rewrite elem_of_union elem_of_singleton in H0.
destruct H0; first done.
rewrite lookup_insert_ne in H; last done.
iApply ("IH" $! H0 H with "Hchain").
iIntros "Hchain". iApply "HPost". iFrame.
Qed.
Fixpoint signal_node (l : loc) (n : node) : node :=
if bool_decide (n.(location) = l)
then {|location:=n.(location); flag:=true;
γrs:=n.(γrs); γs:=n.(γs); prev:=n.(prev)|}
else {|location:=n.(location); flag:=n.(flag);
γrs:=n.(γrs); γs:=n.(γs); prev:=signal_node l <$> n.(prev)|}.
(* FIXME: Perhaps for these *)
Lemma to_recvs_signal_node (l : loc) (n : node) :
to_recvs (signal_node l n) = to_recvs n.
Proof.
induction n using node_prev_ind; simpl.
- destruct (bool_decide (l0 = l)); reflexivity.
- destruct (bool_decide (l0 = l)); simpl;
[|rewrite IHn]; reflexivity.
Qed.
(* Lemma to_sends_signal_node (l : loc) (n : node) :
l ∈ dom (to_sends n) →
to_sends (signal_node l n)
= <[n.(location) := Excl (true, n.(γs), n.(prev))]> (to_sends n).
Proof.
intros Hdom. induction n using node_prev_ind; simpl in *.
- destruct (decide (l0 = l)) as [-> | Hneq].
+ rewrite bool_decide_eq_true_2; last done.
simpl. by rewrite insert_insert insert_empty.
+ by rewrite insert_empty dom_singleton_L elem_of_singleton in Hdom.
- destruct (decide (l0 = l)) as [-> | Hneq].
+ rewrite bool_decide_eq_true_2; last done.
simpl. by rewrite insert_insert.
+ rewrite bool_decide_eq_false_2; last done. simpl.
rewrite dom_insert elem_of_union elem_of_singleton in Hdom.
destruct Hdom; first done.
apply IHn in H. rewrite H.
rewrite insert_insert.
Qed. *)
Lemma wp_signal_node (n start : node) (γ : gname) (R : iProp Σ)
(s : stuckness) (E : coPset) (Ψ : val → iProp Σ) :
R -∗
saved_prop_own n.(γs) DfracDiscarded R -∗
own γ (● to_sends start) -∗
own γ (◯ {[n.(location) := Excl (false, n.(γs), n.(prev))]}) -∗
▷ is_node start -∗
node_chain start -∗
(let start' := signal_node n.(location) start in
own γ (● to_sends start') -∗
is_node start' -∗
node_chain start' -∗
Ψ #()) -∗
WP #(n.(location)) <- (#true, option_node_to_val n.(prev))%V @ s; E {{ v, Ψ v }}.
Proof.
iIntros "HR #Hsp H● H◯ Hstart Hchain HPost".
iDestruct (own_valid_2 with "H● H◯")
as %[? _]%auth_both_valid_discrete.
pose proof (dom_included _ _ H).
rewrite dom_singleton_L singleton_subseteq_l in H0.
rewrite lookup_included in H.
specialize H with (location n).
rewrite lookup_singleton in H.
rewrite option_included in H.
destruct H as [|(? & ? & [=<-] & ? & ?)]; first congruence.
(* TODO: AAAAAAAAAAAAAAAAAAAAAAA *)
destruct H2 as [<-%leibniz_equiv | H]; last first.
{ destruct H as [f H%leibniz_equiv]. }
iMod (own_update_2 _ _ _
(● <[n.(location) := Excl (true, n.(γs), n.(prev))]> _ ⋅ ◯ _)
with "H● H◯") as "[H● H◯]".
{ apply auth_update. eapply insert_local_update.
- apply H1.
- Fail apply lookup_singleton. admit.
-
apply lookup_insert. admit. }
by apply exclusive_local_update. }
pose proof (dom_included _ _ H).
rewrite dom_singleton_L singleton_subseteq_l in H0.
rewrite lookup_included in H.
specialize H with (location n).
rewrite lookup_singleton in H.
iInduction start as [|] "IH" using node_prev_ind; simpl in *.
- iDestruct "Hchain" as "[Hl _]".
rewrite !insert_empty in H, H0 |- *.
rewrite dom_singleton_L elem_of_singleton in H0.
subst l. rewrite bool_decide_eq_true_2; last done.
rewrite lookup_singleton Excl_included in H.
fold_leibniz. injection H as <- <- ->.
wp_store.
iMod (own_update_2 _ _ _
(● <[n.(location) := Excl (true, n.(γs), None)]> _ ⋅ ◯ _)
with "H● H◯") as "[H● H◯]".
{ apply auth_update. eapply singleton_local_update.
{ apply lookup_singleton. }
by apply exclusive_local_update. }
simpl. rewrite insert_singleton.
iApply ("HPost" with "H● [Hstart HR] [$Hl]").
iDestruct "Hstart" as (R') "(#Hsp' & HPs & _)".
iDestruct (saved_prop_agree with "Hsp Hsp'") as "Heq".
iExists R. iFrame "Hsp". iSplit; last done.
iIntros "!> _". iApply "HPs". by iRewrite -"Heq".
- iDestruct "Hchain" as "[Hl Hchain]".
rewrite dom_insert_L in H0.
destruct (decide (l = n.(location))) as [-> | Hneq].
+ rewrite bool_decide_eq_true_2; last done.
simpl. rewrite lookup_insert Excl_included in H.
fold_leibniz. injection H as <- <- ->.
wp_store.
iMod (own_update_2 _ _ _
(● <[n.(location) := Excl (true, n.(γs), Some start)]> _ ⋅ ◯ _)
with "H● H◯") as "[H● H◯]".
{ apply auth_update. eapply singleton_local_update.
{ Fail apply lookup_insert. admit. }
by apply exclusive_local_update. }
rewrite insert_insert.
iApply ("HPost" with "H● [HR Hstart] [$Hl $Hchain]").
iDestruct "Hstart" as (R') "(#Hsp' & HPs & Hstart)".
iDestruct (saved_prop_agree with "Hsp Hsp'") as "Heq".
iExists R. iFrame "Hsp Hstart".
iIntros "!> _". iApply "HPs". by iRewrite -"Heq".
+ rewrite elem_of_union elem_of_singleton in H0.
destruct H0; first done.
rewrite lookup_insert_ne in H; last done.
iApply ("IH" $! H0 H with "HR").
iIntros "Hchain". iApply "HPost". iFrame.
Lemma signal_spec (b : val) (R : iProp Σ) :
{{{ send b R ∗ R }}} signal b {{{ RET #(); True }}}.
......@@ -333,14 +448,25 @@ Section proof.
iDestruct "Hs" as (γ γ' n ->) "(H◯ & #Hsp & #Hinv)".
wp_lam. wp_apply unwrap_spec. wp_let. wp_bind (! _)%E.
iInv barrierN as "H" "Hclose".
(* bi.later_exist is need due to some bug:
(* FIXME: bi.later_exist is need due to some bug:
if barrier_inv started with ∃ n : nat, this isn't needed...*)
iDestruct (bi.later_exist with "H") as (start) "(>Hchain & Hstart & >H● & >H●')".
wp_apply (wp_read_node with "H● H◯ Hchain").
iIntros "H● H◯ Hchain".
iMod ("Hclose" with "[H● H●' Hchain Hstart]") as "_".
{ iExists start. iFrame. }
iModIntro. wp_let. wp_proj.
{ iExists start. iFrame. } clear start.
iModIntro. wp_let. wp_proj. wp_pair.
iInv barrierN as "H" "Hclose".
(* FIXME: bi.later_exist is need due to some bug:
if barrier_inv started with ∃ n : nat, this isn't needed...*)
iDestruct (bi.later_exist with "H") as (start) "(>Hchain & Hstart & >H● & >H●')".
wp_apply (wp_signal_node with "HR Hsp H● H◯ Hstart Hchain").
iIntros "H● Hstart Hchain".
iMod ("Hclose" with "[H● H●' Hchain Hstart]") as "_"; last by iApply "HΦ".
iExists (signal_node n.(location) start). iFrame.
by rewrite to_recvs_singal_something.
Admitted.
Global Opaque new_barrier signal wait extend.
End proof.
Supports Markdown
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