Commit 326964bd authored by Ike Mulder's avatar Ike Mulder
Browse files

Fixed wrong HasRightId instance for ucmras, hopefully fixed barrier_client.

parent 8a0e7272
Pipeline #59777 passed with stage
in 31 minutes and 50 seconds
......@@ -79,7 +79,7 @@ Section ucmra_instances.
IsValidOp a a ε Σ True%I | 5.
Proof. apply is_valid_op_comm, _. Qed.
Global Instance has_right_id (a : A) Σ :
Global Instance has_right_id (a : A) :
HasRightId a.
Proof. exists ε. rewrite right_id //. Qed.
End ucmra_instances.
......@@ -705,6 +705,13 @@ Section recursive.
iExists (to_agree o1). iRewrite -"H".
by rewrite agree_idemp.
Qed.
Lemma to_agree_equiv {O : ofe} (o1 o2 : O) : to_agree o1 to_agree o2 o1 o2.
Proof.
intros.
apply to_agree_included.
exists (to_agree o1).
rewrite agree_idemp. by rewrite H.
Qed.
Global Instance auth_frag_valid_op {A : ucmra} (a a1 a2 : A) Σ P :
IsValidOp a a1 a2 Σ P
......
......@@ -105,14 +105,18 @@ Section proof.
increment #l
{{ RET #(); P1 γc q }}.
Global Instance has_right_id {A : ucmra} (a : A) :
HasRightId a.
Proof. exists ε. rewrite right_id //. Qed.
Instance check_rising_spec γc (l : loc) :
SPEC q, {{ P1 γc q inv N (counter_inv γc l) }}
check_rising #l
{{ RET #(); P1 γc q }}.
Proof.
iStepsS.
assert (x8 = x8 `max` x1) by lia. rewrite {2}H1.
iLeft. iStepS. rewrite -H1. iSmash.
assert (x8 = x8 `max` x1) as Hx8 by lia. rewrite {2}Hx8.
iLeft. iStepS. rewrite -Hx8. iSmash.
Qed.
Program Instance decrement_spec γc (l : loc) :
......@@ -126,8 +130,8 @@ Section proof.
{{ RET #(); P2 γc q }}.
Proof.
iStepsS.
assert (x9 = x9 `max` x1) by lia. rewrite {3}H1.
iRight. iStepS. rewrite -H1. iSmash.
assert (x9 = x9 `max` x1) as Hx9 by lia. rewrite {3}Hx9.
iRight. iStepS. rewrite -Hx9. iSmash.
Qed.
Opaque P1 P2.
......@@ -171,13 +175,11 @@ Section proof.
iSplitR; [ | iSplitR; iIntros "!>"; [ | iStepsS]].
- iIntros "!> !>". iStepS.
iInv N as "HN". iRevert "HN".
iStepsS; case: H0 => /= H1 H2; simplify_eq.
apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
iRight. iStepsS.
- iIntros "!> !>". iStepS.
iInv N as "HN". iRevert "HN".
iStepsS; case: H0 => /= H1 H2; simplify_eq.
apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
iSmash.
Unshelve. all: apply inhabitant.
Qed.
......
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