Commit b0ec18bc authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents b2bdf539 3f1a2384
......@@ -276,6 +276,7 @@ Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
Notation "■ φ" := (uPred_const φ%C%type)
(at level 20, right associativity) : uPred_scope.
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
Notation "x ⊥ y" := (uPred_const (x%C%type y%C%type)) : uPred_scope.
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
......
......@@ -16,7 +16,7 @@ Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
Proof. by rewrite -wp_if_true -wp_value. Qed.
Lemma wp_assert' {Σ} (Φ : val iProp heap_lang Σ) e :
WP e {{ λ v, v = #true Φ #() }} WP Assert e {{ Φ }}.
WP e {{ v, v = #true Φ #() }} WP Assert e {{ Φ }}.
Proof.
rewrite /Assert. wp_focus e; apply wp_mono=>v.
apply uPred.const_elim_l=>->. apply wp_assert.
......
......@@ -17,7 +17,7 @@ Section client.
Local Notation iProp := (iPropG heap_lang Σ).
Definition y_inv (q : Qp) (l : loc) : iProp :=
( f : val, l {q} f n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
Lemma y_inv_split q l : y_inv q l (y_inv (q/2) l y_inv (q/2) l).
Proof.
......@@ -27,7 +27,7 @@ Section client.
Lemma worker_safe q (n : Z) (b y : loc) :
(heap_ctx heapN recv heapN N b (y_inv q y))
WP worker n (%b) (%y) {{ λ _, True }}.
WP worker n (%b) (%y) {{ _, True }}.
Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv".
......@@ -36,7 +36,7 @@ Section client.
iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"].
Qed.
Lemma client_safe : heapN N heap_ctx heapN WP client {{ λ _, True }}.
Lemma client_safe : heapN N heap_ctx heapN WP client {{ _, True }}.
Proof.
iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done.
......@@ -61,7 +61,7 @@ Section ClosedProofs.
Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
Proof.
iIntros "! Hσ".
iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
......
......@@ -13,10 +13,10 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma barrier_spec (heapN N : namespace) :
heapN N
recv send : loc iProp -n> iProp,
( P, heap_ctx heapN {{ True }} newbarrier #() {{ λ v,
( P, heap_ctx heapN {{ True }} newbarrier #() {{ v,
l : loc, v = LocV l recv l P send l P }})
( l P, {{ send l P P }} signal (LocV l) {{ λ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }})
( l P, {{ send l P P }} signal (LocV l) {{ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) (recv l P - recv l Q)).
Proof.
......
......@@ -24,10 +24,10 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (l : loc) (R : iProp) : iProp :=
( N γ, (heapN N) heap_ctx heapN inv N (lock_inv γ l R))%I.
( N γ, heapN N heap_ctx heapN inv N (lock_inv γ l R))%I.
Definition locked (l : loc) (R : iProp) : iProp :=
( N γ, (heapN N) heap_ctx heapN
( N γ, heapN N heap_ctx heapN
inv N (lock_inv γ l R) own γ (Excl ()))%I.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
......
......@@ -37,8 +37,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
v, lv = InjRV v (Ψ v own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp) : iProp :=
( (heapN N) γ, heap_ctx heapN own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I.
(heapN N γ, heap_ctx heapN own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I.
Typeclasses Opaque join_handle.
......
......@@ -13,11 +13,11 @@ Implicit Types ef : option (expr []).
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ :
WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
WP e @ E {{ λ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }}
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }}
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
......@@ -81,7 +81,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Φ :
( Φ (LitV LitUnit) WP e {{ λ _, True }}) WP Fork e @ E {{ Φ }}.
( Φ (LitV LitUnit) WP e {{ _, True }}) WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_head_step; eauto.
......
......@@ -2,6 +2,7 @@ From iris.heap_lang Require Export derived.
Export heap_lang.
Arguments wp {_ _} _ _%E _.
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
(at level 20, e, Φ at level 200,
format "'WP' e @ E {{ Φ } }") : uPred_scope.
......@@ -9,6 +10,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
(at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e @ E {{ v , Q } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion App : expr >-> Funclass.
......
......@@ -84,7 +84,7 @@ Qed.
Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
m
(ownP σ1 ownG m) WP e @ E {{ λ v', φ v' }}
(ownP σ1 ownG m) WP e @ E {{ v', φ v' }}
rtc step ([e], σ1) (of_val v :: t2, σ2)
φ v.
Proof.
......@@ -100,7 +100,7 @@ Qed.
Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 :
m
{{ ownP σ1 ownG m }} e @ E {{ λ v', φ v' }}
{{ ownP σ1 ownG m }} e @ E {{ v', φ v' }}
rtc step ([e], σ1) (of_val v :: t2, σ2)
φ v.
Proof.
......
......@@ -14,7 +14,7 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.
Lemma wp_ectx_bind {E e} K Φ :
WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_lift_head_step E1 E2
......
......@@ -19,6 +19,19 @@ Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht P e (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (True ht E P e (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (True ht P e (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : C_scope.
Section hoare.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
......@@ -42,8 +55,7 @@ Proof. solve_proper. Qed.
Lemma ht_alt E P Φ e : (P WP e @ E {{ Φ }}) {{ P }} e @ E {{ Φ }}.
Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
Lemma ht_val E v :
{{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}.
Proof. iIntros "! _". by iApply wp_value'. Qed.
Lemma ht_vs E P P' Φ Φ' e :
......@@ -83,13 +95,13 @@ Proof.
Qed.
Lemma ht_frame_l E P Φ R e :
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ λ v, R Φ v }}.
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ v, R Φ v }}.
Proof.
iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
Qed.
Lemma ht_frame_r E P Φ R e :
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ λ v, Φ v R }}.
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}.
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
......@@ -122,7 +134,7 @@ Qed.
Lemma ht_frame_step_l' E P R e Φ :
to_val e = None
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ λ v, R Φ v }}.
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ v, R Φ v }}.
Proof.
iIntros {?} "#Hwp ! [HR HP]".
iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
......@@ -130,7 +142,7 @@ Qed.
Lemma ht_frame_step_r' E P Φ R e :
to_val e = None
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ λ v, Φ v R }}.
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}.
Proof.
iIntros {?} "#Hwp ! [HP HR]".
iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
......@@ -138,7 +150,7 @@ Qed.
Lemma ht_inv N E P Φ R e :
atomic e nclose N E
(inv N R {{ R P }} e @ E nclose N {{ λ v, R Φ v }})
(inv N R {{ R P }} e @ E nclose N {{ v, R Φ v }})
{{ P }} e @ E {{ Φ }}.
Proof.
iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
......
......@@ -3,14 +3,14 @@ From iris.program_logic Require Export hoare lifting.
From iris.program_logic Require Import ownership.
From iris.proofmode Require Import tactics pviewshifts.
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
(default True%I ef (λ e, ht E P e Φ))
(at level 20, P, ef, Φ at level 200,
format "{{ P } } ef ?@ E {{ Φ } }") : uPred_scope.
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
(True default True ef (λ e, ht E P e Φ))
(at level 20, P, ef, Φ at level 200,
format "{{ P } } ef ?@ E {{ Φ } }") : C_scope.
Local Notation "{{ P } } ef ?@ E {{ v , Q } }" :=
(default True%I ef (λ e, ht E P e (λ v, Q)))
(at level 20, P, ef, Q at level 200,
format "{{ P } } ef ?@ E {{ v , Q } }") : uPred_scope.
Local Notation "{{ P } } ef ?@ E {{ v , Q } }" :=
(True default True ef (λ e, ht E P e (λ v, Q)))
(at level 20, P, ef, Q at level 200,
format "{{ P } } ef ?@ E {{ v , Q } }") : C_scope.
Section lifting.
Context {Λ : language} {Σ : iFunctor}.
......@@ -26,7 +26,7 @@ Lemma ht_lift_step E1 E2
((P ={E1,E2}=> ownP σ1 P')
( e2 σ2 ef, φ e2 σ2 ef ownP σ2 P' ={E2,E1}=> Φ1 e2 σ2 ef Φ2 e2 σ2 ef)
( e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }})
( e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ {{ λ _, True }}))
( e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ {{ _, True }}))
{{ P }} e1 @ E1 {{ Ψ }}.
Proof.
iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
......@@ -45,8 +45,8 @@ Lemma ht_lift_atomic_step
atomic e1
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( e2 σ2 ef, {{ φ e2 σ2 ef P }} ef ?@ {{ λ _, True }})
{{ ownP σ1 P }} e1 @ E {{ λ v, σ2 ef, ownP σ2 φ (of_val v) σ2 ef }}.
( e2 σ2 ef, {{ φ e2 σ2 ef P }} ef ?@ {{ _, True }})
{{ ownP σ1 P }} e1 @ E {{ v, σ2 ef, ownP σ2 φ (of_val v) σ2 ef }}.
Proof.
iIntros {? Hsafe Hstep} "#Hef".
set (φ' e σ ef := is_Some (to_val e) φ e σ ef).
......@@ -68,7 +68,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
(( e2 ef, {{ φ e2 ef P }} e2 @ E {{ Ψ }})
( e2 ef, {{ φ e2 ef P' }} ef ?@ {{ λ _, True }}))
( e2 ef, {{ φ e2 ef P' }} ef ?@ {{ _, True }}))
{{ (P P') }} e1 @ E {{ Ψ }}.
Proof.
iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
......@@ -83,7 +83,7 @@ Lemma ht_lift_pure_det_step
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
({{ P }} e2 @ E {{ Ψ }} {{ P' }} ef ?@ {{ λ _, True }})
({{ P }} e2 @ E {{ Ψ }} {{ P' }} ef ?@ {{ _, True }})
{{ (P P') }} e1 @ E {{ Ψ }}.
Proof.
iIntros {? Hsafe Hdet} "[#He2 #Hef]".
......
......@@ -82,13 +82,13 @@ Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
Lemma wp_inv E e N P Φ R :
atomic e nclose N E
R inv N P
R ( P - WP e @ E nclose N {{ λ v, P Φ v }})
R ( P - WP e @ E nclose N {{ v, P Φ v }})
R WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
atomic e nclose N E
R inv N P
R (P - WP e @ E nclose N {{ λ v, P Φ v }})
R (P - WP e @ E nclose N {{ v, P Φ v }})
R WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
......
......@@ -33,13 +33,13 @@ Arguments pvs {_ _} _ _ _%I.
Instance: Params (@pvs) 4.
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
(at level 199, E1, E2 at level 50, Q at level 200,
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
(at level 199, E at level 50, Q at level 200,
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : uPred_scope.
Notation "|==> Q" := (pvs Q%I)
(at level 199, Q at level 200, format "|==> Q") : uPred_scope.
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
......
......@@ -8,15 +8,30 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
(at level 199, E1,E2 at level 50,
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (True vs E1 E2 P%I Q%I)
(at level 199, E1, E2 at level 50,
Notation "P ={ E1 , E2 }=> Q" := (True (P ={E1,E2}=> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
(at level 199, E at level 50, format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True vs E E P%I Q%I)
(at level 199, E at level 50, format "P ={ E }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True (P ={E}=> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q) (Q ={E2,E1}=> P))%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=> Q") : uPred_scope.
Notation "P <={ E1 , E2 }=> Q" := (True (P <={E1,E2}=> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=> Q") : C_scope.
Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=> Q") : uPred_scope.
Notation "P <={ E }=> Q" := (True (P <={E}=> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=> Q") : C_scope.
Section vs.
Context {Λ : language} {Σ : iFunctor}.
......
......@@ -64,6 +64,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
(at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e @ E {{ v , Q } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
......@@ -141,7 +148,7 @@ Proof.
rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
eapply wp_step_inv with (S k) r'; eauto.
Qed.
Lemma wp_pvs E e Φ : WP e @ E {{ λ v, |={E}=> Φ v }} WP e @ E {{ Φ }}.
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split=> n r; revert e r;
induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
......@@ -155,7 +162,7 @@ Proof.
Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 E1 atomic e
(|={E1,E2}=> WP e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) WP e @ E1 {{ Φ }}.
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) WP e @ E1 {{ Φ }}.
Proof.
rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
eauto using atomic_not_val. intros rf k Ef σ1 ???.
......@@ -172,7 +179,7 @@ Proof.
- by rewrite -assoc.
- constructor; apply pvs_intro; auto.
Qed.
Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} R) WP e @ E {{ λ v, Φ v R }}.
Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} R) WP e @ E {{ v, Φ v R }}.
Proof.
rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
......@@ -192,8 +199,7 @@ Qed.
Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None E E1 E2 E1
(WP e @ E {{ Φ }} |={E1,E2}=> |={E2,E1}=> R)
WP e @ (E E1) {{ λ v, Φ v R }}.
Proof.
WP e @ (E E1) {{ v, Φ v R }}.
rewrite wp_eq pvs_eq=> He ??.
uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
constructor; [done|]=>rf k Ef σ1 ?? Hws1.
......@@ -222,7 +228,7 @@ Proof.
eapply (Hmask E); by auto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
WP e @ E {{ λ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split=> n r; revert e r;
induction n as [n IH] using lt_wf_ind=> e r ?.
......@@ -254,10 +260,10 @@ Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_value_pvs E Φ e v :
to_val e = Some v (|={E}=> Φ v) WP e @ E {{ Φ }}.
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : (R WP e @ E {{ Φ }}) WP e @ E {{ λ v, R Φ v }}.
Lemma wp_frame_l E e Φ R : (R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Lemma wp_frame_step_r' E e Φ R :
to_val e = None (WP e @ E {{ Φ }} R) WP e @ E {{ λ v, Φ v R }}.
to_val e = None (WP e @ E {{ Φ }} R) WP e @ E {{ v, Φ v R }}.
Proof.
intros. rewrite {2}(_ : E = E ); last by set_solver.
rewrite -(wp_frame_step_r E ); [|auto|set_solver..].
......@@ -266,22 +272,22 @@ Qed.
Lemma wp_frame_step_l E E1 E2 e Φ R :
to_val e = None E E1 E2 E1
((|={E1,E2}=> |={E2,E1}=> R) WP e @ E {{ Φ }})
WP e @ (E E1) {{ λ v, R Φ v }}.
WP e @ (E E1) {{ v, R Φ v }}.
Proof.
rewrite [((|={E1,E2}=> _) _)%I]comm; setoid_rewrite (comm _ R).
apply wp_frame_step_r.
Qed.
Lemma wp_frame_step_l' E e Φ R :
to_val e = None ( R WP e @ E {{ Φ }}) WP e @ E {{ λ v, R Φ v }}.
to_val e = None ( R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
Proof.
rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
apply wp_frame_step_r'.
Qed.
Lemma wp_always_l E e Φ R `{!PersistentP R} :
(R WP e @ E {{ Φ }}) WP e @ E {{ λ v, R Φ v }}.
(R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
Lemma wp_always_r E e Φ R `{!PersistentP R} :
(WP e @ E {{ Φ }} R) WP e @ E {{ λ v, Φ v R }}.
(WP e @ E {{ Φ }} R) WP e @ E {{ v, Φ v R }}.
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma wp_wand_l E e Φ Ψ :
(( v, Φ v - Ψ v) WP e @ E {{ Φ }}) WP e @ E {{ Ψ }}.
......
......@@ -7,21 +7,21 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "​" := Enil (format "​") : proof_scope.
Notation "Γ ​ H : P" := (Esnoc Γ H P)
Notation "​ Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format "Γ ​ '//' H : P") : proof_scope.
left associativity, format "​ Γ H : P '//'") : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
(of_envs (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '//' '--------------------------------------' □ Δ '//' '--------------------------------------' ★ '//' Q '//'") :
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
C_scope.
Notation "Δ '--------------------------------------' ★ Q" :=
(of_envs (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Δ '//' '--------------------------------------' ★ '//' Q '//'") : C_scope.
format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(of_envs (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '//' '--------------------------------------' □ '//' Q '//'") : C_scope.
format "Γ '--------------------------------------' □ '//' Q '//'") : C_scope.
Notation "​​ Q" := (of_envs (Envs Enil Enil) Q%I)
(at level 1, format "​​ Q") : C_scope.
(at level 1, Q at level 200, format "​​ Q") : C_scope.
......@@ -24,7 +24,7 @@ Section LiftingTests.
Definition heap_e : expr [] :=
let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
Lemma heap_e_spec E N :
nclose N E heap_ctx N WP heap_e @ E {{ λ v, v = #2 }}.
nclose N E heap_ctx N WP heap_e @ E {{ v, v = #2 }}.
Proof.
iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
......@@ -58,7 +58,7 @@ Section LiftingTests.
Qed.
Lemma Pred_user E :
(True : iProp) WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
(True : iProp) WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ v, v = #40 }}.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
End LiftingTests.
......@@ -66,7 +66,7 @@ Section ClosedProofs.
Definition Σ : gFunctors := #[ heapGF ].
Notation iProp := (iPropG heap_lang Σ).
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
Proof.
iProof. iIntros "! Hσ".
iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
......
......@@ -19,8 +19,8 @@ Definition barrier_res γ (Φ : X → iProp) : iProp :=
( x, one_shot_own γ x Φ x)%I.
Lemma worker_spec e γ l (Φ Ψ : X iProp) :
(recv heapN N l (barrier_res γ Φ) x, {{ Φ x }} e {{ λ _, Ψ x }})
WP wait (%l) ;; e {{ λ _, barrier_res γ Ψ }}.
(recv heapN N l (barrier_res γ Φ) x, {{ Φ x }} e {{ _, Ψ x }})
WP wait (%l) ;; e {{ _, barrier_res γ Ψ }}.
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
......@@ -50,10 +50,10 @@ Qed.
Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
heapN N eM' = wexpr' eM eW1' = wexpr' eW1 eW2' = wexpr' eW2
(heap_ctx heapN P
{{ P }} eM {{ λ _, x, Φ x }}
( x, {{ Φ1 x }} eW1 {{ λ _, Ψ1 x }})
( x, {{ Φ2 x }} eW2 {{ λ _, Ψ2 x }}))
WP client eM' eW1' eW2' {{ λ _, γ, barrier_res γ Ψ }}.
{{ P }} eM {{ _, x, Φ x }}
( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}))
WP client eM' eW1' eW2' {{ _, γ, barrier_res γ Ψ }}.
Proof.
iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
iPvs one_shot_alloc as {γ} "Hγ".
......
......@@ -37,8 +37,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
Lemma wp_one_shot (Φ : val iProp) :
(heap_ctx heapN f1 f2 : val,
( n : Z, WP f1 #n {{ λ w, w = #true w = #false }})
WP f2 #() {{ λ g, WP g #() {{ λ _, True }} }} - Φ (f1,f2)%V)
( n : Z, WP f1 #n {{ w, w = #true w = #false }})
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "[#? Hf] /=".
......@@ -83,9 +83,9 @@ Qed.
Lemma hoare_one_shot (Φ : val iProp) :
heap_ctx heapN {{ True }} one_shot_example #()
{{ λ ff,
( n : Z, {{ True }} Fst ff #n {{ λ w, w = #true w = #false }})
{{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }}
{{ ff,
( n : Z, {{ True }} Fst ff #n {{ w, w = #true w = #false }})
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
}}.
Proof.
iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
......
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