Guarantees by Construction (Mechanization)

Jules Jacobs

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
From dlfactris.lang Require Export notation.
From dlfactris.base_logic Require Export proofmode.

Module Sub.
  Notation prot := aMiniProt.
  Notation dual := dual.

  Definition fork_chan : val := λ: "f", ForkChan "f".
  Definition recv : val := λ: "c", Recv "c".
  Definition send : val := λ: "c" "x", Send "c" "x".

  Definition subprot (p1 p2 : aMiniProt) : aProp :=                              (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=37b2ff6b *)
    match prot_action p1, prot_action p2 with
    | ASend, ASend => ∀ v, p2 v -∗ p1 v
    | ARecv, ARecv => ∀ v, p1 v -∗ p2 v
    | _, _ => False
    end.

  Definition own_chan (c : val) (p : prot) : aProp :=
    ∃ (l : loc) p', ⌜⌜ c = #l ⌝⌝ ∗ ▷ subprot p' p ∗ own_chan l p'.
  Global Instance: Params (@own_chan) 1 := {}.

  Global Instance subprot_ne : NonExpansive2 subprot.
  Proof.
    intros ? [??] [??] [??] [??] [??] [??]; simplify_eq/=.
    rewrite /subprot /=. by repeat f_equiv.
  Qed.
  Global Instance subprot_proper : Proper ((≡) ==> (≡) ==> (≡)) subprot.
  Proof. apply ne_proper_2, _. Qed.

  Global Instance own_chan_contractive c : Contractive (own_chan c).
  Proof. solve_contractive. Qed.
  Global Instance own_chan_ne c : NonExpansive (own_chan c).
  Proof. solve_proper. Qed.
  Global Instance own_chan_proper c : Proper ((≡) ==> (≡)) (own_chan c).
  Proof. solve_proper. Qed.

  Module Import notations.
    Notation "p ⊑ q" := (subprot p q) : bi_scope.
    Notation "c ↣ p" := (own_chan c p) : bi_scope.
  End notations.

  Lemma subprot_refl p : ⊢ p ⊑ p.
  Proof. destruct p as [[] Φ]; rewrite /subprot //=; auto. Qed.

  Lemma subprot_dual p1 p2 : dual p1 ⊑ dual p2 ⊣⊢ p2 ⊑ p1.
  Proof. destruct p1 as [[]], p2 as [[]]; auto. Qed.

  Lemma subprot_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
  Proof.
    iIntros "Hsp1 Hsp2".
    destruct p1 as [[] P1], p2 as [[] P2], p3 as [[] P3];
      rewrite /subprot //=; iIntros (v) "H //";
      by do 2 (iApply "Hsp1" || iApply "Hsp2").
  Qed.

  Lemma own_chan_subprot c p p' : c ↣ p -∗ ▷ (p ⊑ p') -∗ c ↣ p'.
  Proof.
    iIntros "(%l & %p'' & -> & Hsp' & Hc) Hsp".
    iExists l, p''. iSplit; [done|]. iFrame. by iApply (subprot_trans with "Hsp'").
  Qed.

  Local Lemma own_chan_from_base l p : aprop.own_chan l p ⊢ #l ↣ p.
  Proof.
    iIntros "Hown". iExists l, p. iSplit; [done|]. iFrame. iApply subprot_refl.
  Qed.

  (** WP's for own_chan_sub *)

  Lemma wp_fork_chan p (f : val) :
    ▷ (∀ c, c ↣ dual p -∗ WP f c {{ _, emp }}) -∗
    WP fork_chan f {{ c, c ↣ p }}.
  Proof.
    iIntros "Hf". wp_rec. iApply (wp_fork with "[Hf]"); iIntros "!>" (l) "Hown".
    - iApply "Hf". by iApply own_chan_from_base.
    - by iApply own_chan_from_base.
  Qed.

  Lemma wp_recv c Φ : c ↣ MiniProt ARecv Φ -∗ WP recv c {{ Φ }}.
  Proof.
    iIntros "(%l & %p' & -> & Hsp & Hc)". wp_rec.
    destruct p' as [[] Ψ]; rewrite /subprot //=.
    by iApply (wp_recv with "Hc").
  Qed.

  Lemma wp_send c v Φ :
    c ↣ MiniProt ASend Φ -∗ ▷ Φ v -∗
    WP send c v {{ v, ⌜⌜ v = #() ⌝⌝ }}.
  Proof.
    iIntros "(%l & %p' & -> & Hsp & Hc) HΦ". wp_rec.
    destruct p' as [[] Ψ]; rewrite /subprot //=.
    iApply (wp_send with "[$]"). by iApply "Hsp".
  Qed.

  Global Opaque fork_chan send recv own_chan.
  Global Typeclasses Opaque subprot.
End Sub.