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

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

(** This file includes a specification [cmp_spec] for comparing values based on
a given interpretation [I], a relation [R] that matches up with a HeapLang
implementation [cmp]. The file also provides an instance for the [≤] relation
on integers [Z].*)
From dlfactris.lang Require Import notation.
From dlfactris.session_logic Require Import proofmode.

Definition cmp_spec {A} (I : A  val  aProp)
    (R : relation A) `{!RelDecision R} (cmp : val) : aProp :=
   (∀ x x' v v',
      I x v - I x' v' -
      WP cmp v v'
      {{ w, ⌜⌜ w = #(bool_decide (R x x')) ⌝⌝  I x v  I x' v' }})%I.

Definition IZ (x : Z) (v : val) : aProp := ⌜⌜ v = #x ⌝⌝%I.
Definition cmpZ : val := λ: "x" "y", "x"  "y".

Lemma cmpZ_spec :  cmp_spec IZ (≤)%Z cmpZ.
Proof. rewrite /IZ. iIntros "!>" (x x' v v' -> ->). by wp_rec!. Qed.