translation.v 7.33 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1
2
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.algebra Require Import frac auth.
Léon Gondelman's avatar
Léon Gondelman committed
4
From iris.base_logic.lib Require Import fractional.
Dan Frumin's avatar
Dan Frumin committed
5
From iris_c.lib Require Import locking_heap mset flock U.
Dan Frumin's avatar
Dan Frumin committed
6
From iris_c.c_translation Require Import monad lifting proofmode.
Léon Gondelman's avatar
Léon Gondelman committed
7

Dan Frumin's avatar
Dan Frumin committed
8
9
Definition a_alloc : val := λ: "x",
  a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
Léon Gondelman's avatar
Léon Gondelman committed
10
11
12
13

Definition a_store : val := λ: "x1" "x2",
  a_bind (λ: "vv",
    a_atomic_env (λ: "env",
Dan Frumin's avatar
Dan Frumin committed
14
      mset_add (Fst "vv") "env" ;;
Léon Gondelman's avatar
Léon Gondelman committed
15
16
17
18
19
20
21
22
      Fst "vv" <- Snd "vv" ;;
      Snd "vv"
    )
  ) (a_par "x1" "x2").

Definition a_load : val := λ: "x",
  a_bind (λ: "v",
    a_atomic_env (λ: "env",
Dan Frumin's avatar
Dan Frumin committed
23
      assert: (mset_member "v" "env" = #false);;
Léon Gondelman's avatar
Léon Gondelman committed
24
25
26
27
28
      !"v"
    )
  ) "x".

Definition a_un_op (op : un_op) : val := λ: "x",
29
  a_bind (λ: "v", a_ret (λ: <>, UnOp op "v")) "x".
Léon Gondelman's avatar
Léon Gondelman committed
30
31
32

Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
  a_bind (λ: "vv",
33
    a_ret (BinOp op (Fst "vv") (Snd "vv"))
Léon Gondelman's avatar
Léon Gondelman committed
34
35
36
37
38
  ) (a_par "x1" "x2").

(* M () *)
(* The eta expansion is used to turn it into a value *)
Definition a_seq : val := λ: "env",
39
  a_atomic_env (λ: "env", mset_clear "env") "env".
Dan Frumin's avatar
Dan Frumin committed
40

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
Definition a_sequence : val := λ: "e1" "e2",
  a_bind (λ: <>,
    a_bind (λ: <>, (a_bind (λ: "v", a_ret "v") "e2")) a_seq
  ) "e1".

Definition a_if : val := λ: "cnd" "e1" "e2",
  a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".

Definition a_while: val := λ: "cond" "body",
  let: "rwhile" :=
     rec: "while" "cnd" "bdy" :=
       a_if "cnd"
         (a_sequence "bdy"
            (λ: "env" "l", ("while" "cnd" "bdy") "env" "l"))
         (a_ret #())
  in "rwhile" "cond" "body".

Dan Frumin's avatar
Dan Frumin committed
58
Section proofs.
Dan Frumin's avatar
Dan Frumin committed
59
  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Dan Frumin's avatar
Dan Frumin committed
60

Dan Frumin's avatar
Dan Frumin committed
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
  Lemma a_seq_spec R `{Timeless _ R} Φ :
    U (Φ #()) -
    awp a_seq R Φ.
  Proof.
    iIntros "HΦ". rewrite /a_seq.
    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
    wp_rec. iRevert "Hflock Hunfl". iRevert (γ π env lk).
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
    iApply wp_fupd.
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    wp_let. iApply (mset_clear_spec with "HX").
    iNext. iIntros "HX".
    iDestruct "HΦ" as (us) "[Hus HΦ]".
    clear Hlocks.
    iInduction us as [|u us] "IH" forall (σ); simpl.
    - iModIntro. iFrame "HR". iSplitR "HΦ".
      + iExists , σ. iFrame. iPureIntro.
        rewrite /correct_locks /set_Forall. set_solver.
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
      iAssert (⌜σ !! u.1 = Some LLvl%I) with "[Hσ Hu]" as %?.
      { rewrite mapsto_eq /mapsto_def.
        iDestruct "Hu" as "[Hu Hl]".
          by iDestruct (own_valid_2 with "Hσ Hl")
            as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
      iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
      iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
      { iIntros "Hus". iApply "HΦ". by iFrame. }
      { rewrite -big_sepM_insert_override; eauto. }
  Qed.

Dan Frumin's avatar
Dan Frumin committed
95
96
97
98
99
100
  Lemma a_load_spec R `{Timeless _ R} (l : loc) (v : val) Φ :
    l U v -
    (l U v - Φ v) -
    awp (a_load (a_ret #l)) R Φ.
  Proof.
    unfold a_load. iIntros "Hv HΦ".
Dan Frumin's avatar
Dan Frumin committed
101
    rewrite /a_ret.
Dan Frumin's avatar
Dan Frumin committed
102
    do 2 awp_lam.
Dan Frumin's avatar
Dan Frumin committed
103
104
    iApply awp_bind.
    iApply awp_value.
Dan Frumin's avatar
Dan Frumin committed
105
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
106
107
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
Dan Frumin's avatar
Dan Frumin committed
108
109
110
111
112
113
114
115
116
117
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
    assert (#l  X).
    { unfold correct_locks in *. intros Hx. apply Hl.
      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
    wp_let.
    wp_apply wp_assert.
    wp_apply (mset_member_spec #l env with "HX").
118
    iIntros "Henv /=". case_decide; first by exfalso. simpl.
Dan Frumin's avatar
Dan Frumin committed
119
120
    wp_op. iSplit; eauto. iNext. wp_seq.
    rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load.
Dan Frumin's avatar
Dan Frumin committed
121
122
123
124
    iCombine "Hv Hl" as "Hv". iFrame "HR".
    iSplitR "HΦ Hv".
    - iExists X,σ. by iFrame.
    - by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
125
126
127
128
129
130
  Qed.

  Lemma a_alloc_spec R `{Timeless _ R} (v : val) Φ :
    ( l, l U v - Φ #l) -
    awp (a_alloc (a_ret v)) R Φ.
  Proof.
Dan Frumin's avatar
Dan Frumin committed
131
132
133
134
135
136
137
    unfold a_alloc. iIntros "HΦ".
    rewrite /a_ret.
    do 2 awp_lam.
    iApply awp_bind. iApply awp_value.
    awp_let.
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
Dan Frumin's avatar
Dan Frumin committed
138
139
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks.
Dan Frumin's avatar
Dan Frumin committed
140
141
    iApply wp_fupd.
    wp_let. wp_alloc l as "Hl".
Dan Frumin's avatar
Dan Frumin committed
142
143
144
    iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
    { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
      iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
Dan Frumin's avatar
Dan Frumin committed
145
146
      iDestruct "Hls" as (v') "Hl'".
      by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
Dan Frumin's avatar
Dan Frumin committed
147
148
    iDestruct "Hl" as "[Hl Hl']".
    iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
Dan Frumin's avatar
Dan Frumin committed
149
150
151
152
153
    iModIntro. iFrame "HR". iSplitR "HΦ Hl'".
    - iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
      + rewrite big_sepM_insert; eauto. iFrame. eauto.
      + iPureIntro. by rewrite locked_locs_alloc_unlocked.
    - by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
154
  Qed.
Dan Frumin's avatar
Dan Frumin committed
155

Dan Frumin's avatar
Dan Frumin committed
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
  Lemma a_store_spec `{Timeless _ R} (l : loc) (v : val) (w : val) Φ :
    l U v -
    (l L w - Φ w) -
    awp (a_store (a_ret #l) (a_ret w)) R Φ.
  Proof.
    unfold a_store. iIntros "Hv HΦ".
    rewrite /a_ret.
    repeat (awp_pure _).
    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
    Opaque par. repeat (wp_pure _).
    wp_bind (_ ||| _)%E.
    iApply (wp_par (fun v => v = #l) (fun v => v = w))%I.
    { repeat wp_pure _. eauto. }
    { repeat wp_pure _. eauto. }
    iIntros (? ?) "[% %]"; simplify_eq/=. iNext.
    wp_let. wp_let.
    iRevert "Hflock Hunfl". iRevert (γ π env lk).
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
    assert (#l  X).
    { unfold correct_locks in *. intros Hx. apply Hl.
      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
    wp_let. wp_proj.
    wp_apply (mset_add_spec with "[$HX]"); eauto.
    iIntros "HX". wp_seq.
    iAssert (⌜σ !! l = Some ULvl%I) with "[Hσ Hv]" as %?.
    { rewrite mapsto_eq /mapsto_def.
      iDestruct "Hv" as "[Hv Hl]".
      by iDestruct (own_valid_2 with "Hσ Hl")
        as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
    iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
    do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
    iDestruct "Hv" as "[Hv Hl]".
    rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
    iDestruct "Hls" as "[Hl' Hls]".
    iDestruct "Hl'" as (?) "Hl'".
    iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
    iCombine "Hv Hl'" as "Hv".
    wp_store.
    iDestruct "Hv" as "[Hv Hl']".
    iSpecialize ("Hls" with "[Hl']"); eauto.
    wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
    - iExists ({[#l]}  X),(<[l:=LLvl]> σ). iFrame. iSplitL.
      + rewrite -big_sepM_insert_override; eauto.
      + (* TODO: a separate lemma somewhere *)
        iPureIntro. rewrite locked_locs_lock.
        revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
    - iApply "HΦ". iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
210
End proofs.