iris_wp.v 42.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import world_prop core_lang masks iris_vs.
2
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
3

Ralf Jung's avatar
Ralf Jung committed
4 5
Module IrisWP (RL : PCM_T) (C : CORE_LANG).
  Module Export VS := IrisVS RL C.
6

7 8 9
  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

Filip Sieczkowski's avatar
Filip Sieczkowski committed
10 11 12 13 14 15 16 17 18
  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.
19 20 21 22 23
    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
24 25 26 27 28 29

    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 :=
30 31
      forall w' k s rf mf σ (HSw : w  w') (HLt : k < n) (HD : mf # m)
             (HE : erasure σ (m  mf) (Some r · rf) s w' @ S k),
Filip Sieczkowski's avatar
Filip Sieczkowski committed
32
        (forall (HV : is_value e),
33
         exists w'' r' s', w'  w'' /\ φ (exist _ e HV) w'' (S k) r'
34
                           /\ erasure σ (m  mf) (Some r' · rf) s' w'' @ S k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
35 36
        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                (HStep : prim_step (ei, σ) (ei', σ')),
37
         exists w'' r' s', w'  w'' /\ WP (K [[ ei' ]]) φ w'' k r'
38
                           /\ erasure σ' (m  mf) (Some r' · rf) s' w'' @ k) /\
39
        (forall e' K (HDec : e = K [[ fork e' ]]),
40 41 42
         exists w'' rfk rret s', w'  w''
                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                 /\ WP e' (umconst ) w'' k rfk
43
                                 /\ erasure σ (m  mf) (Some rfk · Some rret · rf) s' w'' @ k).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
44 45 46 47

    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.
48
      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf mf σ HSw HLt HD HE.
49
      rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
50
      specialize (Hp w' k s (Some rd · rf) mf σ); destruct Hp as [HV [HS HF] ];
51
      [| now eauto with arith | ..]; try assumption; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
52
      split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
      - 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
73 74 75 76 77 78 79 80 81 82 83 84 85
    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.
86
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
87 88
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
89 90
          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
91
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
92
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
93 94
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
95 96
          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
97
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
98
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
99 100
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
101
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
102 103
          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
104 105 106 107
      - 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.
108
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
109 110
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
111 112
          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
113
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
114
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
115 116
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
117 118
          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
119
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
120
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
121 122
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
123
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
124 125
          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
126 127 128 129 130 131 132 133 134 135 136 137 138
    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.
139 140
        + 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
141
          apply EQφ, Hφ; now eauto with arith.
142 143
        + 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
144
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
145 146
        + 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
147 148
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
      - split; [| split]; intros.
149 150
        + 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
151
          apply EQφ, Hφ; now eauto with arith.
152 153
        + 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
154
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
155 156
        + 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
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
          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].
175 176
        + 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
177
          eapply (EQWP _ _ _), HWP; now eauto with arith.
178 179
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
180
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
181
      - split; [assumption | split; intros].
182 183
        + 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
184
          eapply (EQWP _ _ _), HWP; now eauto with arith.
185 186
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
187
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
188 189 190 191 192 193 194
    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].
195 196
        + 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
197
          eapply EQWP, HWP; now eauto with arith.
198 199
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
200
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
201
      - split; [assumption | split; intros].
202 203
        + 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
204
          eapply EQWP, HWP; now eauto with arith.
205 206
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; split; [assumption |].
207
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
208 209 210 211 212 213
    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 φ).
214

Filip Sieczkowski's avatar
Filip Sieczkowski committed
215
  End HoareTriples.
216

217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
  Section Soundness.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.
    Local Open Scope list_scope.

    Inductive stepn : nat -> cfg -> cfg -> Prop :=
    | stepn_O ρ : stepn O ρ ρ
    | stepn_S ρ1 ρ2 ρ3 n
              (HS  : step ρ1 ρ2)
              (HSN : stepn n ρ2 ρ3) :
        stepn (S n) ρ1 ρ3.

    Inductive wptp (m : mask) (w : Wld) (n : nat) : tpool -> list res -> Prop :=
    | wp_emp : wptp m w n nil nil
    | wp_cons e r tp rs
              (WPE  : wp m e (umconst ) w n r)
              (WPTP : wptp m w n tp rs) :
        wptp m w n (e :: tp) (r :: rs).

238
    (* Trivial lemmas about split over append *)
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
    Lemma wptp_app m w n tp1 tp2 rs1 rs2
          (HW1 : wptp m w n tp1 rs1)
          (HW2 : wptp m w n tp2 rs2) :
      wptp m w n (tp1 ++ tp2) (rs1 ++ rs2).
    Proof.
      induction HW1; [| constructor]; now trivial.
    Qed.

    Lemma wptp_app_tp m w n t1 t2 rs
          (HW : wptp m w n (t1 ++ t2) rs) :
      exists rs1 rs2, rs1 ++ rs2 = rs /\ wptp m w n t1 rs1 /\ wptp m w n t2 rs2.
    Proof.
      revert rs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
      - exists (@nil res) (@nil res); now auto using wptp.
      - exists (@nil res); simpl; now eauto using wptp.
      - apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [EQrs [WP1 WP2] ] ] ]; clear IHt1.
        exists (r :: rs1) rs2; simpl; subst; now auto using wptp.
    Qed.

    Lemma comp_list_app rs1 rs2 :
      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
    Proof.
      induction rs1; simpl comp_list; [now rewrite pcm_op_unit by apply _ |].
      now rewrite IHrs1, assoc.
    Qed.

265 266 267 268 269 270 271 272 273 274 275
    (* Closure under future worlds and smaller steps *)
    Lemma wptp_closure m (w1 w2 : Wld) n1 n2 tp rs
          (HSW : w1  w2) (HLe : n2 <= n1)
          (HW : wptp m w1 n1 tp rs) :
      wptp m w2 n2 tp rs.
    Proof.
      induction HW; constructor; [| assumption].
      eapply uni_pred; [eassumption | reflexivity |].
      rewrite <- HSW; assumption.
    Qed.

276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.

    Lemma unfold_wp m :
      wp m == (wpF m) (wp m).
    Proof.
      unfold wp; apply fixp_eq.
    Qed.

    Lemma sound_tp m n k e e' tp tp' σ σ' φ w r rs s
          (HSN  : stepn n (e :: tp, σ) (e' :: tp', σ'))
          (HV   : is_value e')
          (HWE  : wp m e φ w (n + S k) r)
          (HWTP : wptp m w (n + S k) tp rs)
          (HE   : erasure σ m (Some r · comp_list rs) s w @ n + S k) :
      exists w' r' s',
        w  w' /\ φ (exist _ e' HV) w' (S k) r' /\ erasure σ' m (Some r') s' w' @ S k.
    Proof.
      revert e tp σ w r rs s HSN HWE HWTP HE; induction n using wf_nat_ind; rename H into HInd.
      intros; inversion HSN; subst; clear HSN.
      (* e is a value *)
      { rename e' into e; clear HInd HWTP; simpl plus in *; rewrite unfold_wp in HWE.
297 298 299
        edestruct (HWE w k) as [HVal _];
          [reflexivity | unfold lt; reflexivity | apply mask_emp_disjoint
           | rewrite mask_emp_union; eassumption |].
300
        specialize (HVal HV); destruct HVal as [w' [r' [s' [HSW [Hφ HE'] ] ] ] ].
301
        rewrite mask_emp_union in HE'; destruct (Some r' · comp_list rs) as [r'' |] eqn: EQr.
302 303 304 305 306 307 308 309 310 311 312
        - exists w' r'' s'; split; [assumption | split; [| assumption] ].
          eapply uni_pred, Hφ; [reflexivity |].
          rewrite ord_res_optRes; exists (comp_list rs); rewrite comm, EQr; reflexivity.
        - exfalso; eapply erasure_not_empty, HE'.
          now erewrite pcm_op_zero by apply _.
      }
      rename n0 into n; specialize (HInd n (le_n _)); inversion HS; subst; clear HS.
      (* atomic step *)
      { destruct t1 as [| ee t1]; inversion H0; subst; clear H0.
        (* step in e *)
        - simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [HS _] ];
313
          [reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
314
          edestruct HS as [w' [r' [s' [HSW [HWE' HE'] ] ] ] ]; [reflexivity | eassumption | clear HS HWE HE].
315
          rewrite mask_emp_union in HE'; setoid_rewrite HSW; eapply HInd; try eassumption.
316 317 318 319 320
          eapply wptp_closure, HWTP; [assumption | now auto with arith].
        (* step in a spawned thread *)
        - apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
          inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
          edestruct (WPE w (n + S k) s (Some r · comp_list (rs1 ++ rs0))) as [_ [HS _] ];
321 322
            [reflexivity | apply le_n | apply mask_emp_disjoint
             | eapply erasure_equiv, HE; try reflexivity; [apply mask_emp_union |] |].
323 324 325 326 327 328 329 330 331
          + rewrite !comp_list_app; simpl comp_list; unfold equiv.
            rewrite assoc, (comm (Some r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
            now rewrite assoc, (comm (Some r0)), <- assoc.
          + edestruct HS as [w' [r0' [s' [HSW [WPE' HE'] ] ] ] ];
            [reflexivity | eassumption | clear WPE HS].
            setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
            * rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
            * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
            constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
332
          * eapply erasure_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
333 334 335 336 337 338 339 340
            rewrite assoc, (comm (Some r0')), <- assoc; apply pcm_op_equiv; [reflexivity |].
            rewrite !comp_list_app; simpl comp_list.
            now rewrite assoc, (comm (comp_list rs1)), <- assoc.
      }
      (* fork *)
      destruct t1 as [| ee t1]; inversion H; subst; clear H.
      (* fork from e *)
      - simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [_ HF] ];
341
        [reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
342 343 344 345
        specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [s' [HSW [HWE' [HWFK HE'] ] ] ] ] ] ].
        clear HWE HE; setoid_rewrite HSW; eapply HInd with (rs := rs ++ [rfk]); try eassumption; [|].
        + apply wptp_app; [| now auto using wptp].
          eapply wptp_closure, HWTP; [assumption | now auto with arith].
346
        + eapply erasure_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
347 348 349 350 351 352 353
          rewrite (comm (Some rfk)), <- assoc; apply pcm_op_equiv; [reflexivity |].
          rewrite comp_list_app; simpl comp_list; rewrite comm.
          now erewrite (comm _ 1), pcm_op_unit by apply _.
      (* fork from a spawned thread *)
      - apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
        inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
        edestruct (WPE w (n + S k) s (Some r · comp_list (rs1 ++ rs0))) as [_ [_ HF] ];
354 355
          [reflexivity | apply le_n | apply mask_emp_disjoint
           | eapply erasure_equiv, HE; try reflexivity; [apply mask_emp_union |] |].
356 357 358 359 360 361 362 363
        + rewrite assoc, (comm (Some r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
          rewrite !comp_list_app; simpl comp_list; now rewrite assoc, (comm (Some r0)), <- assoc.
        + specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [s' [HSW [WPE' [WPS HE'] ] ] ] ] ] ]; clear WPE.
          setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
          * rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
          * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
            constructor; [eassumption | apply wptp_app; [| now eauto using wptp] ].
            eapply wptp_closure, WPTP; [assumption | now auto with arith].
364
          * eapply erasure_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397
            rewrite (assoc _ (Some r)), (comm _ (Some r)), <- assoc.
            apply pcm_op_equiv; [reflexivity |].
            rewrite (comm (Some rfk)), <- assoc, comp_list_app; simpl comp_list.
            rewrite assoc, (comm _ (Some rret)), <- assoc.
            apply pcm_op_equiv; [reflexivity |].
            rewrite (comm (Some rfk)), !comp_list_app; simpl comp_list.
            rewrite assoc; apply pcm_op_equiv; [reflexivity |].
            now erewrite comm, pcm_op_unit by apply _.
    Qed.

    Lemma unit_min r : pcm_unit _  r.
    Proof.
      exists r; now erewrite comm, pcm_op_unit by apply _.
    Qed.

    (** This is a (relatively) generic soundness statement; one can
        simplify it for certain classes of assertions (e.g.,
        independent of the worlds) and obtain easy corollaries. *)
    Theorem soundness m e p φ n k e' tp σ σ' w r s
            (HT  : valid (ht m p e φ))
            (HSN : stepn n ([e], σ) (e' :: tp, σ'))
            (HV  : is_value e')
            (HP  : p w (n + S k) r)
            (HE  : erasure σ m (Some r) s w @ n + S k) :
      exists w' r' s',
        w  w' /\ φ (exist _ e' HV) w' (S k) r' /\ erasure σ' m (Some r') s' w' @ S k.
    Proof.
      specialize (HT w (n + S k) r).
      eapply sound_tp; [eassumption | | constructor | eapply erasure_equiv, HE; try reflexivity; [] ].
      - apply HT in HP; try reflexivity; [eassumption | apply unit_min].
      - simpl comp_list; now erewrite comm, pcm_op_unit by apply _.
    Qed.

398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417
    Program Definition cons_pred (φ : value -=> Prop): value -n> Props :=
      n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
    Next Obligation.
      firstorder.
    Qed.
    Next Obligation.
      intros x y  H_xy P n r. simpl. rewrite H_xy. tauto.
    Qed.
    Next Obligation.
      intros x y H_xy P m r. simpl in H_xy. destruct n.
      - intros LEZ. exfalso. omega.
      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
    Qed.

    Theorem soundness_obs m e (φ : value -=> Prop) n e' tp σ σ'
            (HT  : valid (ht m (ownS σ) e (cons_pred φ)))
            (HSN : stepn n ([e], σ) (e' :: tp, σ'))
            (HV : is_value e') :
        φ (exist _ e' HV).
    Proof.
418 419 420 421 422 423 424 425
      edestruct (soundness _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) 1 HT HSN) as [w [r [s [H_wle [H_phi _] ] ] ] ].
      - exists (pcm_unit _); now rewrite pcm_op_unit by apply _.
      - rewrite Plus.plus_comm; split.
        + assert (HS : Some (ex_own _ σ, pcm_unit _) · 1 = Some (ex_own _ σ, pcm_unit _));
          [| now setoid_rewrite HS].
          eapply ores_equiv_eq; now erewrite comm, pcm_op_unit by apply _.
        + exists (fdEmpty (V:=res)); split; [reflexivity|].
          intros i _; split; [reflexivity |].
426 427 428 429
          intros _ _ [].
      - exact H_phi.
    Qed.

430 431
  End Soundness.

432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455
  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.
456
      intros w' nn rr w _ n r' _ _ _; clear w' nn rr.
457
      rewrite unfold_wp; intros w'; intros; split; [| split]; intros.
458 459
      - exists w' r' s; split; [reflexivity | split; [| assumption] ].
        simpl; reflexivity.
460 461
      - contradiction (values_stuck _ HV _ _ HDec).
        repeat eexists; eassumption.
462 463 464 465 466 467 468
      - subst e; assert (HT := fill_value _ _ HV); subst K.
        revert HV; rewrite fill_empty; intros.
        contradiction (fork_not_value _ HV).
    Qed.

    Lemma wpO m e φ w r : wp m e φ w O r.
    Proof.
469
      rewrite unfold_wp; intros w'; intros; now inversion HLt.
470
    Qed.
471 472

    (** Bind **)
473 474 475 476

    (** Quantification in the logic works over nonexpansive maps, so
        we need to show that plugging the value into the postcondition
        and context is nonexpansive. *)
477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
    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.

492 493 494 495 496 497 498
    Lemma htBind P φ φ' K e m :
      ht m P e φ  all (plugV m φ φ' K)  ht m P (K [[ e ]]) φ'.
    Proof.
      intros wz nz rz [He HK] w HSw n r HLe _ HP.
      specialize (He _ HSw _ _ HLe (unit_min _) HP).
      rewrite HSw, <- HLe in HK; clear wz nz HSw HLe HP.
      revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
499
      rewrite unfold_wp in He; rewrite unfold_wp.
500 501 502 503 504 505
      destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
      - intros w'; intros; edestruct He as [HV _]; try eassumption; [].
        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [s' [HSw' [Hφ HE] ] ] ] ].
        (* Fold the goal back into a wp *)
        setoid_rewrite HSw'.
        assert (HT : wp m (K [[ e ]]) φ' w'' (S k) r');
506
          [| rewrite unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
507 508 509 510 511 512
        clear HE; specialize (HK (exist _ e HVal)).
        do 30 red in HK; unfold proj1_sig in HK.
        apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
      - intros w'; intros; edestruct He as [_ [HS HF] ]; try eassumption; [].
        split; [intros HVal; contradiction HNVal; assert (HT := fill_value _ _ HVal);
                subst K; rewrite fill_empty in HVal; assumption | split; intros].
513 514
        + clear He HF HE; edestruct step_by_value as [K' EQK];
          [eassumption | repeat eexists; eassumption | eassumption |].
515 516 517 518 519 520 521 522 523 524 525 526 527 528
          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
          edestruct HS as [w'' [r' [s' [HSw' [He HE] ] ] ] ]; try eassumption; [].
          subst e; clear HStep HS.
          do 3 eexists; split; [eassumption | split; [| eassumption] ].
          rewrite <- fill_comp; apply IH; try assumption; [].
          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
        + clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
          edestruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE] ] ] ] ] ] ];
            try eassumption; []; subst e; clear HF.
          do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
          rewrite <- fill_comp; apply IH; try assumption; [].
          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
    Qed.
529 530 531

    (** Consequence **)

532 533 534
    (** Much like in the case of the plugging, we need to show that
        the map from a value to a view shift between the applied
        postconditions is nonexpansive *)
535 536 537 538 539 540 541 542 543 544 545 546 547 548 549
    Program Definition vsLift m1 m2 φ φ' :=
      n[(fun v => vs m1 m2 (φ v) (φ' v))].
    Next Obligation.
      intros v1 v2 EQv; unfold vs.
      rewrite EQv; reflexivity.
    Qed.
    Next Obligation.
      intros v1 v2 EQv; unfold vs.
      rewrite EQv; reflexivity.
    Qed.

    Lemma htCons P P' φ φ' m e :
      vs m m P P'  ht m P' e φ'  all (vsLift m m φ' φ)  ht m P e φ.
    Proof.
      intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
550
      specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
551
      rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
552
      intros w'; intros; edestruct HP as [w'' [r' [s' [HSw' [Hp' HE'] ] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
553 554 555
      clear HP HE; rewrite HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
      setoid_rewrite HSw'.
      assert (HT : wp m e φ w'' (S k) r');
556
        [| rewrite unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
557 558 559 560 561
      unfold lt in HLt; rewrite HSw, HSw', <- HLt in Hφ; clear - He Hφ.
      (* Second phase of the proof: got rid of the preconditions,
         now induction takes care of the evaluation. *)
      rename r' into r; rename w'' into w.
      revert w r e He Hφ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
562
      rename H into IH; intros; rewrite unfold_wp; rewrite unfold_wp in He.
563 564 565 566
      intros w'; intros; edestruct He as [HV [HS HF] ]; try eassumption; [].
      split; [intros HVal; clear HS HF IH | split; intros; [clear HV HF | clear HV HS] ].
      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [s' [HSw' [Hφ' HE] ] ] ] ].
        eapply Hφ in Hφ'; [| etransitivity; eassumption | apply HLt | apply unit_min].
567 568 569
        clear w n HSw Hφ HLt; edestruct Hφ' as [w [r'' [s'' [HSw [Hφ HE'] ] ] ] ];
        [reflexivity | apply le_n | rewrite mask_union_idem; eassumption | eassumption |].
        exists w r'' s''; split; [etransitivity; eassumption | split; assumption].
570
      - clear HE He; edestruct HS as [w'' [r' [s' [HSw' [He HE] ] ] ] ];
571
        try eassumption; clear HS.
572 573 574
        do 3 eexists; split; [eassumption | split; [| eassumption] ].
        apply IH; try assumption; [].
        unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
575
      - clear HE He; edestruct HF as [w'' [rfk [rret [s' [HSw' [HWF [HWR HE] ] ] ] ] ] ]; [eassumption |].
576 577 578 579
        clear HF; do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
        apply IH; try assumption; [].
        unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
    Qed.
580

581
    Lemma htACons m m' e P P' φ φ'
582
          (HAt   : atomic e)
583 584 585 586
          (HSub  : m'  m) :
      vs m m' P P'  ht m' P' e φ'  all (vsLift m' m φ' φ)  ht m P e φ.
    Proof.
      intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
587
      specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
588 589 590
      split; [intros HV; contradiction (atomic_not_value e) |].
      split; [| intros; subst; contradiction (fork_not_atomic K e') ].
      intros; rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
591 592 593 594
      edestruct HP as [w'' [r' [s' [HSw' [Hp' HE'] ] ] ] ]; try eassumption; [|].
      { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
        destruct Hmm'; [| apply HSub]; assumption.
      }
595 596
      clear HP HE; rewrite HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
      unfold lt in HLt; rewrite HSw0, <- HLt in Hφ; clear w n HSw0 HLt Hp'.
597 598
      rewrite unfold_wp in He; edestruct He as [_ [HS _] ];
        [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
599 600
      edestruct HS as [w [r'' [s'' [HSw [He' HE] ] ] ] ]; try eassumption; clear He HS HE'.
      destruct k as [| k]; [exists w' r' s'; split; [reflexivity | split; [apply wpO | exact I] ] |].
601 602 603
      assert (HNV : ~ is_value ei)
        by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
      subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
604
      rewrite fill_empty in *; rename ei into e.
605
      setoid_rewrite HSw'; setoid_rewrite HSw.
606 607 608 609
      assert (HVal := atomic_step _ _ _ _ HAt HStep).
      rewrite HSw', HSw in Hφ; clear - HE He' Hφ HSub HVal HD.
      rewrite unfold_wp in He'; edestruct He' as [HV _];
      [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
610 611
      clear HE He'; specialize (HV HVal); destruct HV as [w' [r [s [HSw [Hφ' HE] ] ] ] ].
      eapply Hφ in Hφ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
612 613 614 615 616
      clear Hφ; edestruct Hφ' as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ];
        [reflexivity | apply le_n | | eassumption |].
      { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
        destruct Hmm'; [apply HSub |]; assumption.
      }
617
      clear Hφ' HE; exists w'' r' s'; split;
618 619
      [etransitivity; eassumption | split; [| eassumption] ].
      clear - Hφ; rewrite unfold_wp; intros w; intros; split; [intros HVal' | split; intros; exfalso].
620 621 622
      - do 3 eexists; split; [reflexivity | split; [| eassumption] ].
        unfold lt in HLt; rewrite HLt, <- HSw.
        eapply φ, Hφ; [| apply le_n]; simpl; reflexivity.
623
      - eapply values_stuck; [.. | repeat eexists]; eassumption.
624 625 626
      - clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
        rewrite fill_empty in HVal; now apply fork_not_value in HVal.
    Qed.
627 628

    (** Framing **)
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659

    (** Helper lemma to weaken the region mask *)
    Lemma wp_mask_weaken m1 m2 e φ (HD : m1 # m2) :
      wp m1 e φ  wp (m1  m2) e φ.
    Proof.
      intros w n; revert w e φ; induction n using wf_nat_ind; rename H into HInd; intros w e φ r HW.
      rewrite unfold_wp; rewrite unfold_wp in HW; intros w'; intros.
      edestruct HW with (mf := mf  m2) as [HV [HS HF] ]; try eassumption;
      [| eapply erasure_equiv, HE; try reflexivity; [] |].
      { intros j [ [Hmf | Hm'] Hm]; [apply (HD0 j) | apply (HD j) ]; tauto.
      }
      { clear; intros j; tauto.
      }
      clear HW HE; split; [intros HVal; clear HS HF HInd | split; [intros; clear HV HF | intros; clear HV HS] ].
      - specialize (HV HVal); destruct HV as [w'' [r' [s' [HSW [Hφ HE] ] ] ] ].
        do 3 eexists; split; [eassumption | split; [eassumption |] ].
        eapply erasure_equiv, HE; try reflexivity; [].
        intros j; tauto.
      - edestruct HS as [w'' [r' [s' [HSW [HW HE] ] ] ] ]; try eassumption; []; clear HS.
        do 3 eexists; split; [eassumption | split; [eapply HInd, HW; assumption |] ].
        eapply erasure_equiv, HE; try reflexivity; [].
        intros j; tauto.
      - destruct (HF _ _ HDec) as [w'' [rfk [rret [s' [HSW [HWR [HWF HE] ] ] ] ] ] ]; clear HF.
        do 4 eexists; split; [eassumption |].
        do 2 (split; [apply HInd; eassumption |]).
        eapply erasure_equiv, HE; try reflexivity; [].
        intros j; tauto.
    Qed.

    Lemma htFrame m m' P R e φ (HD : m # m') :
      ht m P e φ  ht (m  m') (P * R) e (lift_bin sc φ (umconst R)).
660 661 662 663
    Proof.
      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
      specialize (He _ HSw _ _ HLe (unit_min _) HP).
      clear P w n rz HSw HLe HP; rename w' into w; rename n' into n.
664 665 666
      apply wp_mask_weaken; [assumption |]; revert e w r1 r EQr HLR He.
      induction n using wf_nat_ind; intros; rename H into IH.
      rewrite unfold_wp; rewrite unfold_wp in He; intros w'; intros.
667 668 669 670 671
      rewrite <- EQr, <- assoc in HE; edestruct He as [HV [HS HF] ]; try eassumption; [].
      clear He; split; [intros HVal; clear HS HF IH HE | split; intros; [clear HV HF HE | clear HV HS HE] ].
      - specialize (HV HVal); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE] ] ] ] ].
        rewrite assoc in HE; destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
        [| eapply erasure_not_empty in HE; [contradiction | now erewrite !pcm_op_zero by apply _] ].
672
        do 3 eexists; split; [eassumption | split; [| eassumption ] ].
673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689
        exists r1' r2; split; [now rewrite EQr' | split; [assumption |] ].
        unfold lt in HLt; rewrite HLt, <- HSw', <- HSw; apply HLR.
      - edestruct HS as [w'' [r1' [s' [HSw' [He HE] ] ] ] ]; try eassumption; []; clear HS.
        destruct k as [| k]; [exists w' r1' s'; split; [reflexivity | split; [apply wpO | exact I] ] |].
        rewrite assoc in HE; destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
        [| eapply erasure_not_empty in HE; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        do 3 eexists; split; [eassumption | split; [| eassumption] ].
        eapply IH; try eassumption; [rewrite <- EQr'; reflexivity |].
        unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWF [HWR HE] ] ] ] ] ] ].
        destruct k as [| k]; [exists w' rfk rret s'; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
        rewrite assoc, <- (assoc (Some rfk)) in HE; destruct (Some rret · Some r2) as [rret' |] eqn: EQrret;
        [| eapply erasure_not_empty in HE; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
        do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
        eapply IH; try eassumption; [rewrite <- EQrret; reflexivity |].
        unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
    Qed.
690

691 692
    Lemma htAFrame m m' P R e φ
          (HD  : m # m')
693
          (HAt : atomic e) :
694
      ht m P e φ  ht (m  m') (P *  R) e (lift_bin sc φ (umconst R)).
695 696 697
    Proof.
      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
      specialize (He _ HSw _ _ HLe (unit_min _) HP).
698
      clear rz n HLe; apply wp_mask_weaken; [assumption |]; rewrite unfold_wp.
699 700 701 702 703
      clear w HSw; rename n' into n; rename w' into w; intros w'; intros.
      split; [intros; exfalso | split; intros; [| exfalso] ].
      - contradiction (atomic_not_value e).
      - destruct k as [| k];
        [exists w' r s; split; [reflexivity | split; [apply wpO | exact I] ] |].
704
        rewrite unfold_wp in He; rewrite <- EQr, <- assoc in HE.
705 706 707 708 709 710 711
        edestruct He as [_ [HeS _] ]; try eassumption; [].
        edestruct HeS as [w'' [r1' [s' [HSw' [He' HE'] ] ] ] ]; try eassumption; [].
        clear HE He HeS; rewrite assoc in HE'.
        destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
          [| eapply erasure_not_empty in HE';
             [contradiction | now erewrite !pcm_op_zero by apply _] ].
        do 3 eexists; split; [eassumption | split; [| eassumption] ].
712 713 714
        assert (HNV : ~ is_value ei)
          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
715
        rewrite fill_empty in *.
716
        unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
717 718 719 720 721
        assert (HVal := atomic_step _ _ _ _ HAt HStep).
        clear - He' HVal EQr' HLR; rename w'' into w; rewrite unfold_wp; intros w'; intros.
        split; [intros HV; clear HVal | split; intros; exfalso].
        + rewrite unfold_wp in He'; rewrite <- EQr', <- assoc in HE; edestruct He' as [HVal _]; try eassumption; [].
          specialize (HVal HV); destruct HVal as [w'' [r1'' [s'' [HSw' [Hφ HE'] ] ] ] ].
722 723 724 725 726 727
          rewrite assoc in HE'; destruct (Some r1'' · Some r2) as [r'' |] eqn: EQr'';
          [| eapply erasure_not_empty in HE';
             [contradiction | now erewrite !pcm_op_zero by apply _] ].
          do 3 eexists; split; [eassumption | split; [| eassumption] ].
          exists r1'' r2; split; [now rewrite EQr'' | split; [assumption |] ].
          unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
728 729
        + eapply values_stuck; [.. | repeat eexists]; eassumption.
        + subst; clear -HVal.
730 731 732 733
          assert (HT := fill_value _ _ HVal); subst K; rewrite fill_empty in HVal.
          contradiction (fork_not_value e').
      - subst; clear -HAt; eapply fork_not_atomic; eassumption.
    Qed.
734 735

    (** Fork **)
736
    Lemma htFork m P R e :
737
      ht m P e (umconst )  ht m ( P *  R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
738 739
    Proof.
      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
740 741 742 743
      destruct n' as [| n']; [apply wpO |].
      simpl in HP; specialize (He _ HSw _ _ (Le.le_Sn_le _ _ HLe) (unit_min _) HP).
      clear rz n HLe; rewrite unfold_wp.
      clear w HSw HP; rename n' into n; rename w' into w; intros w'; intros.
744 745
      split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso |] ].
      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite fill_empty in HDec; subst.
746
        eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
747 748
      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite fill_empty in HDec.
        apply fork_inj in HDec; subst e'; rewrite <- EQr in HE.
749 750
        unfold lt in HLt; rewrite <- (le_S_n _ _ HLt), HSw in He.
        simpl in HLR; rewrite <- Le.le_n_Sn in HE.
751
        do 4 eexists; split; [reflexivity | split; [| split; eassumption] ].
752
        rewrite fill_empty; rewrite unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
753 754 755 756 757
        clear - HLR; intros w''; intros; split; [intros | split; intros; exfalso].
        + do 3 eexists; split; [reflexivity | split; [| eassumption] ].
          exists (pcm_unit _) r2; split; [now erewrite pcm_op_unit by apply _ |].
          split; [| unfold lt in HLt; rewrite <- HLt, HSw in HLR; apply HLR].
          simpl; reflexivity.
758
        + eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
759 760 761 762 763
        + assert (HV := fork_ret_is_value); rewrite HDec in HV; clear HDec.
          assert (HT := fill_value _ _ HV);subst K; rewrite fill_empty in HV.
          eapply fork_not_value; eassumption.
    Qed.

764 765
  End HoareTripleProperties.

766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786
  Section DerivedRules.
    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).

    Lemma vsFalse m1 m2 :
      valid (vs m1 m2  ).
    Proof.
      rewrite valid_iff, box_top.
      unfold vs; apply box_intro.
      rewrite <- and_impl, and_projR.
      apply bot_false.
    Qed.

  End DerivedRules.

Ralf Jung's avatar
Ralf Jung committed
787
End IrisWP.