iris.v 36.2 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
  Section Erasure.
    Local Open Scope pcm_scope.
161 162 163 164 165 166 167
    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
     *)
168
    Fixpoint comp_list (xs : list res) : option res :=
169 170
      match xs with
        | nil => 1
171
        | (x :: xs)%list => Some x · comp_list xs
172 173 174
      end.

    Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
175
    Definition erase (m : nat -f> res) : option res := comp_list (cod m).
176 177

    Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
178
      erase rs == Some r · erase (fdRemove i rs).
179
    Proof.
180 181
      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.
182
      destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
183 184
      simpl comp_list; rewrite IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some s)); reflexivity.
185 186 187
    Qed.

    Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
188
      Some r · erase rs == erase (fdUpdate i r rs).
189
    Proof.
190 191
      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].
192
      destruct (comp i j); [discriminate | reflexivity |].
193 194
      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some r)); reflexivity.
195 196
    Qed.

197 198 199
    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).
200
    Proof.
201 202
      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.
203
      destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
204 205 206
      - 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.
207 208 209
    Qed.

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

211
    Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
212
       (mkUPred (fun n _ =>
213
                    erase_state (option_map fst (Some r · Some s)) σ
214
                    /\ exists rs : nat -f> res,
215
                         erase rs == Some s /\
216 217 218 219
                         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) _).
220
    Next Obligation.
221 222
      intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
      setoid_rewrite HLe; eassumption.
223 224
    Qed.

Filip Sieczkowski's avatar
Filip Sieczkowski committed
225
    Global Instance erasure_equiv σ : Proper (meq ==> eq ==> eq ==> equiv ==> equiv) (erasure σ).
226
    Proof.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
227
      intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |]; subst r' s'.
228
      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
229
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
230 231
        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
232
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
233 234
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
235 236 237 238 239
    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 |].
240 241 242 243
      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.
244 245 246
        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 |].
247 248 249 250
        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.
251 252 253
        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 |].
254
        apply HR; [reflexivity | assumption].
255 256 257 258 259 260 261 262 263 264
    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.
265 266

    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
267 268 269 270 271 272
      mkUPred (fun n r => forall w1 rf rr s mf σ k (HSub : w  w1) (HLe : k < n)
                                 (HD : mf # m1  m2) (HEq : Some r · Some rf == Some rr)
                                 (HE : erasure σ (m1  mf) rr s w1 @ S k),
                          exists w2 r' rr' s',
                            w1  w2 /\ p w2 (S k) r' /\ Some r' · Some rf == Some rr'
                            /\ erasure σ (m2  mf) rr' s' w2 @ S k) _.
273
    Next Obligation.
274
      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
275 276 277 278 279 280 281 282 283 284
      rewrite <- HR, (comm (Some rd)), <- assoc in HEq; clear r2 HR.
      destruct (Some rd · Some rf) as [rf' |] eqn: HR;
        [| erewrite comm, pcm_op_zero in HEq by apply _; contradiction].
      destruct (HP w1 rf' rr s mf σ k) as [w2 [r1' [rr' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try assumption; [|].
      - eauto with arith.
      - rewrite <- HR, assoc in HR'; clear rf' HR HEq HP.
        destruct (Some r1' · Some rd) as [r2' |] eqn: HR;
          [| erewrite pcm_op_zero in HR' by apply _; contradiction].
        exists w2 r2' rr' s'; split; [assumption | split; [| split; assumption] ].
        eapply uni_pred, HP'; [| exists rd; rewrite comm, HR]; reflexivity.
285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
    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)).
300
        edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
301 302
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
303 304
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
          exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
305 306 307
          * 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)).
308
        edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
309 310
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
311 312
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
          exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
313 314 315 316 317 318 319 320 321 322 323 324 325 326
          * 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.
327 328
      - edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
        clear HP; repeat (eexists; try eassumption); [].
329
        apply EQp; [now eauto with arith | assumption].
330 331
      - edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
        clear HP; repeat (eexists; try eassumption); [].
332 333 334 335 336 337 338 339
        apply EQp; [now eauto with arith | assumption].
    Qed.

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

  End ViewShifts.

340 341 342 343
  Section ViewShiftProps.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
344 345

    Implicit Types (p q r : Props) (i : nat) (m : mask).
346 347 348 349 350 351 352 353 354 355 356 357 358 359

    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.
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
      - rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
        destruct (Some rr · Some s) as [ss |] eqn: HR; setoid_rewrite HR in HES;
          [| contradiction (erase_state_nonzero _ HES) ].
        destruct (Some r · Some rf) as [rr' |] eqn: HR1;
          [simpl in HEq; subst rr' | contradiction].
        destruct (Some ri · erase (fdRemove i rs)) as [s' |] eqn: HR2;
          [simpl in HE; subst s' | contradiction].
        assert (HEq : Some r · Some ri · Some rf · erase (fdRemove i rs) == Some ss).
        { rewrite <- (assoc (Some r)), (comm (Some ri)), assoc, HR1, <- assoc, HR2, HR; reflexivity. }
        clear HR HR1 HR2; destruct (Some r · Some ri) as [rri |] eqn: HR1;
        [| now erewrite !pcm_op_zero in HEq by apply _].
        destruct (Some rri · Some rf) as [rr' |] eqn: HR2;
          [| now erewrite pcm_op_zero in HEq by apply _].
        destruct (erase (fdRemove i rs)) as [s' |] eqn: HRS;
          [| now erewrite comm, pcm_op_zero in HEq by apply _].
        exists w' rri rr' s'; split; [reflexivity | split; [| split; [rewrite HR2; reflexivity | split] ] ].
376 377
        + simpl; eapply HInv; [now auto with arith |].
          specialize (HSub i); rewrite HLu in HSub.
378
          eapply uni_pred, HM with i; [| exists r; rewrite <- HR1 | | | rewrite HLr]; try reflexivity; [|].
379 380 381
          * left; unfold mask_sing, mask_set.
            destruct (Peano_dec.eq_nat_dec i i); tauto.
          * symmetry; destruct (w' i); [assumption | contradiction].
382 383 384
        + destruct (Some rr' · Some s') as [ss' |] eqn: HR; [| contradiction].
          setoid_rewrite HR; simpl in HEq; subst; assumption.
        + exists (fdRemove i rs); split; [rewrite HRS; reflexivity | intros j Hm].
385 386 387 388 389 390 391 392 393 394 395
          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.

396
    (*Lemma vsClose i p :
397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428
      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 k as [| k]; [now inversion HGt |].
      destruct HE as [HES [rs [HE HM] ] ].
      exists w' 1 (r · s); split; [reflexivity | split; [exact I |] ].
      split; [erewrite pcm_op_unit, assoc, (comm rf) by apply _; assumption |].
      remember (match rs i with Some ri => ri | None => 1 end) as ri eqn: EQri.
      exists (fdUpdate i (ri · r) rs); split; intros.
      - clear -HE EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
        [erewrite erase_insert_old; [reflexivity | assumption] |].
        erewrite pcm_op_unit, erase_insert_new; [reflexivity | assumption | apply _].
      - specialize (HD i0); unfold mask_sing, mask_set in *; simpl in Hm, HD.
        destruct (Peano_dec.eq_nat_dec i i0); [subst i0; clear Hm | destruct Hm as [Hm | Hm]; [contradiction |] ].
        + split; intros.
          * specialize (HSub i); rewrite HLu in HSub.
            rewrite !fdLookup_in_strong, fdUpdate_eq; destruct (w' i);
            [intuition now eauto | contradiction].
          * rewrite fdUpdate_eq in HLrs; simpl in HLrs; subst ri0.
            destruct n as [| n]; [now inversion HLe |]; simpl in HP.
            rewrite <- HSub; specialize (HSub i); rewrite HLu in HSub.
            destruct (w' i) as [π' |]; [| contradiction]; simpl in HSub, HLw.
            rewrite <- HLw, <- HSub; apply HInv; [now auto with arith |].
            eapply uni_pred, HP; [now auto with arith |].
            subst r; rewrite assoc; eexists; reflexivity.
        + rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption.
          auto.
429
    Qed.*)
430 431 432 433 434 435

    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).
436
      edestruct Hpq as [w2 [rq [rrq [sq [HSw12 [Hq [HEq' HErq] ] ] ] ] ] ]; try eassumption; [|].
437 438 439 440 441
      { (* 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].
      }
442
      clear HS; assert (HS : pcm_unit _  rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
443
      rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
444 445
      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [rrR [sR [HSw23 [Hr [HR HEr] ] ] ] ] ] ];
        try (reflexivity || eassumption); [now auto with arith | |].
446 447 448 449 450 451
      { (* 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.
452
      setoid_rewrite HSw12; eauto 8.
453 454
    Qed.

455 456
    Lemma vsEnt p q m :
       (p  q)  vs m m p q.
457
    Proof.
458 459 460 461 462 463
      intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
      intros np rp HLe HS Hp w1; intros.
      exists w1 rp rr s; split; [reflexivity | split; [| split; assumption ] ].
      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.
464

465
    (* Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
466 467
      vs m1 m2 p q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (p * r) (q * r).
    Proof.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
468 469 470 471 472 473 474 475 476 477 478 479 480 481
      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.
      assert (HS : 1 ⊑ rp) by (exists rp; erewrite comm, pcm_op_unit by apply _; reflexivity).
      specialize (HVS _ _ HLe HS Hp w' s (rr · rf) (mf ∪ mf0) σ k); clear HS.
      destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
      - (* disjointness: possible lemma *)
        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.
      - exists w'' (rq · rr) s'; split; [assumption | split].
        + rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr; now auto.
        + rewrite <- assoc; eapply erasure_equiv, HEq; try reflexivity; [].
          clear; intros i; tauto.
482
    Qed.*)
483 484 485 486 487 488 489 490 491 492

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

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

Filip Sieczkowski's avatar
Filip Sieczkowski committed
493 494 495 496 497 498 499 500 501 502 503
  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.
504 505 506 507 508
    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
509 510 511 512 513 514

    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 :=
515 516 517
      forall w' k s rf rr σ
             (HSw : w  w') (HLt : k < n) (HR : Some r · Some rf == Some rr)
             (HE : erasure σ m rr s w' @ S k),
Filip Sieczkowski's avatar
Filip Sieczkowski committed
518
        (forall (HV : is_value e),
519 520 521
         exists w'' r' rr' s', w'  w'' /\ φ (exist _ e HV) w'' (S k) r'
                               /\ Some r' · Some rf == Some rr'
                               /\ erasure σ m rr' s' w'' @ S k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
522 523
        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                (HStep : prim_step (ei, σ) (ei', σ')),
524 525 526
         exists w'' r' rr' s', w'  w'' /\ WP (K [[ ei' ]]) φ w'' k r'
                               /\ Some r' · Some rf == Some rr'
                               /\ erasure σ' m rr' s' w'' @ k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
527
        (forall e' K (HDec : e = K [[ e' ]]),
528 529 530 531
         exists w'' rfk rret rr' s', w'  w'' /\ Some rfk · Some rret · Some rf == Some rr'
                                     /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                     /\ WP e' (umconst ) w'' k rfk
                                     /\ erasure σ m rr' s' w'' @ k).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
532 533 534 535

    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.
536 537 538 539 540 541
      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf rr σ HSw HLt HR HE.
      rewrite <- EQr, (comm (Some rd)), <- assoc in HR.
      destruct (Some rd · Some rf) as [rf' |] eqn: HRF;
        [| now erewrite comm, pcm_op_zero in HR by apply _].
      specialize (Hp w' k s rf' rr σ); destruct Hp as [HV [HS HF] ];
      [| now eauto with arith | ..]; try assumption; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
542
      split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
      - specialize (HV HV0); destruct HV as [w'' [r2' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
        rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
        destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
          [| now erewrite pcm_op_zero in HR' by apply _].
        exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
        eapply uni_pred, Hφ; [| eexists; rewrite <- HR1]; reflexivity.
      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r2' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
        rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
        destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
          [| now erewrite pcm_op_zero in HR' by apply _].
        exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
        eapply uni_pred, HWP; [| eexists; rewrite <- HR1]; reflexivity.
      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret2 [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
        rewrite <- HRF, assoc, <- (assoc (Some rfk)), (comm (Some rret2)) in HR'.
        destruct (Some rd · Some rret2) as [rret1 |] eqn: HR1;
          [| now erewrite (comm _ 0), !pcm_op_zero in HR' by apply _].
        exists w'' rfk rret1 rr'; exists s'; repeat (split; try assumption); [].
        eapply uni_pred, HWR; [| eexists; rewrite <- HR1]; reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
561 562 563 564 565 566 567 568 569 570 571 572 573
    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.
574
        + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
575 576
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
577 578
          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
          split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
579
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
580
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
581 582
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
583 584
          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
          split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
585
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
586
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
587 588
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
589 590 591
          exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          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
592 593 594 595
      - 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.
596
        + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
597 598
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
599 600
          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
          split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
601
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
602
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
603 604
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
605 606
          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
          split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
607
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
608
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
609 610
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
611 612 613
          exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          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
614 615 616 617 618 619 620 621 622 623 624 625 626
    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.
627 628
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
629
          apply EQφ, Hφ; now eauto with arith.
630 631
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
632
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
633 634
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
635 636
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
      - split; [| split]; intros.
637 638
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
639
          apply EQφ, Hφ; now eauto with arith.
640 641
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
642
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
643 644
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
          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].
663 664
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
665
          eapply (EQWP _ _ _), HWP; now eauto with arith.
666 667 668
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
669
      - split; [assumption | split; intros].
670 671
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
672
          eapply (EQWP _ _ _), HWP; now eauto with arith.
673 674 675
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
676 677 678 679 680 681 682
    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].
683 684
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
685
          eapply EQWP, HWP; now eauto with arith.
686 687 688
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
689
      - split; [assumption | split; intros].
690 691
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
692
          eapply EQWP, HWP; now eauto with arith.
693 694 695
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
696 697 698 699 700 701
    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 φ).
702

Filip Sieczkowski's avatar
Filip Sieczkowski committed
703
  End HoareTriples.
704

705
End Iris.