assert.v 605 Bytes
Newer Older
1
2
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
3

4
5
6
7
8
Definition assert : val :=
  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Global Opaque assert.
9

10
11
Lemma wp_assert {Σ} E (Φ : val  iProp heap_lang Σ) e `{!Closed [] e} :
  WP e @ E {{ v, v = #true   Φ #() }}  WP assert: e @ E {{ Φ }}.
12
Proof.
13
14
15
  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
  iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
  wp_if. done.
16
Qed.