assert.v 687 Bytes
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
3 4
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
5

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

11
Lemma wp_assert `{heapG Σ} E (Φ : val  iProp Σ) e `{!Closed [] e} :
Ralf Jung's avatar
Ralf Jung committed
12
  WP e @ E {{ v, v = #true   Φ #() }}  WP assert: e @ E {{ Φ }}.
13
Proof.
14
  iIntros "HΦ". rewrite /assert -lock. wp_let. wp_seq.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
16
Qed.