Skip to content

GitLab

Commit f2a18f5a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Typeclass to overload WP notation.

parent 83a8c02a
Hide whitespace changes
Inline Side-by-side
Showing with 260 additions and 270 deletions
_CoqProject
View file @ f2a18f5a
......@@ -38,6 +38,7 @@ theories/bi/bi.v
theories/bi/tactics.v
theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/lib/counter_examples.v
theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
......
tests/heap_lang.ref
View file @ f2a18f5a
......@@ -35,7 +35,7 @@
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ
Φ : language.val heap_lang → iPropI Σ
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
......@@ -48,7 +48,7 @@
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ
Φ : language.val heap_lang → iPropI Σ
E : coPset
============================
--------------------------------------∗
......
theories/bi/weakestpre.v 0 → 100644
View file @ f2a18f5a
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
View file @ f2a18f5a
......@@ -50,142 +50,13 @@ Qed.
Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
(e : expr Λ) (Φ : val Λ → iProp Σ) :
iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
Definition twp_aux : seal (@twp_def). by eexists. Qed.
Definition twp := twp_aux.(unseal).
Definition twp_eq : @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.
Definition twp_aux `{irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
Instance twp' `{irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
Definition twp_eq `{irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
Section twp.
Context `{irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ.
......@@ -210,12 +81,12 @@ Proof.
Qed.
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.
intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
Global Instance twp_proper s E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@twp Λ Σ _ s E e).
Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
Qed.
......@@ -339,7 +210,7 @@ Lemma twp_mask_mono s E1 E2 e Φ :
E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
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.
Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
......
theories/program_logic/weakestpre.v
View file @ f2a18f5a
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
From iris.bi Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type".
Import uPred.
......@@ -11,20 +12,6 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
Notation irisG Λ Σ := (irisG' (state Λ) Σ).
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)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
......@@ -45,119 +32,9 @@ Qed.
Definition wp_def `{irisG Λ Σ} (s : stuckness) :
coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def). by eexists. Qed.
Definition wp := wp_aux.(unseal).
Definition wp_eq : @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 } } }" :=