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

Merge branch 'ci/robbert/overloaded_wp' into 'gen_proofmode' 

Typeclass to overload WP notation.

See merge request FP/iris-coq!146
parents 83a8c02a f2a18f5a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 1
− 0
View file @ e67181e6
...@@ -38,6 +38,7 @@ theories/bi/bi.v ...@@ -38,6 +38,7 @@ theories/bi/bi.v
theories/bi/tactics.v theories/bi/tactics.v
theories/bi/monpred.v theories/bi/monpred.v
theories/bi/embedding.v theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/lib/counter_examples.v theories/bi/lib/counter_examples.v
theories/bi/lib/fixpoint.v theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v theories/bi/lib/fractional.v
......
tests/heap_lang.ref
+ 2
− 2
View file @ e67181e6
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
Σ : gFunctors Σ : gFunctors
H : heapG Σ H : heapG Σ
fun1, fun2, fun3 : expr fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iPropI Σ
============================ ============================
--------------------------------------∗ --------------------------------------∗
WP let: "val1" := fun1 #() in WP let: "val1" := fun1 #() in
...@@ -48,7 +48,7 @@ ...@@ -48,7 +48,7 @@
Σ : gFunctors Σ : gFunctors
H : heapG Σ H : heapG Σ
fun1, fun2, fun3 : expr fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iPropI Σ
E : coPset E : coPset
============================ ============================
--------------------------------------∗ --------------------------------------∗
......
theories/bi/weakestpre.v 0 → 100644
+ 241
− 0
View file @ e67181e6
From stdpp Require Export coPset.
From iris.program_logic Require Import language.
From iris.bi Require Import interface derived_connectives.
Inductive stuckness := NotStuck | MaybeStuck.
Definition stuckness_leb (s1 s2 : stuckness) : bool :=
match s1, s2 with
| MaybeStuck, NotStuck => false
| _, _ => true
end.
Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Instance stuckness_le_po : PreOrder stuckness_le.
Proof. split; by repeat intros []. Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
(** Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
class. This argument can be used for e.g. the stuckness bit (as in Iris) or
thread IDs (as in iGPS).
For the case of stuckness bits, there are two specific notations
[WP e @ E {{ Φ }}] and [WP e @ E ?{{ Φ }}], which forces [A] to be [stuckness],
and [s] to be [NotStuck] or [MaybeStuck]. *)
Class Wp (Λ : language) (PROP A : Type) :=
wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
Arguments wp {_ _ _ _} _ _ _%E _%I.
Instance: Params (@wp) 7.
Class Twp (Λ : language) (PROP A : Type) :=
twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
Arguments twp {_ _ _ _} _ _ _%E _%I.
Instance: Params (@twp) 7.
(** Notations for partial weakest preconditions *)
(** Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
(** Notations with binder. The indentation for the inner format block is chosen
such that *if* one has a single-character mask (e.g. [E]), the second line
should align with the binder(s) on the first line. *)
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ s ; E {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E ? {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' ? {{ v , Q } } ']' ']'") : bi_scope.
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ RET pat ; Q } } } ']'") : bi_scope.
(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
(** Notations for total weakest preconditions *)
(** Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
(** Notations with binder. The indentation for the inner format block is chosen
such that *if* one has a single-character mask (e.g. [E]), the second line
should align with the binder(s) on the first line. *)
Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ s ; E [{ v , Q } ] ']' ']'") : bi_scope.
Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E [{ v , Q } ] ']' ']'") : bi_scope.
Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E ? [{ v , Q } ] ']' ']'") : bi_scope.
Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' [{ v , Q } ] ']' ']'") : bi_scope.
Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' ? [{ v , Q } ] ']' ']'") : bi_scope.
(* Texan triples *)
Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ s ; E [[{ x .. y , RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ E [[{ x .. y , RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ E ? [[{ x .. y , RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "'[hv' [[{ P } ] ] '/ ' e '/' [[{ x .. y , RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "'[hv' [[{ P } ] ] '/ ' e '/' ? [[{ x .. y , RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
(at level 20,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ s ; E [[{ RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
(at level 20,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ E [[{ RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
(at level 20,
format "'[hv' [[{ P } ] ] '/ ' e '/' @ E ? [[{ RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
(at level 20,
format "'[hv' [[{ P } ] ] '/ ' e '/' [[{ RET pat ; Q } ] ] ']'") : bi_scope.
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
(at level 20,
format "'[hv' [[{ P } ] ] '/ ' e '/' ? [[{ RET pat ; Q } ] ] ']'") : bi_scope.
(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }]) : stdpp_scope.
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }]) : stdpp_scope.
theories/program_logic/total_weakestpre.v
+ 7
− 136
View file @ e67181e6
...@@ -50,142 +50,13 @@ Qed. ...@@ -50,142 +50,13 @@ Qed.
Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset) Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
(e : expr Λ) (Φ : val Λ → iProp Σ) : (e : expr Λ) (Φ : val Λ → iProp Σ) :
iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ). iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
Definition twp_aux : seal (@twp_def). by eexists. Qed. Definition twp_aux `{irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
Definition twp := twp_aux.(unseal). Instance twp' `{irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
Definition twp_eq : @twp = @twp_def := twp_aux.(seal_eq). Definition twp_eq `{irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
Arguments twp {_ _ _} _ _ _%E _.
Instance: Params (@twp) 6.
(* Note that using '[[' instead of '[{' results in conflicts with the list
notations. *)
Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ s ; E [{ Φ } ] ']'") : bi_scope.
Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E [{ Φ } ] ']'") : bi_scope.
Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E ? [{ Φ } ] ']'") : bi_scope.
Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' [{ Φ } ] ']'") : bi_scope.
Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' ? [{ Φ } ] ']'") : bi_scope.
Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ s ; E [{ v , Q } ] ']'") : bi_scope.
Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ E [{ v , Q } ] ']'") : bi_scope.
Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ E ? [{ v , Q } ] ']'") : bi_scope.
Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' [{ v , Q } ] ']'") : bi_scope.
Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' ? [{ v , Q } ] ']'") : bi_scope.
(* Texan triples *)
Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ s ; E [[{ x .. y , RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ E [[{ x .. y , RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ E ? [[{ x .. y , RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e [[{ x .. y , RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e ? [[{ x .. y , RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
(at level 20,
format "[[{ P } ] ] e @ s ; E [[{ RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
(at level 20,
format "[[{ P } ] ] e @ E [[{ RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
(at level 20,
format "[[{ P } ] ] e @ E ? [[{ RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
(at level 20,
format "[[{ P } ] ] e [[{ RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
(□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
(at level 20,
format "[[{ P } ] ] e ? [[{ RET pat ; Q } ] ]") : bi_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ s ; E [[{ x .. y , RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ E [[{ x .. y , RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e @ E ? [[{ x .. y , RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e [[{ x .. y , RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _,
P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])
(at level 20, x closed binder, y closed binder,
format "[[{ P } ] ] e ? [[{ x .. y , RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])
(at level 20,
format "[[{ P } ] ] e @ s ; E [[{ RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])
(at level 20,
format "[[{ P } ] ] e @ E [[{ RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])
(at level 20,
format "[[{ P } ] ] e @ E ? [[{ RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])
(at level 20,
format "[[{ P } ] ] e [[{ RET pat ; Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
(∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])
(at level 20,
format "[[{ P } ] ] e ? [[{ RET pat ; Q } ] ]") : stdpp_scope.
Section twp. Section twp.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ. Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ. Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ. Implicit Types v : val Λ.
...@@ -210,12 +81,12 @@ Proof. ...@@ -210,12 +81,12 @@ Proof.
Qed. Qed.
Global Instance twp_ne s E e n : Global Instance twp_ne s E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@twp Λ Σ _ s E e). Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
Proof. Proof.
intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ. intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed. Qed.
Global Instance twp_proper s E e : Global Instance twp_proper s E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@twp Λ Σ _ s E e). Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
Proof. Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist. by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
Qed. Qed.
...@@ -339,7 +210,7 @@ Lemma twp_mask_mono s E1 E2 e Φ : ...@@ -339,7 +210,7 @@ Lemma twp_mask_mono s E1 E2 e Φ :
E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }]. E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed. Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
Global Instance twp_mono' s E e : Global Instance twp_mono' s E e :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (@twp Λ Σ _ s E e). Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
Proof. by intros Φ Φ' ?; apply twp_mono. Qed. Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }]. Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
......
theories/program_logic/weakestpre.v
+ 9
− 132
View file @ e67181e6
From iris.base_logic.lib Require Export fancy_updates. From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language. From iris.program_logic Require Export language.
From iris.bi Require Export weakestpre.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
...@@ -11,20 +12,6 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG { ...@@ -11,20 +12,6 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
Notation irisG Λ Σ := (irisG' (state Λ) Σ). Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Global Opaque iris_invG. Global Opaque iris_invG.
Inductive stuckness := NotStuck | MaybeStuck.
Definition stuckness_leb (s1 s2 : stuckness) : bool :=
match s1, s2 with
| MaybeStuck, NotStuck => false
| _, _ => true
end.
Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Instance stuckness_le_po : PreOrder stuckness_le.
Proof. split; by repeat intros []. Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
Definition wp_pre `{irisG Λ Σ} (s : stuckness) Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) : (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
...@@ -45,119 +32,9 @@ Qed. ...@@ -45,119 +32,9 @@ Qed.
Definition wp_def `{irisG Λ Σ} (s : stuckness) : Definition wp_def `{irisG Λ Σ} (s : stuckness) :
coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s). coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def). by eexists. Qed. Definition wp_aux `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
Definition wp := wp_aux.(unseal). Instance wp' `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
Definition wp_eq : @wp = @wp_def := wp_aux.(seal_eq). Definition wp_eq `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
Arguments wp {_ _ _} _ _ _%E _.
Instance: Params (@wp) 6.
(* Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
(* Notations with binder. The indentation for the inner format block is chosen
such that *if* one has a single-character mask (e.g. [E]), the second line
should align with the binder(s) on the first line. *)
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ s ; E {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' @ E ? {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' ? {{ v , Q } } ']' ']'") : bi_scope.
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ RET pat ; Q } } } ']'") : bi_scope.
(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
Section wp. Section wp.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ}.
...@@ -168,11 +45,12 @@ Implicit Types v : val Λ. ...@@ -168,11 +45,12 @@ Implicit Types v : val Λ.
Implicit Types e : expr Λ. Implicit Types e : expr Λ.
(* Weakest pre *) (* Weakest pre *)
Lemma wp_unfold s E e Φ : WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp s) E e Φ. Lemma wp_unfold s E e Φ :
WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed. Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
Global Instance wp_ne s E e n : Global Instance wp_ne s E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ s E e). Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
Proof. Proof.
revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ. revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
rewrite !wp_unfold /wp_pre. rewrite !wp_unfold /wp_pre.
...@@ -183,7 +61,7 @@ Proof. ...@@ -183,7 +61,7 @@ Proof.
intros v. eapply dist_le; eauto with omega. intros v. eapply dist_le; eauto with omega.
Qed. Qed.
Global Instance wp_proper s E e : Global Instance wp_proper s E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ s E e). Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
Proof. Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist. by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed. Qed.
...@@ -294,7 +172,7 @@ Proof. apply wp_stuck_mono. by destruct s. Qed. ...@@ -294,7 +172,7 @@ Proof. apply wp_stuck_mono. by destruct s. Qed.
Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}. Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed. Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
Global Instance wp_mono' s E e : Global Instance wp_mono' s E e :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e). Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp (PROP:=iProp Σ) s E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed. Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}. Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}.
...@@ -411,5 +289,4 @@ Section proofmode_classes. ...@@ -411,5 +289,4 @@ Section proofmode_classes.
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner". iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose". iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Qed. Qed.
End proofmode_classes. End proofmode_classes.
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