Commit f8e2c74c authored by Ralf Jung's avatar Ralf Jung

compatibility with coq 8.6

parent 3a20cb6a
...@@ -7,7 +7,6 @@ Definition assert : val := ...@@ -7,7 +7,6 @@ Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *) λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *) (* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope. Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Global Opaque assert.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} : Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}. WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
...@@ -15,3 +14,5 @@ Proof. ...@@ -15,3 +14,5 @@ Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq. iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if. iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed. Qed.
Global Opaque assert.
...@@ -22,6 +22,8 @@ Section proof. ...@@ -22,6 +22,8 @@ Section proof.
Context `{!heapG Σ, !barrierG Σ} (N : namespace). Context `{!heapG Σ, !barrierG Σ} (N : namespace).
Implicit Types I : gset gname. Implicit Types I : gset gname.
Local Transparent newbarrier signal wait.
Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ := Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
( Ψ : gname iProp Σ, ( Ψ : gname iProp Σ,
(P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I. (P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I.
......
...@@ -10,7 +10,6 @@ Definition incr : val := ...@@ -10,7 +10,6 @@ Definition incr : val :=
let: "n" := !"l" in let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l". Definition read : val := λ: "l", !"l".
Global Opaque newcounter incr get.
(** Monotone counter *) (** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }. Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
...@@ -167,3 +166,5 @@ Section contrib_spec. ...@@ -167,3 +166,5 @@ Section contrib_spec.
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
End contrib_spec. End contrib_spec.
Global Opaque newcounter incr get.
...@@ -11,7 +11,6 @@ Definition par : val := ...@@ -11,7 +11,6 @@ Definition par : val :=
let: "v1" := join "handle" in let: "v1" := join "handle" in
("v1", "v2"). ("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Global Opaque par.
Section proof. Section proof.
Context `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ}.
...@@ -45,3 +44,5 @@ Proof. ...@@ -45,3 +44,5 @@ Proof.
iSplitL "H1"; by wp_let. iSplitL "H1"; by wp_let.
Qed. Qed.
End proof. End proof.
Global Opaque par.
...@@ -14,7 +14,6 @@ Definition join : val := ...@@ -14,7 +14,6 @@ Definition join : val :=
SOME "x" => "x" SOME "x" => "x"
| NONE => "join" "c" | NONE => "join" "c"
end. end.
Global Opaque spawn join.
(** The CMRA & functor we need. *) (** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
...@@ -79,3 +78,4 @@ Qed. ...@@ -79,3 +78,4 @@ Qed.
End proof. End proof.
Typeclasses Opaque join_handle. Typeclasses Opaque join_handle.
Global Opaque spawn join.
...@@ -10,7 +10,6 @@ Definition try_acquire : val := λ: "l", CAS "l" #false #true. ...@@ -10,7 +10,6 @@ Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val := Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l". rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false. Definition release : val := λ: "l", "l" <- #false.
Global Opaque newlock try_acquire acquire release.
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
...@@ -89,6 +88,9 @@ Section proof. ...@@ -89,6 +88,9 @@ Section proof.
Qed. Qed.
End proof. End proof.
Typeclasses Opaque is_lock locked.
Global Opaque newlock try_acquire acquire release.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ := Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec; {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}. lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
...@@ -25,8 +25,6 @@ Definition acquire : val := ...@@ -25,8 +25,6 @@ Definition acquire : val :=
Definition release : val := λ: "lk", Definition release : val := λ: "lk",
(Fst "lk") <- !(Fst "lk") + #1. (Fst "lk") <- !(Fst "lk") + #1.
Global Opaque newlock acquire release wait_loop.
(** The CMRAs we need. *) (** The CMRAs we need. *)
Class tlockG Σ := Class tlockG Σ :=
tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))). tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
...@@ -170,6 +168,7 @@ Section proof. ...@@ -170,6 +168,7 @@ Section proof.
End proof. End proof.
Typeclasses Opaque is_lock issued locked. Typeclasses Opaque is_lock issued locked.
Global Opaque newlock acquire release wait_loop.
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ := Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec; {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
......
...@@ -11,7 +11,6 @@ Definition client : expr := ...@@ -11,7 +11,6 @@ Definition client : expr :=
let: "b" := newbarrier #() in let: "b" := newbarrier #() in
("y" <- (λ: "z", "z" + #42) ;; signal "b") ||| ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
(worker 12 "b" "y" ||| worker 17 "b" "y"). (worker 12 "b" "y" ||| worker 17 "b" "y").
Global Opaque worker client.
Section client. Section client.
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace). Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
...@@ -55,6 +54,8 @@ Section client. ...@@ -55,6 +54,8 @@ Section client.
Qed. Qed.
End client. End client.
Global Opaque worker client.
Section ClosedProofs. Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ]. Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
......
...@@ -16,7 +16,6 @@ Definition incr : val := ...@@ -16,7 +16,6 @@ Definition incr : val :=
let: "n" := !"l" in let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l". Definition read : val := λ: "l", !"l".
Global Opaque newcounter incr read.
(** The CMRA we need. *) (** The CMRA we need. *)
Inductive M := Auth : nat M | Frag : nat M | Bot. Inductive M := Auth : nat M | Frag : nat M | Bot.
...@@ -137,3 +136,5 @@ Proof. ...@@ -137,3 +136,5 @@ Proof.
iModIntro; rewrite /C; eauto 10 with omega. iModIntro; rewrite /C; eauto 10 with omega.
Qed. Qed.
End proof. End proof.
Global Opaque newcounter incr read.
...@@ -21,7 +21,6 @@ Proof. apply subG_inG. Qed. ...@@ -21,7 +21,6 @@ Proof. apply subG_inG. Qed.
Definition client eM eW1 eW2 : expr := Definition client eM eW1 eW2 : expr :=
let: "b" := newbarrier #() in let: "b" := newbarrier #() in
(eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)). (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
Global Opaque client.
Section proof. Section proof.
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}. Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
...@@ -98,3 +97,5 @@ Proof. ...@@ -98,3 +97,5 @@ Proof.
- iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto. - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
Qed. Qed.
End proof. End proof.
Global Opaque client.
...@@ -18,7 +18,6 @@ Definition one_shot_example : val := λ: <>, ...@@ -18,7 +18,6 @@ Definition one_shot_example : val := λ: <>,
| SOME "m" => assert: "n" = "m" | SOME "m" => assert: "n" = "m"
end end
end)). end)).
Global Opaque one_shot_example.
Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z). Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR). Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
...@@ -97,3 +96,5 @@ Proof. ...@@ -97,3 +96,5 @@ Proof.
iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _". iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed. Qed.
End proof. End proof.
Global Opaque one_shot_example.
...@@ -33,8 +33,6 @@ Definition sum' : val := λ: "t", ...@@ -33,8 +33,6 @@ Definition sum' : val := λ: "t",
sum_loop "t" "l";; sum_loop "t" "l";;
!"l". !"l".
Global Opaque sum_loop sum'.
Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val iProp Σ) : Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val iProp Σ) :
heap_ctx l #n is_tree v t heap_ctx l #n is_tree v t
(l #(sum t + n) - is_tree v t - Φ #()) (l #(sum t + n) - is_tree v t - Φ #())
...@@ -66,3 +64,6 @@ Proof. ...@@ -66,3 +64,6 @@ Proof.
rewrite Z.add_0_r. rewrite Z.add_0_r.
iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ". iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
Qed. Qed.
Global Opaque sum_loop sum'.
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