iris_core.v 16.2 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import ssreflect.
2
Require Import world_prop core_lang masks.
3 4
Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.

Ralf Jung's avatar
Ralf Jung committed
5 6
Set Bullet Behavior "Strict Subproofs".

7 8 9 10 11 12 13 14
Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
  Instance state_type : Setoid C.state := discreteType.
  
  Definition res := (ra_res_ex C.state * RL.res)%type.
  Instance res_type : Setoid res := _.
  Instance res_op   : RA_op res := _.
  Instance res_unit : RA_unit res := _.
  Instance res_valid: RA_valid res := _.
15
  Instance res_ra   : RA res := _.
16 17 18

  (* The order on (ra_pos res) is inferred correctly, but this one is not *)
  Instance res_pord: preoType res := ra_preo res.
19
End IrisRes.
20

21
Module IrisCore (RL : RA_T) (C : CORE_LANG).
22
  Export C.
Ralf Jung's avatar
Ralf Jung committed
23 24
  Module Export R  := IrisRes RL C.
  Module Export WP := WorldProp R.
25 26 27 28

  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

29
  (** Instances for a bunch of types (some don't even have Setoids) *)
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  Instance state_metr : metric state := discreteMetric.
  Instance state_cmetr : cmetric state := discreteCMetric.

  Instance logR_metr : metric RL.res := discreteMetric.
  Instance logR_cmetr : cmetric RL.res := discreteCMetric.

  Instance nat_type : Setoid nat := discreteType.
  Instance nat_metr : metric nat := discreteMetric.
  Instance nat_cmetr : cmetric nat := discreteCMetric.

  Instance expr_type : Setoid expr := discreteType.
  Instance expr_metr : metric expr := discreteMetric.
  Instance expr_cmetr : cmetric expr := discreteCMetric.

  (* We use this type quite a bit, so give it and its instances names *)
  Definition vPred := value -n> Props.
  Instance vPred_type  : Setoid vPred  := _.
  Instance vPred_metr  : metric vPred  := _.
  Instance vPred_cmetr : cmetric vPred := _.
49 50 51 52 53 54 55 56 57 58 59 60


  (** 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 := _.
61
  
62 63 64 65 66 67 68 69 70
  (** And now we're ready to build the IRIS-specific connectives! *)

  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.

    Program Definition box : Props -n> Props :=
71
      n[(fun p => m[(fun w => mkUPred (fun n r => p w n ra_pos_unit) _)])].
72
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
73
      intros n m r s HLe _ Hp; rewrite-> HLe; assumption.
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
    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}.

94
    Program Definition intEqP (t1 t2 : T) : UPred pres :=
95 96
      mkUPred (fun n r => t1 = S n = t2) _.
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
97
      intros n1 n2 _ _ HLe _; apply mono_dist; omega.
98 99 100 101 102 103 104 105 106
    Qed.

    Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).

    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.
Ralf Jung's avatar
Ralf Jung committed
107
      - rewrite ->EQl, EQr; assumption.
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
    Qed.

    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.

  Section Invariants.

    (** Invariants **)
127
    Definition invP (i : nat) (p : Props) (w : Wld) : UPred pres :=
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
      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 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 invP; simpl morph.
      apply intEq_dist; [reflexivity |].
      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
    Qed.

  End Invariants.

  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.
David Swasey's avatar
David Swasey committed
160
  Notation "∃ x , p" := (xist n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
161
  Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
David Swasey's avatar
David Swasey committed
162
  Notation "∃ x : T , p" := (xist n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
163 164 165 166 167 168 169 170 171

  Lemma valid_iff p :
    valid p <-> (  p).
  Proof.
    split; intros Hp.
    - intros w n r _; apply Hp.
    - intros w n r; apply Hp; exact I.
  Qed.

172 173
  Section Ownership.
    Local Open Scope ra.
174

175 176 177 178
    (** Ownership **)
    (* We define this on *any* resource, not just the positive (valid) ones.
       Note that this makes ownR trivially *False* for invalid u: There is no
       elment v such that u · v = r (where r is valid) *)
Ralf Jung's avatar
Ralf Jung committed
179 180
    Program Definition ownR: res -=> Props :=
      s[(fun u => pcmconst (mkUPred(fun n r => u  ra_proj r) _) )].
181 182 183 184
    Next Obligation.
      intros n m r1 r2 Hle [d Hd ] [e He]. change (u  (ra_proj r2)). rewrite <-Hd, <-He.
      exists (d · e). rewrite assoc. reflexivity.
    Qed.
Ralf Jung's avatar
Ralf Jung committed
185 186 187 188 189 190 191 192
    Next Obligation.
      intros u1 u2 Hequ. intros w n r. split; intros [t Heqt]; exists t; [rewrite <-Hequ|rewrite Hequ]; assumption.
    Qed.

    Lemma ownR_sc u t:
      ownR (u · t) == ownR u * ownR t.
    Proof.
      intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
Ralf Jung's avatar
Ralf Jung committed
193
      - destruct Hut as [s Heq]. rewrite-> assoc in Heq.
194 195
        exists (s · u) by auto_valid.
        exists t by auto_valid.
Ralf Jung's avatar
Ralf Jung committed
196 197 198 199 200 201 202 203 204 205
        split; [|split].
        + rewrite <-Heq. reflexivity.
        + exists s. reflexivity.
        + do 13 red. reflexivity.
      - destruct Hu as [u' Hequ]. destruct Ht as [t' Heqt].
        exists (u' · t'). rewrite <-EQr, <-Hequ, <-Heqt.
        rewrite !assoc. eapply ra_op_proper; try (reflexivity || now apply _).
        rewrite <-assoc, (comm _ u), assoc. reflexivity.
    Qed.

206
    Lemma ownR_valid u (INVAL: ~u):
Ralf Jung's avatar
Ralf Jung committed
207 208 209
      ownR u  .
    Proof.
      intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq.
210
      rewrite <-Heq in VAL. apply ra_op_valid2 in VAL. contradiction.
Ralf Jung's avatar
Ralf Jung committed
211
    Qed.
212

213 214 215 216 217
    (** Proper physical state: ownership of the machine state **)
    Program Definition ownS : state -n> Props :=
      n[(fun s => ownR (ex_own _ s, 1%ra))].
    Next Obligation.
      intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
Ralf Jung's avatar
Ralf Jung committed
218
      rewrite EQr. reflexivity.
219
    Qed.
220

221 222
    (** Proper ghost state: ownership of logical **)
    Program Definition ownL : RL.res -n> Props :=
Ralf Jung's avatar
Ralf Jung committed
223
      n[(fun r => ownR (1%ra, r))].
224 225 226 227
    Next Obligation.
      intros r1 r2 EQr. destruct n as [| n]; [apply dist_bound |eapply dist_refl].
      simpl in EQr. intros w m t. simpl. change ( (ex_unit state, r1)  (ra_proj t) <->  (ex_unit state, r2)  (ra_proj t)). rewrite EQr. reflexivity.
    Qed.
228

229 230 231 232
    (** Ghost state ownership **)
    Lemma ownL_sc (u t : RL.res) :
      ownL (u · t) == ownL u * ownL t.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
233 234 235 236 237
      assert (Heq: (ex_unit state, u · t) == ((ex_unit state, u) · (ex_unit state, t)) ) by reflexivity.
      (* I cannot believe I have to write this... *)
      change (ownR (ex_unit state, u · t) == ownR (ex_unit state, u) * ownR (ex_unit state, t)).
      rewrite Heq.
      now eapply ownR_sc.
238 239 240
    Qed.

  End Ownership.
241 242 243 244 245 246 247 248 249 250 251 252 253

  (** 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 |].
254
    now eapply unit_min.
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
  Qed.

  Lemma box_top :  ==  .
  Proof.
    intros w n r; simpl; unfold const; reflexivity.
  Qed.

  Lemma box_disj p q :
     (p  q) ==  p   q.
  Proof.
    intros w n r; reflexivity.
  Qed.

  (** Timeless *)

  Definition timelessP (p : Props) w n :=
    forall w' k r (HSw : w  w') (HLt : k < n) (Hp : p w' k r), p w' (S k) r.

  Program Definition timeless (p : Props) : Props :=
    m[(fun w => mkUPred (fun n r => timelessP p w n) _)].
  Next Obligation.
    intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
Ralf Jung's avatar
Ralf Jung committed
277
    omega.
278 279 280 281 282 283 284 285 286 287 288 289 290 291
  Qed.
  Next Obligation.
    intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
    split; intros HT w' m r HSw HLt' Hp.
    - symmetry in EQw; assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
      apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
    - assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
      apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
  Qed.
  Next Obligation.
    intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp.
    eapply HT, Hp; [etransitivity |]; eassumption.
  Qed.

292
  Section WorldSatisfaction.
293
    Local Open Scope ra_scope.
294 295
    Local Open Scope bi_scope.

296
    (* First, we need to compose the resources of a finite map. This won't be pretty, for
297 298 299 300
       now, since the library does not provide enough
       constructs. Hopefully we can provide a fold that'd work for
       that at some point
     *)
301
    Fixpoint comp_list (xs : list pres) : res :=
302 303
      match xs with
        | nil => 1
304
        | (x :: xs)%list => ra_proj x · comp_list xs
305 306
      end.

307 308 309
    Lemma comp_list_app rs1 rs2 :
      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
310 311
      induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
      now rewrite ->IHrs1, assoc.
312 313
    Qed.

314 315
    Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
    Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
316

Ralf Jung's avatar
Ralf Jung committed
317
    Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
318
      comp_map rs == ra_proj r · comp_map (fdRemove i rs).
319
    Proof.
320
      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
Ralf Jung's avatar
Ralf Jung committed
321 322 323 324
      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
      simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
      rewrite-> !assoc, (comm (_ s)); reflexivity.
325 326
    Qed.

Ralf Jung's avatar
Ralf Jung committed
327
    Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
328
      ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
329
    Proof.
330
      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
331
      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
Ralf Jung's avatar
Ralf Jung committed
332
      destruct (comp i j); [contradiction | reflexivity |].
333
      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
Ralf Jung's avatar
Ralf Jung committed
334
      rewrite-> !assoc, (comm (_ r)); reflexivity.
335 336
    Qed.

337
    Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
Ralf Jung's avatar
Ralf Jung committed
338
          (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
339
      ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
340
    Proof.
341
      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
Ralf Jung's avatar
Ralf Jung committed
342 343 344
      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
      - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
345
      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
Ralf Jung's avatar
Ralf Jung committed
346
        rewrite-> !assoc, (comm (_ r2)); reflexivity.
347 348
    Qed.

349
    Definition state_sat (r: res) σ: Prop := r /\
Ralf Jung's avatar
Ralf Jung committed
350 351
      match fst r with
        | ex_own s => s = σ
352 353
        | _ => True
      end.
354 355 356

    Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
    Proof.
357
      intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
358
    Qed.
359 360 361

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

362 363
    Program Definition wsat (σ : state) (m : mask) (r : res) (w : Wld) : UPred () :=
       (mkUPred (fun n _ => exists rs : nat -f> pres,
364 365
                    state_sat (r · (comp_map rs)) σ
                      /\ forall i (Hm : m i),
366 367 368 369
                           (i  dom rs <-> i  dom w) /\
                           forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
                             ı π w n ri) _).
    Next Obligation.
370
      intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
371 372 373
      setoid_rewrite HLe; eassumption.
    Qed.

374
    Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
375
    Proof.
376
      intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |].
377
      split; intros [rs [HE HM] ]; exists rs.
378
      - split; [rewrite <-EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
379 380
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
381
      - split; [rewrite EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
382 383 384 385
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
    Qed.

386
    Global Instance wsat_dist n σ m r : Proper (dist n ==> dist n) (wsat σ m r).
387 388
    Proof.
      intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
389
      split; intros [rs [HE HM] ]; exists rs.
390 391
      - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
Ralf Jung's avatar
Ralf Jung committed
392
        assert (EQπ := EQw i); rewrite-> HLw in EQπ; clear HLw.
393 394
        destruct (w1 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
Ralf Jung's avatar
Ralf Jung committed
395
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
396 397 398
        apply HR; [reflexivity | assumption].
      - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
Ralf Jung's avatar
Ralf Jung committed
399
        assert (EQπ := EQw i); rewrite-> HLw in EQπ; clear HLw.
400 401
        destruct (w2 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
Ralf Jung's avatar
Ralf Jung committed
402
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
403 404 405
        apply HR; [reflexivity | assumption].
    Qed.

Ralf Jung's avatar
Ralf Jung committed
406
    Lemma wsat_valid σ m (r: res) w k :
407
      wsat σ m r w (S k) tt -> r.
408
    Proof.
409
      intros [rs [HD _] ]. destruct HD as [VAL _].
410
      eapply ra_op_valid; [now apply _|]. eassumption.
411 412
    Qed.

413
  End WorldSatisfaction.
414 415 416

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

Ralf Jung's avatar
Ralf Jung committed
417
End IrisCore.