Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing (Artifact)

From dlfactris.base_logic Require Import proofmode.
From dlfactris.lang Require Import notation.

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.
Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.

Lemma wp_assert (Φ : val → aProp) e :
  WP e {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
  WP (assert: e)%V {{ Φ }}.
Proof.
  iIntros "HΦ". wp_rec. iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst.
  by wp_pures.
Qed.