ModelCredits.v 24.3 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(** 

This file formalizes "Separation Logic with Time Credits",
following the presentation by Arthur Charguéraud and 
François Pottier described in the following papers:


- Machine-Checked Verification of the Correctness and Amortized 
  Complexity of an Efficient Union-Find Implementation (ITP'15)

- Verifying the Correctness and Amortized Complexity of a Union-Find 
  Implementation in Separation Logic with Time Credits
  (Draft journal paper)

Author: Arthur Charguéraud.
License: MIT.

*)


charguer's avatar
charguer committed
21 22
Set Implicit Arguments.
Require Import LibCore Shared ModelLambda.
charguer's avatar
charguer committed
23
Open Scope state_scope.
charguer's avatar
charguer committed
24

charguer's avatar
charguer committed
25

charguer's avatar
charguer committed
26 27 28
(********************************************************************)
(* ** Semantics, extended *)

charguer's avatar
charguer committed
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions
    (used by the formalization of Separation Logic with time credits) *)

Section Redn.
Local Open Scope nat_scope.
Local Open Scope state_scope.

Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
  | redn_val : forall m v,
      redn 0 m (trm_val v) m v
  | redn_if : forall n m1 m2 v r t1 t2,
      redn n m1 (If v = val_int 0 then t2 else t1) m2 r ->
      redn n m1 (trm_if v t1 t2) m2 r
  | redn_let : forall n1 n2 m1 m2 m3 x t1 t2 v1 r,
      redn n1 m1 t1 m2 v1 ->
      redn n2 m2 (subst_trm x v1 t2) m3 r ->
      redn (n1+n2) m1 (trm_let x t1 t2) m3 r
  | redn_app : forall n m1 m2 v1 v2 f x t r,
      v1 = val_fix f x t ->
      redn n m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
      redn (S n) m1 (trm_app v1 v2) m2 r
charguer's avatar
charguer committed
51 52 53
  | redn_new : forall ma mb v l,
      mb = (state_single l v) ->
      \# ma mb ->
54
      redn 0 ma (prim_new v) (mb \+ ma) (val_loc l)
charguer's avatar
charguer committed
55 56
  | redn_get : forall m l v,
      state_data m l = Some v ->
57
      redn 0 m (prim_get (val_loc l)) m v
charguer's avatar
charguer committed
58 59
  | redn_set : forall m m' l v,
      m' = state_update m l v ->
60
      redn 0 m (prim_set (val_pair (val_loc l) v)) m' val_unit.
charguer's avatar
charguer committed
61

charguer's avatar
charguer committed
62 63
End Redn.

charguer's avatar
charguer committed
64 65 66 67 68 69
Ltac state_red_base tt ::=
  match goal with H: redn _ _ ?t _ _ |- redn _ _ ?t _ _ =>
    applys_eq H 2 4; try state_eq end.



charguer's avatar
charguer committed
70 71 72
(********************************************************************)
(* ** Heaps *)

charguer's avatar
charguer committed
73 74 75 76 77 78 79 80 81 82 83 84
(*------------------------------------------------------------------*)
(* ** Representation of credits *)

(** Representation of credits *)

Definition credits : Type := nat.

(** Zero and one credits *)

Definition credits_zero : credits := 0%nat.
Definition credits_one : credits := 1%nat.

charguer's avatar
charguer committed
85 86 87 88 89 90

(*------------------------------------------------------------------*)
(* ** Representation of heaps *)

(** Representation of heaps *)

charguer's avatar
charguer committed
91
Definition heap : Type := (state * credits)%type.
charguer's avatar
charguer committed
92

charguer's avatar
charguer committed
93 94 95 96 97
(** Empty heap *)

Definition heap_empty : heap :=
  (state_empty, 0%nat). 

charguer's avatar
charguer committed
98 99 100 101 102 103 104 105
(** Projections *)

Coercion heap_state (h:heap) : state :=
  match h with (m,c) => m end.

Definition heap_credits (h:heap) : credits :=
  match h with (m,c) => c end.

charguer's avatar
charguer committed
106 107 108 109 110 111 112 113
Notation "h '^s'" := (heap_state h)
   (at level 9, format "h '^s'") : heap_scope.

Notation "h '^c'" := (heap_credits h)
   (at level 9, format "h '^c'") : heap_scope.

Open Scope heap_scope.

charguer's avatar
charguer committed
114 115 116
(** Disjoint heaps *)

Definition heap_disjoint (h1 h2 : heap) : Prop :=
charguer's avatar
charguer committed
117 118 119 120
  \# (h1^s) (h2^s).

Notation "\# h1 h2" := (heap_disjoint h1 h2)
  (at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
charguer's avatar
charguer committed
121 122 123 124

(** Union of heaps *)

Definition heap_union (h1 h2 : heap) : heap :=
charguer's avatar
charguer committed
125
   (h1^s \+ h2^s, (h1^c + h2^c)%nat).
charguer's avatar
charguer committed
126

charguer's avatar
charguer committed
127 128
Notation "h1 \u h2" := (heap_union h1 h2)
   (at level 51, right associativity) : heap_scope.
charguer's avatar
charguer committed
129 130 131 132 133 134 135 136 137


(*------------------------------------------------------------------*)
(* ** Definition of heap predicates *)

(** [hprop] is the type of predicates on heaps *)

Definition hprop := heap -> Prop.

charguer's avatar
charguer committed
138
(** Lifting of predicates *)
charguer's avatar
charguer committed
139

charguer's avatar
charguer committed
140
Definition hprop_pure (P:Prop) : hprop :=
charguer's avatar
charguer committed
141
  fun h => h = heap_empty /\ P.
charguer's avatar
charguer committed
142

charguer's avatar
charguer committed
143
(** Empty heap *)
charguer's avatar
charguer committed
144

charguer's avatar
charguer committed
145
Definition hprop_empty : hprop := 
charguer's avatar
charguer committed
146
  hprop_pure True.
charguer's avatar
charguer committed
147 148 149 150

(** Singleton heap *)

Definition hprop_single (l:loc) (v:val) : hprop := 
charguer's avatar
charguer committed
151 152
  fun h => h^s = state_single l v /\ h^c = credits_zero.

charguer's avatar
charguer committed
153 154 155
(** Heap union *)

Definition hprop_star (H1 H2 : hprop) : hprop := 
charguer's avatar
charguer committed
156 157 158 159 160
  fun h => exists h1 h2, 
              H1 h1 
           /\ H2 h2 
           /\ heap_disjoint h1 h2 
           /\ h = h1 \u h2.
charguer's avatar
charguer committed
161 162 163 164 165 166 167 168 169 170 171

(** Lifting of existentials *)

Definition hprop_exists A (Hof : A -> hprop) : hprop := 
  fun h => exists x, Hof x h.

(** Garbage collection predicate: [Hexists H, H]. *)

Definition hprop_gc : hprop := 
  hprop_exists (fun H => H).

charguer's avatar
charguer committed
172
(** Credits *)
charguer's avatar
charguer committed
173

charguer's avatar
charguer committed
174
Definition hprop_credits (n:nat) : hprop := 
charguer's avatar
charguer committed
175 176 177
  fun h => h^s = state_empty /\ h^c = n.

  (* DEPRECATED fun h => let (m,n') := h in m = state_empty /\ n' = n. *)
charguer's avatar
charguer committed
178

charguer's avatar
charguer committed
179
Global Opaque hprop_empty hprop_pure hprop_single 
charguer's avatar
charguer committed
180
              hprop_star hprop_exists hprop_gc hprop_credits. 
charguer's avatar
charguer committed
181 182 183 184 185 186 187 188


(*------------------------------------------------------------------*)
(* ** Notation for heap predicates *)

Notation "\[]" := (hprop_empty) 
  (at level 0) : heap_scope.

charguer's avatar
charguer committed
189
Notation "\[ P ]" := (hprop_pure P) 
charguer's avatar
charguer committed
190
  (at level 0, P at level 99) : heap_scope.
charguer's avatar
charguer committed
191

charguer's avatar
charguer committed
192 193 194
Notation "r '~~>' v" := (hprop_single r v)
  (at level 32, no associativity) : heap_scope.

charguer's avatar
charguer committed
195 196 197
Notation "H1 '\*' H2" := (hprop_star H1 H2)
  (at level 41, right associativity) : heap_scope.

charguer's avatar
charguer committed
198 199
Notation "Q \*+ H" := (fun x => hprop_star (Q x) H)
  (at level 40) : heap_scope.
charguer's avatar
charguer committed
200 201 202 203 204

Notation "'Hexists' x1 , H" := (hprop_exists (fun x1 => H))
  (at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (hprop_exists (fun x1:T1 => H))
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
charguer's avatar
charguer committed
205
Notation "'Hexists' ( x1 : T1 ) , H" := (hprop_exists (fun x1:T1 => H))
charguer's avatar
charguer committed
206 207
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.

charguer's avatar
charguer committed
208
Notation "\GC" := (hprop_gc) : heap_scope. 
charguer's avatar
charguer committed
209

charguer's avatar
charguer committed
210 211
Notation "'\$' n" := (hprop_credits n) 
  (at level 40, format "\$ n") : heap_scope.
charguer's avatar
charguer committed
212

charguer's avatar
charguer committed
213 214 215 216
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.

charguer's avatar
charguer committed
217 218

(********************************************************************)
charguer's avatar
charguer committed
219
(* ** Properties *)
charguer's avatar
charguer committed
220

charguer's avatar
charguer committed
221 222 223
(*------------------------------------------------------------------*)
(* ** Tactic for automation *)

charguer's avatar
charguer committed
224 225 226 227 228 229
Lemma heap_disjoint_def : forall h1 h2,
  heap_disjoint h1 h2 = state_disjoint (h1^s) (h2^s).
Proof using. auto. Qed.

Hint Rewrite heap_disjoint_def : rew_disjoint.

charguer's avatar
charguer committed
230 231 232 233 234
Tactic Notation "state_disjoint_pre" :=
  subst; rew_disjoint; jauto_set.

Hint Extern 1 (\# _ _) => state_disjoint_pre.

charguer's avatar
charguer committed
235 236
Ltac math_0 ::= unfolds credits.

charguer's avatar
charguer committed
237

charguer's avatar
charguer committed
238
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
239
(* ** Properties of [heap] *)
charguer's avatar
charguer committed
240

charguer's avatar
charguer committed
241 242 243 244 245 246 247 248 249 250 251 252 253 254
Lemma heap_eq : forall h1 h2,
  (h1^s = h2^s /\ h1^c = h2^c) -> h1 = h2.
Proof using.
  intros (s1,n1) (s2,n2) (M1&M2). simpls. subst. fequals.
Qed.

Lemma heap_eq_forward : forall h1 h2,
  h1 = h2 ->
  h1^s = h2^s /\ h1^c = h2^c.
Proof using. intros (s1,n1) (s2,n2) M. inverts~ M. Qed.


(*------------------------------------------------------------------*)
(* ** Properties of [heap_disjoint] *)
charguer's avatar
charguer committed
255 256 257

Lemma heap_disjoint_sym : forall h1 h2,
  \# h1 h2 -> \# h2 h1.
charguer's avatar
charguer committed
258 259 260 261
Proof using.
  intros [m1 n1] [m2 n2] H. simpls.
  hint state_disjoint_sym. autos*.
Qed.
charguer's avatar
charguer committed
262 263 264

Lemma heap_disjoint_comm : forall h1 h2,
  \# h1 h2 = \# h2 h1.
charguer's avatar
charguer committed
265 266 267 268
Proof using. 
  intros [m1 n1] [m2 n2]. simpls.
  hint state_disjoint_sym. extens*.
Qed. 
charguer's avatar
charguer committed
269 270 271

Lemma heap_disjoint_empty_l : forall h,
  \# heap_empty h.
charguer's avatar
charguer committed
272
Proof using. intros [m n]. hint state_disjoint_empty_l. simple*. Qed.
charguer's avatar
charguer committed
273 274 275

Lemma heap_disjoint_empty_r : forall h,
  \# h heap_empty.
charguer's avatar
charguer committed
276
Proof using. intros [m n]. hint state_disjoint_empty_r. simple*. Qed.
charguer's avatar
charguer committed
277 278

Lemma heap_disjoint_union_eq_r : forall h1 h2 h3,
charguer's avatar
charguer committed
279
  \# h1 (h2 \u h3) = (\# h1 h2 /\ \# h1 h3).
charguer's avatar
charguer committed
280 281 282 283 284 285 286
Proof using.
  intros [m1 n1] [m2 n2] [m3 n3].
  unfolds heap_disjoint, heap_union. simpls.
  rewrite state_disjoint_union_eq_r. extens*.
Qed.

Lemma heap_disjoint_union_eq_l : forall h1 h2 h3,
charguer's avatar
charguer committed
287
  \# (h2 \u h3) h1 = (\# h1 h2 /\ \# h1 h3).
charguer's avatar
charguer committed
288 289 290 291
Proof using.
  intros. rewrite heap_disjoint_comm. 
  apply heap_disjoint_union_eq_r.
Qed.
charguer's avatar
charguer committed
292

charguer's avatar
charguer committed
293 294 295 296
Hint Resolve 
   heap_disjoint_sym 
   heap_disjoint_empty_l heap_disjoint_empty_r
   heap_disjoint_union_eq_l heap_disjoint_union_eq_r.
charguer's avatar
charguer committed
297

charguer's avatar
charguer committed
298 299 300 301 302
Tactic Notation "rew_disjoint" :=
  autorewrite with rew_disjoint in *.
Tactic Notation "rew_disjoint" "*" :=
  rew_disjoint; auto_star.

charguer's avatar
charguer committed
303

charguer's avatar
charguer committed
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
(*------------------------------------------------------------------*)
(* ** Properties of [heap_union] *)

Lemma heap_union_comm : forall h1 h2,
  \# h1 h2 ->
  h1 \u h2 = h2 \u h1.
Proof using.
  intros [m1 n1] [m2 n2] H. unfold heap_union.
  simpl. fequals. state_eq. math.
Qed.

Lemma heap_union_assoc : forall h1 h2 h3,
  (h1 \u h2) \u h3 = h1 \u (h2 \u h3).
Proof using.
  intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_union.
  simpl. fequals. state_eq. math.
Qed.

Lemma heap_union_empty_l : forall h,
  heap_empty \u h = h.
Proof using. 
  intros [m n]. unfold heap_union, heap_empty. simpl.
  fequals. apply~ state_union_empty_l.
Qed.

Lemma heap_union_empty_r : forall h,
  h \u heap_empty = h.
Proof using. 
  intros. rewrite~ heap_union_comm. apply~ heap_union_empty_l.
Qed.

Lemma heap_union_state : forall h1 h2,
  heap_state (h1 \u h2) = (heap_state h1) \+ (heap_state h2).
Proof using. intros (m1&n1) (m2&n2). auto. Qed.

Lemma heap_union_credits : forall h1 h2,
  heap_credits (h1 \u h2) = (heap_credits h1 + heap_credits h2)%nat.
Proof using. intros (m1&n1) (m2&n2). auto. Qed.

Hint Resolve heap_union_comm
   heap_union_empty_l heap_union_empty_r.

charguer's avatar
charguer committed
346 347 348 349
Hint Rewrite heap_union_state : rew_disjoint.

Hint Rewrite heap_union_state : rew_state.

charguer's avatar
charguer committed
350 351 352 353
Hint Rewrite 
  heap_union_empty_l heap_union_empty_r
  heap_union_state heap_union_credits : rew_heap.

charguer's avatar
charguer committed
354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
Tactic Notation "rew_heap" :=
  autorewrite with rew_heap.
Tactic Notation "rew_heap" "~" :=
  rew_heap; auto_tilde.
Tactic Notation "rew_heap" "in" hyp(H) :=
  autorewrite with rew_heap in H.
Tactic Notation "rew_heap" "~" "in" hyp(H) :=
  rew_heap in H; auto_tilde.
Tactic Notation "rew_heap" "in" "*" :=
  autorewrite with rew_heap in *.
Tactic Notation "rew_heap" "~" "in" "*" :=
  rew_heap in *; auto_tilde.

Ltac heap_eq :=
  solve [ rew_heap; subst; auto ].

charguer's avatar
charguer committed
370

charguer's avatar
charguer committed
371 372
(*------------------------------------------------------------------*)
(* ** Properties of [hprop] *)
charguer's avatar
charguer committed
373

charguer's avatar
charguer committed
374
(* LATER: use rew_heap more often, like RO dev does *)
charguer's avatar
charguer committed
375

charguer's avatar
charguer committed
376 377
Global Instance hprop_inhab : Inhab hprop.
Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
charguer's avatar
charguer committed
378 379 380

Section HeapProp.

charguer's avatar
charguer committed
381
Implicit Types H : hprop.
charguer's avatar
charguer committed
382
Transparent hprop_empty hprop_pure hprop_single hprop_star hprop_gc heap_union.
charguer's avatar
charguer committed
383

charguer's avatar
charguer committed
384
Lemma hprop_pure_prove : forall (P:Prop),
charguer's avatar
charguer committed
385 386 387 388
  P -> 
  \[P] heap_empty.
Proof using. intros. hnfs~. Qed.

charguer's avatar
charguer committed
389
Lemma hprop_pure_inv : forall h (P:Prop),
charguer's avatar
charguer committed
390
  \[P] h -> h = heap_empty /\ P.
charguer's avatar
charguer committed
391 392
Proof using. intros. auto. Qed.

charguer's avatar
charguer committed
393
Lemma hprop_pure_inv' : forall m n (P:Prop),
charguer's avatar
charguer committed
394 395
  \[P] (m,n) -> m = state_empty /\ n = credits_zero /\ P.
Proof using.
charguer's avatar
charguer committed
396
  introv M. lets (E&N): hprop_pure_inv M.
charguer's avatar
charguer committed
397 398 399
  unfold heap_empty in E. inverts* E.
Qed.

charguer's avatar
charguer committed
400 401 402 403 404
Lemma hprop_empty_prove : 
  \[] heap_empty.
Proof using. hnfs~. Qed.

Lemma hprop_empty_inv : forall h, 
charguer's avatar
charguer committed
405
  \[] h -> h = heap_empty.
charguer's avatar
charguer committed
406
Proof using. introv M. forwards*: hprop_pure_inv M. Qed.
charguer's avatar
charguer committed
407

charguer's avatar
charguer committed
408 409
Lemma hprop_credits_inv : forall h n,
  (\$ n) h -> h = (state_empty,n).
charguer's avatar
charguer committed
410
Proof using. intros (m,n') n (M1&M2). simpls. subst*. Qed.
charguer's avatar
charguer committed
411

charguer's avatar
charguer committed
412 413 414 415 416 417 418 419 420 421 422 423
Lemma hprop_gc_prove : forall h, 
  \GC h.
Proof using. intros. exists~ (=h). Qed.

Lemma hprop_gc_merge : 
  \GC \* \GC = \GC.
Proof using.
  unfold hprop. extens. intros h. iff (h1&h2&M1&M2&D&U) M.
  { apply hprop_gc_prove. }
  { exists h heap_empty. splits~. apply hprop_gc_prove. }
Qed.

charguer's avatar
charguer committed
424 425
Lemma hprop_star_comm : forall H1 H2,
   H1 \* H2 = H2 \* H1.
charguer's avatar
charguer committed
426 427 428 429 430 431 432 433 434
Proof using. 
  intros H1 H2. unfold hprop, hprop_star. extens. intros h.
  iff (h1&h2&M1&M2&D&U); rewrite~ heap_union_comm in U; exists* h2 h1.
Qed.

Lemma hprop_star_empty_l : forall H,
   \[] \* H = H.
Proof using.
  intro. unfold hprop, hprop_star. extens. intros h.
charguer's avatar
charguer committed
435 436
  iff (h1&h2&(M1&E1)&M2&D&U) M. 
  subst h1 h. rewrite~ heap_union_empty_l.
charguer's avatar
charguer committed
437 438 439 440 441 442 443 444 445 446
  exists heap_empty h. hint hprop_empty_prove. splits~. 
Qed.

Lemma hprop_star_empty_r : forall H, 
  H \* \[] = H.
Proof using.
  apply neutral_r_from_comm_neutral_l.
  applys hprop_star_comm. applys hprop_star_empty_l.
Qed.

charguer's avatar
charguer committed
447
Lemma hprop_star_assoc : forall H1 H2 H3,
charguer's avatar
charguer committed
448
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
charguer's avatar
charguer committed
449 450 451
Proof using. 
  intros H1 H2 H3. unfold hprop, hprop_star. extens. intros h. split.
  { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
charguer's avatar
charguer committed
452
    exists h1 (h2 \u h3). splits~.
charguer's avatar
charguer committed
453
    { exists h2 h3. splits*. }
charguer's avatar
charguer committed
454 455 456 457 458
    { subst. applys heap_eq. split. { state_eq. } { simpl; math. } } }
  { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
    exists (h1 \u h2) h3. splits~.
    { exists h1 h2. splits*. } 
    { subst. applys heap_eq. split. { state_eq. } { simpl; math. } } }
charguer's avatar
charguer committed
459
Qed. 
charguer's avatar
charguer committed
460 461 462 463

Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
  (hprop_single l v1) \* (hprop_single l v2) ==> \[False].
Proof using.
charguer's avatar
charguer committed
464
  intros. unfold hprop_single. 
charguer's avatar
charguer committed
465 466 467
  intros h ((m1&n1)&(m2&n2)&(E1&X1)&(E2&X2)&D&E). false.
  subst. applys* state_single_same_loc_disjoint l v1 v2.
  unfolds in D. rewrite <- E1. rewrite <- E2. auto.
charguer's avatar
charguer committed
468 469 470 471 472
Qed.

Lemma hprop_star_prop_elim : forall (P:Prop) H h,
  (\[P] \* H) h -> P /\ H h.
Proof using.
charguer's avatar
charguer committed
473
  introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_empty_l.
charguer's avatar
charguer committed
474 475
Qed.

charguer's avatar
charguer committed
476 477 478 479 480 481 482 483

(*------------------------------------------------------------------*)
(* ** Properties of [himpl] *)

Lemma himpl_forward : forall H1 H2 h,
  (H1 ==> H2) -> (H1 h) -> (H2 h).
Proof using. auto. Qed.

charguer's avatar
charguer committed
484 485 486 487 488 489 490 491 492 493 494 495
Lemma himpl_refl : forall H,
  H ==> H.
Proof using. intros h. auto. Qed.

Lemma himpl_trans : forall H1 H2 H3,
  (H1 ==> H2) -> (H2 ==> H3) -> (H1 ==> H3).
Proof using. introv M1 M2. intros h H1h. eauto. Qed.

Lemma himpl_antisym : forall H1 H2,
  (H1 ==> H2) -> (H2 ==> H1) -> (H1 = H2).
Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed.

charguer's avatar
charguer committed
496 497 498 499 500
Lemma himpl_cancel_l : forall H1 H1' H2,
  H1 ==> H1' -> (H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

Lemma himpl_cancel_r : forall H1 H2 H2',
charguer's avatar
charguer committed
501 502 503 504
  H2 ==> H2' -> (H1 \* H2) ==> (H1 \* H2').
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

Lemma himpl_extract_prop : forall (P:Prop) H H',
charguer's avatar
charguer committed
505 506 507
  (P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using. introv W Hh. lets (?&?): hprop_star_prop_elim Hh. applys* W. Qed.

charguer's avatar
charguer committed
508
Lemma himpl_extract_exists : forall A (x:A) H J,
charguer's avatar
charguer committed
509 510 511
  (H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.

charguer's avatar
charguer committed
512 513
Lemma himpl_inst_prop : forall (P:Prop) H H',
  P -> H ==> H' -> H ==> (\[P] \* H').
charguer's avatar
charguer committed
514
Proof using. 
charguer's avatar
charguer committed
515
  introv HP W. intros h M. hint hprop_pure_prove. exists~ heap_empty h.
charguer's avatar
charguer committed
516
Qed.
charguer's avatar
charguer committed
517

charguer's avatar
charguer committed
518 519 520 521
Lemma himpl_inst_exists : forall A (x:A) H J,
  (H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.

charguer's avatar
charguer committed
522
Lemma himpl_remove_gc : forall H H',
charguer's avatar
charguer committed
523 524 525 526
  H ==> H' ->
  H ==> H' \* \GC.
Proof using.
  introv M. intros h Hh. exists h heap_empty. splits*.
charguer's avatar
charguer committed
527
  exists \[]. applys hprop_empty_prove.
charguer's avatar
charguer committed
528 529
Qed.

charguer's avatar
charguer committed
530 531
End HeapProp.

charguer's avatar
charguer committed
532
Hint Resolve hprop_empty_prove hprop_pure_prove hprop_gc_prove.
charguer's avatar
charguer committed
533 534


charguer's avatar
charguer committed
535
(********************************************************************)
charguer's avatar
charguer committed
536
(* ** Properties of credits *)
charguer's avatar
charguer committed
537

charguer's avatar
charguer committed
538
Section Credits.
charguer's avatar
charguer committed
539
Transparent hprop_credits hprop_empty hprop_pure hprop_star 
charguer's avatar
charguer committed
540
  heap_union heap_disjoint.
charguer's avatar
charguer committed
541

charguer's avatar
charguer committed
542 543 544
Lemma credits_zero_eq : \$ 0 = \[].
Proof using.
  unfold hprop_credits, hprop_empty, heap_empty. 
charguer's avatar
charguer committed
545 546
  applys prop_ext_1. intros [m n]; simpl. iff [M1 M2] M. 
  { subst*. }
charguer's avatar
charguer committed
547
  { lets*: hprop_pure_inv' M. }
charguer's avatar
charguer committed
548 549 550 551 552 553 554 555
Qed.

Lemma credits_split_add : forall (n m : nat),
  \$ (n+m) = \$ n \* \$ m.
Proof using.
  intros c1 c2. unfold hprop_credits, hprop_star, heap_union, heap_disjoint. 
  applys prop_ext_1. intros [m n].
  iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4).
charguer's avatar
charguer committed
556 557 558
  { exists (state_empty,c1) (state_empty,c2). simpls. splits*.
    { fequals. state_eq. } }
  { simpls. inverts M4. subst. split~. state_eq. }  
charguer's avatar
charguer committed
559 560 561 562 563 564 565 566 567 568 569
Qed.

Lemma credits_substract : forall (n m : nat), 
  (n >= m)%nat -> 
  \$ n ==> \$ m \* \$ (n-m).
Proof using.
  introv M. rewrite <- credits_split_add.
  math_rewrite (m + (n-m) = n)%nat. auto.
Qed.

End Credits.
charguer's avatar
charguer committed
570 571 572 573 574 575 576 577


(********************************************************************)
(* ** Rules *)

Implicit Types H : hprop.
Implicit Types Q : val -> hprop.

charguer's avatar
charguer committed
578 579 580 581 582 583

(*------------------------------------------------------------------*)
(* ** Definition of [on_sub] *)

Definition on_sub H := (H \* \GC).

charguer's avatar
charguer committed
584
Lemma on_sub_base : forall H h,
charguer's avatar
charguer committed
585 586 587 588 589 590 591 592 593
  H h -> 
  on_sub H h.
Proof using. intros H h M. exists~ h heap_empty. Qed.

Lemma on_sub_gc : forall H h,
  on_sub (H \* \GC) h ->
  on_sub H h.
Proof using.
  introv M. unfolds on_sub. applys himpl_forward (rm M).
charguer's avatar
charguer committed
594
  rewrite hprop_star_assoc. rewrite~ hprop_gc_merge.
charguer's avatar
charguer committed
595 596 597 598 599 600 601 602
Qed.

Lemma on_sub_union_r : forall H h1 h2,
  on_sub H h1 ->
  \# h1 h2 ->
  on_sub H (h1 \u h2).
Proof using.
  introv M D. unfolds on_sub. rewrite <- hprop_gc_merge.
charguer's avatar
charguer committed
603
  rewrite <- hprop_star_assoc. exists~ h1 h2.
charguer's avatar
charguer committed
604 605
Qed.

charguer's avatar
charguer committed
606 607 608 609 610 611 612 613
Lemma on_sub_union : forall H1 H2 h1 h2,
  on_sub H1 h1 ->
  H2 h2 ->
  \# h1 h2 ->
  on_sub (H1 \* H2) (h1 \u h2).
Proof using.
  introv M P2 D. unfolds on_sub. 
  rewrite hprop_star_assoc.
charguer's avatar
charguer committed
614 615
  rewrite (@hprop_star_comm H2 \GC).
  rewrite <- hprop_star_assoc.
charguer's avatar
charguer committed
616 617 618
  exists~ h1 h2. 
Qed.

charguer's avatar
charguer committed
619 620 621 622 623 624 625 626 627 628 629 630
Lemma on_sub_weaken : forall Q Q' v h,
  on_sub (Q v) h ->
  Q ===> Q' ->
  on_sub (Q' v) h.
Proof using.
  introv M W. unfolds on_sub. applys himpl_forward (rm M).
  applys~ himpl_cancel_l. 
Qed.


(*------------------------------------------------------------------*)
(* ** Spending of credits *)
charguer's avatar
charguer committed
631 632 633

Definition pay_one H H' :=
  H ==> (\$ 1%nat) \* H'.
charguer's avatar
charguer committed
634

charguer's avatar
charguer committed
635 636 637

(*------------------------------------------------------------------*)
(** Definition of triples *)
charguer's avatar
charguer committed
638

charguer's avatar
charguer committed
639 640 641
(** Recall that the projection [heap_state : heap >-> state]
   is used as a Coercion, so that we can write [h] where the
   underlying state is expected. *)
charguer's avatar
charguer committed
642

charguer's avatar
charguer committed
643
Definition triple t H Q :=
charguer's avatar
charguer committed
644 645 646
  forall h1 h2, 
  \# h1 h2 -> 
  H h1 -> 
charguer's avatar
charguer committed
647
  exists n h1' v, 
charguer's avatar
charguer committed
648
       \# h1' h2 
charguer's avatar
charguer committed
649 650
    /\ redn n (h1 \u h2) t (h1' \u h2) v
    /\ on_sub (Q v) h1'
charguer's avatar
charguer committed
651
    /\ (heap_credits h1 = n + heap_credits h1')%nat. 
charguer's avatar
charguer committed
652

charguer's avatar
charguer committed
653

charguer's avatar
charguer committed
654
(*------------------------------------------------------------------*)
655
(** Equivalent definitions of triples *)
charguer's avatar
charguer committed
656

charguer's avatar
charguer committed
657 658
(** We show that the definition of [triple] is equivalent to the
    following lower-level definition. *)
charguer's avatar
charguer committed
659

charguer's avatar
charguer committed
660
Definition triple' t H Q :=
charguer's avatar
charguer committed
661 662 663 664 665 666 667 668 669
  forall m1 c1 m2, 
  state_disjoint m1 m2 -> 
  H (m1,c1) -> 
  exists n m1' c1' v, 
       state_disjoint m1' m2 
    /\ redn n (m1 \+ m2) t (m1' \+ m2) v
    /\ (Q v \* \GC) (m1',c1')
    /\ (c1 = n + c1')%nat.

charguer's avatar
charguer committed
670
Lemma triple_eq_triple' : triple = triple'.
charguer's avatar
charguer committed
671 672
Proof using.
  applys func_ext_3. intros t H Q. extens.
charguer's avatar
charguer committed
673
  unfold triple, triple'. iff M.
charguer's avatar
charguer committed
674 675 676 677 678 679 680 681 682
  { introv D P1. forwards~ (n&h1'&v&R1&R2&R3&R4): M (m1,c1) (m2,0%nat).
    simpls. exists n (h1'^s) (h1'^c) v. splits~.
    { applys_eq R3 1. applys~ heap_eq. } }
  { introv D P1. forwards~ (n&m1'&c1'&v&R1&R2&R3&R4): M (h1^s) (h1^c) (h2^s).
    { applys_eq P1 1. applys~ heap_eq. }
    exists n (m1',c1') v. splits~. }  
Qed.


683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713
(** We show that the definition of [triple] is equivalent to the
    following higher-level definition. *)

Definition triple'' t H Q :=
  forall H' m c, 
  (H \* H') (m, c) -> 
  exists n m' c' v, 
       redn n m t m' v
    /\ (Q v \* \GC \* H') (m', c')
    /\ (c = n + c')%nat.

Lemma triple_eq_triple'' : triple = triple''.
Proof using.
  applys func_ext_3. intros t H Q. extens.
  unfold triple, triple''. iff M.
  { introv (h1&h2&N1&N2&D&U). inverts U.
    forwards~ (n&h1'&v&R1&R2&R3&R4): M h1 h2.
    exists n (h1'^s \+ h2^s) (h1'^c + h2^c)%nat v. splits~.
    { rewrite <- hprop_star_assoc. exists~ h1' h2. }
    { math. } }
  { introv D P1.
    forwards~ (n&m'&c'&v&R1&R2&R3): M (=h2) (h1 \+ h2) (h1^c + h2^c)%nat.
    { exists~ h1 h2. } 
    rewrite <- hprop_star_assoc in R2.
    destruct R2 as ((m1'&c1')&(m2'&c2')&N0&N1&N2&N3).
    inverts N3. subst h2.
    exists n (m1',c1') v. simpls. splits~. { math. } }
Qed.



charguer's avatar
charguer committed
714
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
715 716 717 718 719 720
(** Structural rules *)

Lemma rule_extract_prop : forall t (P:Prop) H Q,
  (P -> triple t H Q) ->
  triple t (H \* \[P]) Q.
Proof using. 
charguer's avatar
charguer committed
721
  introv M D (h21&h22&N1&(HE&HP)&N3&N4). subst h22 h1.
charguer's avatar
charguer committed
722
  rewrite heap_union_empty_r. applys* M. 
charguer's avatar
charguer committed
723 724
Qed.

charguer's avatar
charguer committed
725
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
charguer's avatar
charguer committed
726 727
  (forall x, triple t (J x) Q) ->
  triple t (hprop_exists J) Q.
charguer's avatar
charguer committed
728
Proof using. introv M D (x&Jx). applys* M. Qed.
charguer's avatar
charguer committed
729

charguer's avatar
charguer committed
730
Lemma rule_consequence : forall t H' Q' H Q,
charguer's avatar
charguer committed
731
  H ==> H' ->
charguer's avatar
charguer committed
732 733 734
  triple t H' Q' ->
  Q' ===> Q ->
  triple t H Q.
charguer's avatar
charguer committed
735
Proof using. 
charguer's avatar
charguer committed
736 737 738 739
  introv MH M MQ. intros h1 h2 D P1. 
  lets P1': (rm MH) (rm P1). 
  forwards~ (n&h1'&v&(N1&N2&N3&N4)): (rm M) h2 (rm P1'). 
  exists n h1' v. splits~. { applys~ on_sub_weaken Q'. }
charguer's avatar
charguer committed
740 741
Qed.

charguer's avatar
charguer committed
742 743 744 745 746
Lemma rule_frame : forall t H Q H',
  triple t H Q ->
  triple t (H \* H') (Q \*+ H').
Proof using. 
  introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
charguer's avatar
charguer committed
747 748
  lets~ (n&h1'a&v&Da&Ra&Qa&Na): M h1a (h1b \u h2).
  subst h1. exists n (h1'a \u h1b) v. splits.
charguer's avatar
charguer committed
749
  { auto. }
charguer's avatar
charguer committed
750 751 752 753 754
  { state_red. }
  { applys~ on_sub_union. }
  { do 2 rewrite heap_union_credits. math. }
Qed.

charguer's avatar
charguer committed
755 756 757 758 759 760 761 762 763
Lemma rule_gc_post : forall t H Q,
  triple t H (Q \*+ \GC) ->
  triple t H Q.
Proof using.
  introv M. intros h1 h2 D P1. 
  forwards* (n&h1'&v&(N1&N2&N3&N4)): (rm M) h1 h2.
  exists n h1' v. splits~. { applys~ on_sub_gc. }
Qed.

charguer's avatar
charguer committed
764 765 766 767 768
Lemma rule_gc_pre : forall t H Q,
  triple t H Q ->
  triple t (H \* \GC) Q.
Proof using.
  introv M. applys rule_gc_post. applys~ rule_frame.
charguer's avatar
charguer committed
769 770
Qed.

charguer's avatar
charguer committed
771 772

(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
773 774 775 776 777 778
(** Term rules *)

Lemma rule_val : forall v H Q,
  H ==> Q v ->
  triple (trm_val v) H Q.
Proof using.
charguer's avatar
charguer committed
779
  introv M D H1. exists 0%nat h1 v. splits~.
charguer's avatar
charguer committed
780
  { applys redn_val. }
charguer's avatar
charguer committed
781
  { applys~ on_sub_base. }
charguer's avatar
charguer committed
782 783
Qed.

charguer's avatar
charguer committed
784
Lemma rule_if : forall v t1 t2 H Q,
charguer's avatar
charguer committed
785 786 787
  triple (If v = val_int 0 then t2 else t1) H Q ->
  triple (trm_if v t1 t2) H Q.
Proof using.
charguer's avatar
charguer committed
788 789
  introv M D H1. forwards (n&h1'&v'&Da&Ra&Qa&Na): M D H1.
  exists n h1' v'. splits~.
charguer's avatar
charguer committed
790
  { applys~ redn_if. }
charguer's avatar
charguer committed
791 792
Qed.

charguer's avatar
charguer committed
793
Lemma rule_let : forall x t1 t2 H Q Q1,
charguer's avatar
charguer committed
794 795 796 797 798
  triple t1 H Q1 ->
  (forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
  triple (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2. intros h1 h2 D1 H1.
charguer's avatar
charguer committed
799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824
  lets (na&h1'&v1&Da&Ra&Qa&Na): M1 D1 H1.
  lets (h1'a&h1'b&N1&N2&N3&N4): (rm Qa).
  forwards~ (nb&h1''&v2&Db&Rb&Qb&Nb): M2 v1 h1'a (h1'b \u h2).
  exists (na+nb)%nat (h1'' \u h1'b) v2. splits~.
  { applys redn_let Ra. state_red. }
  { applys~ on_sub_union_r. }
  { subst. simpls. math. } 
Qed.

Lemma rule_let_val : forall x v1 t2 H Q,
  (forall (X:val), X = v1 -> triple (subst_trm x X t2) H Q) ->
  triple (trm_let x (trm_val v1) t2) H Q.
Proof using. 
  introv M. forwards~ M': M.
  applys_eq~ (>> rule_let H (fun x => H \* \[x = v1])) 2.
  { applys rule_val. rewrite hprop_star_comm. applys~ himpl_inst_prop. }
  { intros X. applys rule_extract_prop. applys M. }
Qed.

Lemma rule_app : forall f x F V t1 H H' Q,
  F = (val_fix f x t1) ->
  pay_one H H' ->
  triple (subst_trm f F (subst_trm x V t1)) H' Q ->
  triple (trm_app F V) H Q.
Proof using.
  introv EF HP M. subst F. intros h1 h2 D P1.
charguer's avatar
charguer committed
825
  lets P1': (rm HP) (rm P1). (* LATER: lemma for these lines *)
charguer's avatar
charguer committed
826 827 828
  lets (h1a&h1b&V1&P1''&V2&V3): (rm P1').
  lets V1': hprop_credits_inv (rm V1).
  forwards~ (n&h1'&v&N1&N2&N3&N4): (rm M) h2 (rm P1'').
charguer's avatar
charguer committed
829 830 831
  exists (S n) h1' v. splits~.
  { applys~ redn_app. state_red. }
  { subst. simpl. math. }
charguer's avatar
charguer committed
832 833
Qed.

charguer's avatar
charguer committed
834
Lemma rule_let_fix : forall f x t1 t2 H Q,
charguer's avatar
charguer committed
835
  (forall (F:val), 
charguer's avatar
charguer committed
836 837 838
    (forall X H' H'' Q', 
      pay_one H' H'' ->
      triple (subst_trm f F (subst_trm x X t1)) H'' Q' ->
charguer's avatar
charguer committed
839
      triple (trm_app F X) H' Q') ->  
charguer's avatar
charguer committed
840
    triple (subst_trm f F t2) H Q) ->
charguer's avatar
charguer committed
841
  triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
charguer's avatar
charguer committed
842
Proof using.
charguer's avatar
charguer committed
843 844 845
  introv M. applys rule_let_val. intros F EF. 
  applys (rm M). clears H Q. intros X H H' Q N.
  applys~ rule_app.
charguer's avatar
charguer committed
846
Qed.
charguer's avatar
charguer committed
847

charguer's avatar
charguer committed
848
Lemma rule_new : forall v,
849
  triple (prim_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
charguer's avatar
charguer committed
850
Proof using.
charguer's avatar
charguer committed
851 852 853 854 855 856 857 858
  intros. intros h1 h2 _ P1.
  lets E: hprop_empty_inv P1. subst h1.
  lets (l&Dl): (state_disjoint_new (heap_state h2) v).
  sets h1': (state_single l v, 0%nat).
  exists 0%nat h1' (val_loc l). splits~.
  { rew_state. applys~ redn_new. }
  { applys~ on_sub_base. exists l. 
    applys~ himpl_inst_prop (l ~~> v). split~. }
charguer's avatar
charguer committed
859 860 861
Qed.

Lemma rule_get : forall v l,
862
  triple (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
charguer's avatar
charguer committed
863
Proof using.
charguer's avatar
charguer committed
864 865
  intros. intros h1 h2 D P1. exists 0%nat h1 v. splits~.
  { rew_state. applys redn_get. lets (P1a&P1b): P1.
charguer's avatar
charguer committed
866
    rewrite P1a. applys~ state_union_single_read. }
charguer's avatar
charguer committed
867 868
  { exists h1 heap_empty. splits~.
    { exists~ heap_empty h1. } }
charguer's avatar
charguer committed
869 870 871
Qed.

Lemma rule_set : forall l v w,
872
  triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
charguer's avatar
charguer committed
873
Proof using.
charguer's avatar
charguer committed
874 875 876 877
  intros. intros h1 h2 D P1. lets (P1a&P1b): P1.
  sets h1': (state_single l w, 0%nat).
  exists 0%nat h1' val_unit. splits~.
  { applys state_disjoint_single_set v. rewrite~ <- P1a. }
charguer's avatar
charguer committed
878 879
  { rew_state. applys~ redn_set. rewrite P1a. 
    applys~ state_union_single_write v w. }
charguer's avatar
charguer committed
880 881
  { applys~ on_sub_base. applys~ himpl_inst_prop (l ~~> w). split~. }
Qed.
charguer's avatar
charguer committed
882 883