Commit 64bb0481 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Stronger masks for the WP of assert.

parent a709fc36
...@@ -7,8 +7,8 @@ Definition assert : val := ...@@ -7,8 +7,8 @@ Definition assert : val :=
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. Global Opaque assert.
Lemma wp_assert {Σ} (Φ : val iProp heap_lang Σ) e `{!Closed [] e} : Lemma wp_assert {Σ} E (Φ : val iProp heap_lang Σ) e `{!Closed [] e} :
WP e {{ v, v = #true Φ #() }} WP assert: e {{ Φ }}. WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof. Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq. iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst. iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
......
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