iris.v 43.5 KB
Newer Older
1
Require Import world_prop core_lang lang masks.
2
Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
3
4
5
6

Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).

  Module Import L  := Lang RP RL C.
7
  Module Import R <: PCM_T.
8
9
10
11
12
13
14
    Definition res := (RP.res * RL.res)%type.
    Instance res_op   : PCM_op res := _.
    Instance res_unit : PCM_unit res := _.
    Instance res_pcm  : PCM res := _.
  End R.
  Module Import WP := WorldProp R.

15
16
17
  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

18
19
20
21
22
23
24
25
26
27
28
29
30
  (** The final thing we'd like to check is that the space of
      propositions does indeed form a complete BI algebra.

      The following instance declaration checks that an instance of
      the complete BI class can be found for Props (and binds it with
      a low priority to potentially speed up the proof search).
   *)

  Instance Props_BI : ComplBI Props | 0 := _.
  Instance Props_Later : Later Props | 0 := _.

  (** And now we're ready to build the IRIS-specific connectives! *)

31
32
33
34
35
36
  Section Necessitation.
    (** Note: this could be moved to BI, since it's possible to define
        for any UPred over a monoid. **)

    Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.

37
    Program Definition box : Props -n> Props :=
38
      n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
    Next Obligation.
      intros n m r s HLe _ Hp; rewrite HLe; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw m r HLt; simpl.
      eapply (met_morph_nonexp _ _ p); eassumption.
    Qed.
    Next Obligation.
      intros w1 w2 Subw n r; simpl.
      apply p; assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w m r HLt; simpl.
      apply EQp; assumption.
    Qed.

  End Necessitation.

  (** "Internal" equality **)
  Section IntEq.
    Context {T} `{mT : metric T}.

61
    Program Definition intEqP (t1 t2 : T) : UPred res :=
62
63
64
65
66
      mkUPred (fun n r => t1 = S n = t2) _.
    Next Obligation.
      intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
    Qed.

67
    Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
68
69
70
71
72
73
74
75

    Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
    Proof.
      intros l1 l2 EQl r1 r2 EQr n r.
      split; intros HEq; do 2 red.
      - rewrite <- EQl, <- EQr; assumption.
      - rewrite EQl, EQr; assumption.
    Qed.
76

77
78
79
80
81
82
83
84
85
86
87
88
89
90
    Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
    Proof.
      intros l1 l2 EQl r1 r2 EQr m r HLt.
      split; intros HEq; do 2 red.
      - etransitivity; [| etransitivity; [apply HEq |] ];
        apply mono_dist with n; eassumption || now auto with arith.
      - etransitivity; [| etransitivity; [apply HEq |] ];
        apply mono_dist with n; eassumption || now auto with arith.
    Qed.

  End IntEq.

  Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.

91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
  Section Invariants.

    (** Invariants **)
    Definition invP (i : nat) (p : Props) (w : Wld) : UPred res :=
      intEqP (w i) (Some (ı' p)).
    Program Definition inv i : Props -n> Props :=
      n[(fun p => m[(invP i p)])].
    Next Obligation.
      intros w1 w2 EQw; unfold equiv, invP in *.
      apply intEq_equiv; [apply EQw | reflexivity].
    Qed.
    Next Obligation.
      intros w1 w2 EQw; unfold invP; simpl morph.
      destruct n; [apply dist_bound |].
      apply intEq_dist; [apply EQw | reflexivity].
    Qed.
    Next Obligation.
      intros w1 w2 Sw; unfold invP; simpl morph.
      intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
      destruct (w1 i) as [μ1 |]; [| contradiction].
      destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
      rewrite <- Sw; assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w; unfold equiv, invP in *; simpl morph.
      apply intEq_equiv; [reflexivity |].
      rewrite EQp; reflexivity.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w; unfold invP; simpl morph.
      apply intEq_dist; [reflexivity |].
      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
    Qed.

  End Invariants.
126

127
128
129
130
131
132
133
134
135
136
137
138
139
  Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope.
  Notation "⊤" := (top : Props) : iris_scope.
  Notation "⊥" := (bot : Props) : iris_scope.
  Notation "p ∧ q" := (and p q : Props) (at level 40, left associativity) : iris_scope.
  Notation "p ∨ q" := (or p q : Props) (at level 50, left associativity) : iris_scope.
  Notation "p * q" := (sc p q : Props) (at level 40, left associativity) : iris_scope.
  Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
  Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
  Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∃ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.

140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
  (** Ownership **)
  Definition ownR (r : res) : Props :=
    pcmconst (up_cr (pord r)).

  (** Physical part **)
  Definition ownRP (r : RP.res) : Props :=
    ownR (r, pcm_unit _).

  (** Logical part **)
  Definition ownRL (r : RL.res) : Props :=
    ownR (pcm_unit _, r).

  (** Proper ghost state: ownership of logical w/ possibility of undefined **)
  Definition ownL (r : option RL.res) : Props :=
    match r with
      | Some r => ownRL r
      | None => 
    end.

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
  Lemma ores_equiv_eq (r1 r2 : option res) (HEq : r1 == r2) : r1 = r2.
  Proof.
    destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
    simpl in HEq; subst; reflexivity.
  Qed.

  (** Lemmas about box **)
  Lemma box_intro p q (Hpq :  p  q) :
     p   q.
  Proof.
    intros w n r Hp; simpl; apply Hpq, Hp.
  Qed.

  Lemma box_elim p :
     p  p.
  Proof.
    intros w n r Hp; simpl in Hp.
    eapply uni_pred, Hp; [reflexivity |].
    exists r; now erewrite comm, pcm_op_unit by apply _.
  Qed.

  (** Ghost state ownership **)
  Lemma ownL_sc (u t : option RL.res) :
    ownL (u · t)%pcm == ownL u * ownL t.
  Proof.
    intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
    - destruct (u · t)%pcm as [ut |] eqn: EQut; [| contradiction].
      do 13 red in Hut; rewrite <- Hut.
      destruct u as [u |]; [| now erewrite pcm_op_zero in EQut by apply _].
      assert (HT := comm (Some u) t); rewrite EQut in HT.
      destruct t as [t |]; [| now erewrite pcm_op_zero in HT by apply _]; clear HT.
      exists (pcm_unit RP.res, u) (pcm_unit RP.res, t).
      split; [unfold pcm_op, res_op, pcm_op_prod | split; do 13 red; reflexivity].
      now erewrite pcm_op_unit, EQut by apply _.
    - destruct u as [u |]; [| contradiction]; destruct t as [t |]; [| contradiction].
      destruct Hu as [ru EQu]; destruct Ht as [rt EQt].
      rewrite <- EQt, assoc, (comm (Some r1)) in EQr.
      rewrite <- EQu, assoc, <- (assoc (Some rt · Some ru)%pcm) in EQr.
      unfold pcm_op at 3, res_op at 4, pcm_op_prod at 1 in EQr.
      erewrite pcm_op_unit in EQr by apply _; clear EQu EQt.
      destruct (Some u · Some t)%pcm as [ut |];
        [| now erewrite comm, pcm_op_zero in EQr by apply _].
      destruct (Some rt · Some ru)%pcm as [rut |];
        [| now erewrite pcm_op_zero in EQr by apply _].
      exists rut; assumption.
  Qed.

206
207
  Section Erasure.
    Local Open Scope pcm_scope.
208
209
210
211
212
213
214
    Local Open Scope bi_scope.

    (* First, we need to erase a finite map. This won't be pretty, for
       now, since the library does not provide enough
       constructs. Hopefully we can provide a fold that'd work for
       that at some point
     *)
215
    Fixpoint comp_list (xs : list res) : option res :=
216
217
      match xs with
        | nil => 1
218
        | (x :: xs)%list => Some x · comp_list xs
219
220
221
      end.

    Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
222
    Definition erase (m : nat -f> res) : option res := comp_list (cod m).
223
224

    Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
225
      erase rs == Some r · erase (fdRemove i rs).
226
    Proof.
227
228
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
229
      destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
230
231
      simpl comp_list; rewrite IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some s)); reflexivity.
232
233
234
    Qed.

    Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
235
      Some r · erase rs == erase (fdUpdate i r rs).
236
    Proof.
237
238
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
239
      destruct (comp i j); [discriminate | reflexivity |].
240
241
      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some r)); reflexivity.
242
243
    Qed.

244
245
246
    Lemma erase_insert_old (rs : nat -f> res) i r1 r2 r
          (HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
      Some r2 · erase rs == erase (fdUpdate i r rs).
247
    Proof.
248
249
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
250
      destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
251
252
253
      - simpl comp_list; rewrite assoc, (comm (Some r2)), <- HEq; reflexivity.
      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
        rewrite !assoc, (comm (Some r2)); reflexivity.
254
255
256
    Qed.

    Global Instance preo_unit : preoType () := disc_preo ().
257

258
    Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
259
       (mkUPred (fun n _ =>
260
                    erase_state (option_map fst (r · s)) σ
261
                    /\ exists rs : nat -f> res,
262
                         erase rs == s /\
263
264
265
266
                         forall i (Hm : m i),
                           (i  dom rs <-> i  dom w) /\
                           forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
                             ı π w n ri) _).
267
    Next Obligation.
268
269
      intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
      setoid_rewrite HLe; eassumption.
270
271
    Qed.

272
    Global Instance erasure_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (erasure σ).
273
    Proof.
274
275
      intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |];
      apply ores_equiv_eq in EQr; apply ores_equiv_eq in EQs; subst r' s'.
276
      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
277
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
278
279
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
280
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
281
282
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
283
284
285
286
287
    Qed.

    Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ m r s).
    Proof.
      intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
288
289
290
291
      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
      - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
        assert (EQπ := EQw i); rewrite HLw in EQπ; clear HLw.
292
293
294
        destruct (w1 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
295
296
297
298
        apply HR; [reflexivity | assumption].
      - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
        assert (EQπ := EQw i); rewrite HLw in EQπ; clear HLw.
299
300
301
        destruct (w2 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
302
        apply HR; [reflexivity | assumption].
303
304
305
306
307
308
309
310
311
312
    Qed.

  End Erasure.

  Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).

  Section ViewShifts.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Obligation Tactic := intros.
313

314
315
316
317
318
319
320
Lemma erasure_not_empty σ m r s w k (HN : r · s == 0) :
  ~ erasure σ m r s w @ S k.
Proof.
  intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
  now apply erase_state_nonzero in HD.
Qed.

321
    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
322
323
324
325
326
327
      mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w  w1) (HLe : k < n)
                                 (HD : mf # m1  m2)
                                 (HE : erasure σ (m1  mf) (Some r · rf) s w1 @ S k),
                          exists w2 r' s',
                            w1  w2 /\ p w2 (S k) r'
                            /\ erasure σ (m2  mf) (Some r' · rf) s' w2 @ S k) _.
328
    Next Obligation.
329
      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
330
331
332
333
334
335
336
337
338
      destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
        try assumption; [now eauto with arith | |].
      - eapply erasure_equiv, HE; try reflexivity.
        rewrite assoc, (comm (Some r1)), HR; reflexivity.
      - rewrite assoc, (comm (Some r1')) in HE'.
        destruct (Some rd · Some r1') as [r2' |] eqn: HR';
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w2 r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
    Qed.

    Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
      n[(fun p => m[(preVS m1 m2 p)])].
    Next Obligation.
      intros w1 w2 EQw n r; split; intros HP w2'; intros.
      - eapply HP; try eassumption; [].
        rewrite EQw; assumption.
      - eapply HP; try eassumption; [].
        rewrite <- EQw; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
      - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
        assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
354
        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
355
356
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
357
358
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
          exists (extend w1'' w2') r' s'; split; [assumption | split].
359
360
361
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
          * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
      - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
362
        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
363
364
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
365
366
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
          exists (extend w1'' w2') r' s'; split; [assumption | split].
367
368
369
370
371
372
373
374
375
376
377
378
379
380
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
          * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
    Qed.
    Next Obligation.
      intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
      etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w n r; split; intros HP w1; intros.
      - setoid_rewrite <- EQp; eapply HP; eassumption.
      - setoid_rewrite EQp; eapply HP; eassumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
381
      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
382
        clear HP; repeat (eexists; try eassumption); [].
383
        apply EQp; [now eauto with arith | assumption].
384
      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
385
        clear HP; repeat (eexists; try eassumption); [].
386
387
388
389
390
391
392
393
        apply EQp; [now eauto with arith | assumption].
    Qed.

    Definition vs (m1 m2 : mask) (p q : Props) : Props :=
       (p  pvs m1 m2 q).

  End ViewShifts.

394
395
396
397
  Section ViewShiftProps.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
398
399

    Implicit Types (p q r : Props) (i : nat) (m : mask).
400
401
402
403
404
405
406
407
408
409
410
411
412
413

    Definition mask_sing i := mask_set mask_emp i True.

    Lemma vsOpen i p :
      valid (vs (mask_sing i) mask_emp (inv i p) ( p)).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ HInv w'; clear nn; intros.
      do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
      destruct HE as [HES [rs [HE HM] ] ].
      destruct (rs i) as [ri |] eqn: HLr.
414
      - rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
415
416
417
418
419
420
421
        assert (HR : Some r · rf · s == Some r · Some ri · rf · erase (fdRemove i rs))
          by (rewrite <- HE, assoc, <- (assoc (Some r)), (comm rf), assoc; reflexivity).
        apply ores_equiv_eq in HR; setoid_rewrite HR in HES; clear HR.
        destruct (Some r · Some ri) as [rri |] eqn: HR;
          [| erewrite !pcm_op_zero in HES by apply _; now apply erase_state_nonzero in HES].
        exists w' rri (erase (fdRemove i rs)); split; [reflexivity |].
        split; [| split; [assumption |] ].
422
        + simpl; eapply HInv; [now auto with arith |].
423
424
          eapply uni_pred, HM with i;
            [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
425
426
          * left; unfold mask_sing, mask_set.
            destruct (Peano_dec.eq_nat_dec i i); tauto.
427
428
429
          * specialize (HSub i); rewrite HLu in HSub.
            symmetry; destruct (w' i); [assumption | contradiction].
        + exists (fdRemove i rs); split; [reflexivity | intros j Hm].
430
431
432
433
434
435
436
437
438
439
440
          destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
          unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
          [subst j; contradiction HD; tauto | clear HD].
          rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; now auto.
      - rewrite <- fdLookup_notin_strong in HLr; contradiction HLr; clear HLr.
        specialize (HSub i); rewrite HLu in HSub; clear - HM HSub.
        destruct (HM i) as [HD _]; [left | rewrite HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
        clear; unfold mask_sing, mask_set.
        destruct (Peano_dec.eq_nat_dec i i); tauto.
    Qed.

441
    Lemma vsClose i p :
442
443
444
445
446
447
448
449
450
      valid (vs mask_emp (mask_sing i) (inv i p *  p) ).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
      do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
      destruct HE as [HES [rs [HE HM] ] ].
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
      exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
      assert (HR' : Some r · rf · s = rf · (Some r · s))
        by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
      setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
      split; [assumption |].
      remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
      destruct (Some ri · Some r) as [rri |] eqn: EQR.
      - exists (fdUpdate i rri rs); split; [| intros j Hm].
        + symmetry; rewrite <- HE; clear - EQR EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
          [eapply erase_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
          erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
          now apply erase_insert_new.
        + specialize (HD j); unfold mask_sing, mask_set in *; simpl in Hm, HD.
          destruct (Peano_dec.eq_nat_dec i j);
            [subst j; clear Hm |
             destruct Hm as [Hm | Hm]; [contradiction | rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
          rewrite !fdLookup_in_strong, fdUpdate_eq.
          destruct n as [| n]; [now inversion HLe | simpl in HP].
          rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
          destruct (w' i) as [π' |]; [| contradiction].
          split; [intuition now eauto | intros].
          simpl in HLw, HLrs, HSub; subst ri0; rewrite <- HLw, <- HSub.
          apply HInv; [now auto with arith |].
          eapply uni_pred, HP; [now auto with arith |].
          assert (HT : Some ri · Some r1 · Some r2 == Some rri)
            by (rewrite <- EQR, <- HR, assoc; reflexivity); clear - HT.
          destruct (Some ri · Some r1) as [rd |];
            [| now erewrite pcm_op_zero in HT by apply _].
          exists rd; assumption.
      - destruct (rs i) as [rsi |] eqn: EQrsi; subst;
        [| erewrite pcm_op_unit in EQR by apply _; discriminate].
        contradiction (erase_state_nonzero σ); clear - HE HES EQrsi EQR.
        assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; assumption].
        apply ores_equiv_eq; rewrite <- HE, erase_remove by eassumption.
        rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
        erewrite !pcm_op_zero by apply _; reflexivity.
    Qed.
488
489
490
491
492
493

    Lemma vsTrans p q r m1 m2 m3 (HMS : m2  m1  m3) :
      vs m1 m2 p q  vs m2 m3 q r  vs m1 m3 p r.
    Proof.
      intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
      intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
494
      edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
495
496
497
498
499
      { (* XXX: possible lemma *)
        clear - HD HMS.
        intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
        destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
      }
500
      clear HS; assert (HS : pcm_unit _  rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
501
      rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
502
      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [sR [HSw23 [Hr HEr] ] ] ] ];
503
        try (reflexivity || eassumption); [now auto with arith | |].
504
505
506
507
508
509
      { (* XXX: possible lemma *)
        clear - HD HMS.
        intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
        destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
      }
      clear HEq Hq HS.
510
      setoid_rewrite HSw12; eauto 8.
511
512
    Qed.

513
514
    Lemma vsEnt p q m :
       (p  q)  vs m m p q.
515
    Proof.
516
517
      intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
      intros np rp HLe HS Hp w1; intros.
518
      exists w1 rp s; split; [reflexivity | split; [| assumption ] ].
519
520
521
      eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
      unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
    Qed.
522

523
    Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1  m2) :
524
525
      vs m1 m2 p q  vs (m1  mf) (m2  mf) (p * r) (q * r).
    Proof.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
526
527
      intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
      intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
528
529
      assert (HS : pcm_unit _  rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) s (mf  mf0) σ k); clear HS.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
530
      destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
531
      - (* disjointness of masks: possible lemma *)
Filip Sieczkowski's avatar
Filip Sieczkowski committed
532
533
534
535
        clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
        eapply HD; split; [eassumption | tauto].
      - rewrite assoc, HR; eapply erasure_equiv, HE; try reflexivity; [].
        clear; intros i; tauto.
536
537
538
539
540
541
      - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
        [| apply erasure_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' rqr s'; split; [assumption | split].
        + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
          rewrite HR'; split; now auto.
        + eapply erasure_equiv, HEq; try reflexivity; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
542
          clear; intros i; tauto.
543
    Qed.
544
545
546
547
548
549
550
551

    Lemma vsFalse m1 m2 :
      valid (vs m1 m2  ).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ HB; contradiction.
    Qed.

552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
    Global Instance nat_type : Setoid nat := discreteType.
    Global Instance nat_metr : metric nat := discreteMetric.
    Global Instance nat_cmetr : cmetric nat := discreteCMetric.

    Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
      n[(fun p => n[(fun n => inv n p)])].
    Next Obligation.
      intros i i' EQi; simpl in EQi; rewrite EQi; reflexivity.
    Qed.
    Next Obligation.
      intros i i' EQi; destruct n as [| n]; [apply dist_bound |].
      simpl in EQi; rewrite EQi; reflexivity.
    Qed.
    Next Obligation.
      intros p1 p2 EQp i; simpl morph.
      apply (morph_resp (inv (` i))); assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp i; simpl morph.
      apply (inv (` i)); assumption.
    Qed.

    Lemma fresh_region (w : Wld) m (HInf : mask_infinite m) :
      exists i, m i /\ w i = None.
    Proof.
      destruct (HInf (S (List.last (dom w) 0%nat))) as [i [HGe Hm] ];
      exists i; split; [assumption |]; clear - HGe.
      rewrite <- fdLookup_notin_strong.
      destruct w as [ [| [n v] w] wP]; unfold dom in *; simpl findom_t in *; [tauto |].
      simpl List.map in *; rewrite last_cons in HGe.
      unfold ge in HGe; intros HIn; eapply Gt.gt_not_le, HGe.
      apply Le.le_n_S, SS_last_le; assumption.
    Qed.

    (* XXX: move up to definitions *)
    Definition injProp (P : Prop) : Props :=
      pcmconst (up_cr (const P)).

    Instance LP_mask m : LimitPreserving m.
    Proof.
      intros σ σc Hp; apply Hp.
    Qed.

    Lemma vsNewInv p m (HInf : mask_infinite m) :
      valid (vs m m ( p) (xist (inv' m p))).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ HP w'; clear nn; intros.
      destruct n as [| n]; [now inversion HLe | simpl in HP].
      rewrite HSub in HP; clear w HSub; rename w' into w.
      destruct (fresh_region w m HInf) as [i [Hm HLi] ].
      assert (HSub : w  fdUpdate i (ı' p) w).
      { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
        now rewrite fdUpdate_neq by assumption.
      }
      exists (fdUpdate i (ı' p) w) (pcm_unit _) (Some r · s); split; [assumption | split].
      - exists (exist _ i Hm); do 16 red.
        unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
      - erewrite pcm_op_unit by apply _.
        assert (HR : rf · (Some r · s) = Some r · rf · s)
          by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
        destruct HE as [HES [rs [HE HM] ] ].
        split; [setoid_rewrite HR; assumption | clear HR].
        assert (HRi : rs i = None).
        { destruct (HM i) as [HDom _]; [tauto |].
          rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
        }
        exists (fdUpdate i r rs); split; [now rewrite <- erase_insert_new, HE by assumption | intros j Hm'].
        rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
        + subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
          simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
          eapply uni_pred, HP; [now auto with arith | reflexivity].
        + rewrite !fdUpdate_neq, <- !fdLookup_in_strong by assumption.
          setoid_rewrite <- HSub.
          apply HM; assumption.
    Qed.

    (* XXX missing statements: NewGhost, GhostUpd, VSTimeless *)
630

Filip Sieczkowski's avatar
Filip Sieczkowski committed
631
632
633
634
635
636
637
638
639
640
641
  End ViewShiftProps.

  Section HoareTriples.
  (* Quadruples, really *)
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.

    Global Instance expr_type : Setoid expr := discreteType.
    Global Instance expr_metr : metric expr := discreteMetric.
642
643
644
645
646
    Global Instance expr_cmetr : cmetric expr := discreteCMetric.
    Instance LP_isval : LimitPreserving is_value.
    Proof.
      intros σ σc HC; apply HC.
    Qed.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
647
648
649
650
651
652

    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : value -n> Props) (r : res).

    Local Obligation Tactic := intros; eauto with typeclass_instances.

    Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
653
654
      forall w' k s rf σ (HSw : w  w') (HLt : k < n)
             (HE : erasure σ m (Some r · rf) s w' @ S k),
Filip Sieczkowski's avatar
Filip Sieczkowski committed
655
        (forall (HV : is_value e),
656
657
         exists w'' r' s', w'  w'' /\ φ (exist _ e HV) w'' (S k) r'
                           /\ erasure σ m (Some r' · rf) s' w'' @ S k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
658
659
        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                (HStep : prim_step (ei, σ) (ei', σ')),
660
661
         exists w'' r' s', w'  w'' /\ WP (K [[ ei' ]]) φ w'' k r'
                           /\ erasure σ' m (Some r' · rf) s' w'' @ k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
662
        (forall e' K (HDec : e = K [[ e' ]]),
663
664
665
666
         exists w'' rfk rret s', w'  w''
                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                 /\ WP e' (umconst ) w'' k rfk
                                 /\ erasure σ m (Some rfk · Some rret · rf) s' w'' @ k).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
667
668
669
670

    Program Definition wpF m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
      n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP m WP e φ w) _)])])])].
    Next Obligation.
671
672
673
      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf σ HSw HLt HE.
      rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
      specialize (Hp w' k s (Some rd · rf) σ); destruct Hp as [HV [HS HF] ];
674
      [| now eauto with arith | ..]; try assumption; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
675
      split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
      - specialize (HV HV0); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE'] ] ] ] ].
        rewrite assoc, (comm (Some r1')) in HE'.
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [s' [HSw' [HWP HE'] ] ] ] ].
        rewrite assoc, (comm (Some r1')) in HE'.
        destruct k as [| k]; [exists w'' r1' s'; simpl erasure; tauto |].
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
        destruct k as [| k]; [exists w'' rfk rret1 s'; simpl erasure; tauto |].
        rewrite assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
        destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
        exists w'' rfk rret2 s'; repeat (split; try assumption); [].
        eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
696
697
698
699
700
701
702
703
704
705
706
707
708
    Qed.
    Next Obligation.
      intros w1 w2 EQw n r; simpl.
      split; intros Hp w'; intros; eapply Hp; try eassumption.
      - rewrite EQw; assumption.
      - rewrite <- EQw; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
      - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
        edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
        [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
        split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
709
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
710
711
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
712
713
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
714
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
715
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
716
717
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
718
719
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
720
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
721
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
722
723
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
724
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
725
726
          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
727
728
729
730
      - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
        edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
        [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
        split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
731
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
732
733
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
734
735
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
736
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
737
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
738
739
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
740
741
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
742
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
743
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
744
745
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
746
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
747
748
          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
749
750
751
752
753
754
755
756
757
758
759
760
761
    Qed.
    Next Obligation.
      intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
      etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros φ1 φ2 EQφ w n r; simpl.
      unfold wpFP; setoid_rewrite EQφ; reflexivity.
    Qed.
    Next Obligation.
      intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
      split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
      - split; [| split]; intros.
762
763
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
764
          apply EQφ, Hφ; now eauto with arith.
765
766
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
767
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
768
769
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
770
771
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
      - split; [| split]; intros.
772
773
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
774
          apply EQφ, Hφ; now eauto with arith.
775
776
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
777
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
778
779
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
    Qed.
    Next Obligation.
      intros e1 e2 EQe φ w n r; simpl.
      simpl in EQe; subst e2; reflexivity.
    Qed.
    Next Obligation.
      intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
      simpl in EQe; subst e2; reflexivity.
    Qed.
    Next Obligation.
      intros WP1 WP2 EQWP e φ w n r; simpl.
      unfold wpFP; setoid_rewrite EQWP; reflexivity.
    Qed.
    Next Obligation.
      intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
      split; intros Hp w'; intros; edestruct Hp as [HF [HS HV] ]; try eassumption; [|].
      - split; [assumption | split; intros].
798
799
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
800
          eapply (EQWP _ _ _), HWP; now eauto with arith.
801
802
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
803
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
804
      - split; [assumption | split; intros].
805
806
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
807
          eapply (EQWP _ _ _), HWP; now eauto with arith.
808
809
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
810
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
811
812
813
814
815
816
817
    Qed.

    Instance contr_wpF m : contractive (wpF m).
    Proof.
      intros n WP1 WP2 EQWP e φ w k r HLt.
      split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
      - split; [assumption | split; intros].
818
819
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
820
          eapply EQWP, HWP; now eauto with arith.
821
822
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
823
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
824
      - split; [assumption | split; intros].
825
826
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
827
          eapply EQWP, HWP; now eauto with arith.
828
829
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
830
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
831
832
833
834
835
836
    Qed.

    Definition wp m : expr -n> (value -n> Props) -n> Props :=
      fixp (wpF m) (umconst (umconst )).

    Definition ht m P e φ :=  (P  wp m e φ).
837

Filip Sieczkowski's avatar
Filip Sieczkowski committed
838
  End HoareTriples.
839

840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
  Section HoareTripleProperties.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.

    Existing Instance LP_isval.

    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (φ : value -n> Props) (r : res).

    (** Ret **)
    Program Definition eqV v : value -n> Props :=
      n[(fun v' : value => v === v')].
    Next Obligation.
      intros v1 v2 EQv w n r; simpl in *; split; congruence.
    Qed.
    Next Obligation.
      intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
      split; congruence.
    Qed.

    Lemma htRet e (HV : is_value e) m :
      valid (ht m  e (eqV (exist _ e HV))).
    Proof.
    Admitted.

    (** Bind **)
    Program Definition plugV m φ φ' K :=
      n[(fun v : value => ht m (φ v) (K [[` v]]) φ')].
    Next Obligation.
      intros v1 v2 EQv w n r; simpl.
      setoid_rewrite EQv at 1.
      simpl in EQv; rewrite EQv; reflexivity.
    Qed.
    Next Obligation.
      intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
      eapply (impl_dist (ComplBI := Props_BI)).
      - apply φ; assumption.
      - destruct n as [| n]; [apply dist_bound | simpl in EQv].
        rewrite EQv; reflexivity.
    Qed.

    Lemma htBind P φ φ' K e m :
      ht m P e φ  all (plugV m φ φ' K)  ht m P (K [[ e ]]) φ'.
    Proof.
    Admitted.

    Lemma htBind_alt P Q φ φ' K e m
          (He : Q  ht m P e φ)
          (HK : forall v, Q  ht m (φ v) (K [[` v ]]) φ') :
      Q  ht m P (K [[ e ]]) φ'.
    Admitted.

    Implicit Type (C : Props).

    (** Consequence **)

    Lemma htCons C P P' φ φ' m e
          (HPre  : C  vs m m P P')
          (HT    : C  ht m P' e φ')
          (HPost : forall v, C  vs m m (φ' v) (φ v)) :
      C  ht m P e φ.
    Admitted.

    Lemma htACons C P P' φ φ' m m' e
          (HAt   : atomic e)
          (HSub  : m'  m)
          (HPre  : C  vs m m' P P')
          (HT    : C  ht m' P' e φ')
          (HPost : forall v, C  vs m' m (φ' v) (φ v)) :
      C  ht m P e φ.
    Admitted.

    (** Framing **)

    Lemma htFrame m P R e φ :
      ht m P e φ  ht m (P * R) e (lift_bin sc φ (umconst R)).
    Admitted.

    Lemma htAFrame m P R e φ
          (HAt : atomic e) :
      ht m P e φ  ht m (P *  R) e (lift_bin sc φ (umconst R)).
    Admitted.

    (** Fork **)

    Lemma htFork m P R e φ :
      ht m P e φ  ht m (P *  R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
    Admitted.

  End HoareTripleProperties.

932
End Iris.