MLExamples.v 13.8 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5
(**

This file formalizes examples from standard Separation Logic, 
as described in Arthur Charguéraud's lecture notes.

charguer's avatar
charguer committed
6 7 8
Author: Arthur Charguéraud.
License: MIT.

charguer's avatar
charguer committed
9 10 11
*)

Set Implicit Arguments.
charguer's avatar
charguer committed
12
Require Import MLCF MLCFLifted.
charguer's avatar
charguer committed
13
Open Scope trm_scope.
charguer's avatar
charguer committed
14
Open Scope heap_scope.
charguer's avatar
charguer committed
15
Open Scope charac.
charguer's avatar
charguer committed
16 17 18 19

Ltac auto_star ::= jauto.


charguer's avatar
charguer committed
20 21 22 23 24 25 26 27

(*
Notation "[ ]" := nil (format "[ ]") : liblist_scope. 
Notation "[ x ]" := (cons x nil) : liblist_scope.
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : liblist_scope.
Open Scope liblist_scope.
*)

charguer's avatar
charguer committed
28
(* ********************************************************************** *)
charguer's avatar
charguer committed
29
(* * Mutable lists *)
charguer's avatar
charguer committed
30

charguer's avatar
charguer committed
31
(** Layout in memory:
charguer's avatar
charguer committed
32

charguer's avatar
charguer committed
33 34
  type 'a mlist = { mutable hd : 'a ; mutable tl : 'a mlist }
  // empty lists represented using null
charguer's avatar
charguer committed
35

charguer's avatar
charguer committed
36
*)
charguer's avatar
charguer committed
37

charguer's avatar
charguer committed
38 39
Definition hd : field := 0%nat.
Definition tl : field := 1%nat.
charguer's avatar
charguer committed
40 41 42 43

Fixpoint MList (L:list val) (p:loc) : hprop :=
  match L with
  | nil => \[p = null]
charguer's avatar
charguer committed
44
  | x::L' => Hexists (p':loc), (p ~> record`{ hd := x; tl := val_loc p' }) \* (p' ~> MList L')
charguer's avatar
charguer committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
  end.

Section Properties.
Implicit Types L : list val.

(** Conversion lemmas for empty lists *)

Lemma MList_nil : forall p,
  p ~> MList nil = \[p = null].
Proof using. intros. xunfold~ MList. Qed.

Lemma MList_unnil : 
  \[] ==> null ~> MList nil.
Proof using. intros. rewrite MList_nil. hsimpl~. Qed.

Lemma MList_null : forall L,
  (null ~> MList L) = \[L = nil].
Proof using. 
  intros. destruct L.
  { xunfold MList. applys himpl_antisym; hsimpl~. }
charguer's avatar
charguer committed
65
  { xunfold MList. applys himpl_antisym. 
charguer's avatar
charguer committed
66
    { hpull ;=> p'. hchange (hrecord_not_null null); auto_false.
charguer's avatar
charguer committed
67 68
      hpull; auto_false. }
    { hpull. } } 
charguer's avatar
charguer committed
69 70 71 72 73 74 75 76 77
Qed.  

Lemma MList_null_keep : forall L,
  null ~> MList L ==>
  null ~> MList L \* \[L = nil].
Proof using. 
  intros. destruct L.
  { hsimpl~. }
  { rewrite MList_null. hsimpl. }
charguer's avatar
charguer committed
78 79
Qed.

charguer's avatar
charguer committed
80 81 82 83
(** Conversion lemmas for non-empty lists *)

Lemma MList_cons : forall p x L',
  p ~> MList (x::L') = 
charguer's avatar
charguer committed
84
  Hexists p', (p ~> record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L'.
charguer's avatar
charguer committed
85 86 87
Proof using. intros. xunfold MList at 1. simple~. Qed.

Lemma MList_uncons : forall p p' x L',
charguer's avatar
charguer committed
88
  (p ~> record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L' ==> 
charguer's avatar
charguer committed
89 90 91 92 93 94 95 96 97 98
  p ~> MList (x::L').
Proof using. intros. rewrite MList_cons. hsimpl. Qed.

Lemma MList_not_null_keep : forall p L,
  p <> null -> 
  p ~> MList L ==> p ~> MList L \* \[L <> nil].
Proof using. 
  intros. destruct L.
  { hchanges -> (MList_nil p). }
  { hsimpl. auto_false. }
charguer's avatar
charguer committed
99 100
Qed.

charguer's avatar
charguer committed
101 102 103 104
Lemma MList_not_null : forall p L,
  p <> null -> 
  p ~> MList L ==> Hexists x p' L',  
       \[L = x::L'] 
charguer's avatar
charguer committed
105
    \* (p ~> record`{ hd := x; tl := val_loc p' }) 
charguer's avatar
charguer committed
106 107 108 109 110 111
    \* p' ~> MList L'.
Proof using.
  intros. hchange~ (@MList_not_null_keep p). hpull. intros. 
  destruct L; tryfalse.
  hchange (MList_cons p). hsimpl~.
Qed.
charguer's avatar
charguer committed
112

charguer's avatar
charguer committed
113
End Properties.
charguer's avatar
charguer committed
114

charguer's avatar
charguer committed
115 116 117 118 119 120
Implicit Arguments MList_null_keep [].
Implicit Arguments MList_cons [].
Implicit Arguments MList_uncons [].
Implicit Arguments MList_not_null [].
Implicit Arguments MList_not_null_keep [].

charguer's avatar
charguer committed
121
Global Opaque MList.
charguer's avatar
charguer committed
122

charguer's avatar
charguer committed
123 124


charguer's avatar
charguer committed
125 126 127 128 129 130 131 132 133 134 135
(** Temporary auxiliary specification *)

Parameter rule_get_tl : forall p x p',
  triple (trm_app prim_get [val_loc p; val_field tl]) 
    (p ~> record `{ hd := x; tl := p'})
    (fun r => \[r = p'] \* p ~> record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)




charguer's avatar
charguer committed
136

charguer's avatar
charguer committed
137
(* ********************************************************************** *)
charguer's avatar
charguer committed
138
(* * Definition of the list increment program *)
charguer's avatar
charguer committed
139 140 141 142

(** Program variables *)

Definition Mlist_length : var := 1%nat.
charguer's avatar
charguer committed
143 144 145
Definition X : var := 3%nat.
Definition P : var := 4%nat.
Definition Q : var := 5%nat.
charguer's avatar
charguer committed
146 147 148 149 150 151
Definition N : var := 6%nat.

(** Program code *)

Definition mlist_length : val :=
  Fix Mlist_length [P] :=   
charguer's avatar
charguer committed
152 153
    Let X := trm_app prim_neq [val_var P; val_loc null] in
    If_ val_var X Then (
charguer's avatar
charguer committed
154 155
      Let Q := prim_get [val_var P; val_field tl] in
      Let N := trm_app (val_var Mlist_length) [val_var Q] in
charguer's avatar
charguer committed
156 157 158 159 160 161 162 163
      trm_app prim_add [val_var N; val_int 1] 
    ) Else (
      val_int 0
    ).

(** Helper for simplifying substitutions *)


charguer's avatar
charguer committed
164 165 166
Lemma mlist_length_closed : 
  closed_val mlist_length.
Proof using. reflexivity. Qed.
charguer's avatar
charguer committed
167

charguer's avatar
charguer committed
168 169 170
Lemma subst_val_mlist_length : forall E,
  subst_val E mlist_length = mlist_length.
Proof using. intros. applys subst_val_closed. applys mlist_length_closed. Qed.
charguer's avatar
charguer committed
171

charguer's avatar
charguer committed
172
Hint Rewrite subst_val_mlist_length : rew_subst.
charguer's avatar
charguer committed
173

charguer's avatar
charguer committed
174 175 176 177 178 179
(* short version to avoid stating the two lemmas above:
   Lemma subst_val_closed' : forall v, closed_val v -> forall E,
    subst_val E v = v.
   Proof using. intros. applys subst_val_closed. Qed.
   Hint Rewrite (@subst_val_closed' mlist_length (refl_equal _)) : rew_subst.
*)
charguer's avatar
charguer committed
180

charguer's avatar
charguer committed
181 182
Ltac simpl_subst := 
  simpl; autorewrite with rew_subst.
charguer's avatar
charguer committed
183

charguer's avatar
charguer committed
184
(* ********************************************************************** *)
charguer's avatar
charguer committed
185 186
(* * Mutable list increment verification, using triples *)

charguer's avatar
charguer committed
187
Section ProofWithTriples.
charguer's avatar
charguer committed
188 189 190 191 192 193

Lemma mlist_incr_spec : forall L p, 
  triple (trm_app mlist_length [val_loc p]) 
    (p ~> MList L)
    (fun r => \[r = val_int (length L)] \* p ~> MList L).
Proof using.
charguer's avatar
charguer committed
194
  intros L. induction_wf: list_sub_wf L. intros p. 
charguer's avatar
charguer committed
195 196 197
  applys rule_app; try reflexivity. 
  Transparent mlist_length.
  simpl_subst.
charguer's avatar
charguer committed
198 199 200 201
  Opaque mlist_length.
  applys rule_let. { xapplys rule_neq. }
  simpl_subst. intros X. xpull. intros EX. 
  applys rule_if_val. subst X.
charguer's avatar
charguer committed
202
  case_if as C1; case_if as C2; tryfalse.
charguer's avatar
charguer committed
203
  { inverts C2. xchange MList_null_keep. 
charguer's avatar
charguer committed
204
    xpull. intros EL. applys rule_val. hsimpl. subst~. }
charguer's avatar
charguer committed
205 206
  { xchange (MList_not_null p). { auto. } 
    xpull. intros x p' L' EL.
charguer's avatar
charguer committed
207
    applys rule_let.
charguer's avatar
charguer committed
208
    { xapplys rule_get_tl. }
charguer's avatar
charguer committed
209
    { simpl_subst. intros p''. xpull. intros E. subst p''. 
charguer's avatar
charguer committed
210
      applys rule_let. 
charguer's avatar
charguer committed
211
      { simpl_subst. xapplys IH. { subst~. } }
charguer's avatar
charguer committed
212
      { simpl_subst. intros r. xpull. intros Er. xchange (MList_uncons p). 
charguer's avatar
charguer committed
213
        subst r. xapplys rule_add. subst. rew_length. fequals. math. } } }
charguer's avatar
charguer committed
214 215
Qed.

charguer's avatar
charguer committed
216 217
End ProofWithTriples.

charguer's avatar
charguer committed
218

charguer's avatar
charguer committed
219
(* ********************************************************************** *)
charguer's avatar
charguer committed
220 221 222 223 224 225 226 227 228 229 230
(* * Demos of characteristic formulae *)

Module MLCFDemo.
Import MLCFTactics.
Open Scope charac.


Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) =>
  Provide rule_get_tl.


charguer's avatar
charguer committed
231
(* ********************************************************************** *)
charguer's avatar
charguer committed
232 233 234 235 236 237 238 239 240 241 242
(* * Mutable list increment verification, using characteristic formulae, 
     without tactics. *)

(** Observe how, in the proof below, the deep embedding is never revealed. *)

Lemma mlist_incr_spec' : forall L p, 
  app mlist_length [val_loc p]
    (p ~> MList L)
    (fun r => \[r = val_int (length L)] \* p ~> MList L).
Proof using.
  intros L. induction_wf: list_sub_wf L. intros p. 
charguer's avatar
charguer committed
243
  applys sound_for_cf_app1 20%nat. reflexivity.
charguer's avatar
charguer committed
244
  simpl; fold mlist_length. 
charguer's avatar
charguer committed
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
  applys local_erase. esplit. split. 
  { applys local_erase. xapplys rule_neq. }
  intros X. xpull. intros EX.
  subst X. applys local_erase.
  split; intros C; case_if as C'; clear C.
  { xchange (MList_not_null p). { auto. } 
    xpull. intros x p' L' EL.
    applys local_erase. esplit. split.
    { applys local_erase. xapplys rule_get_tl. }
    intros p''. xpull. intros E. subst p''.
    applys local_erase. esplit. split.
    { applys local_erase. xapplys IH. { subst~. } }
    { intros r. xpull. intros Er. xchange (MList_uncons p). 
      subst r. applys local_erase. xapplys rule_add.
      subst. rew_length. fequals. math. } }  
  { applys local_erase. unfolds. inverts C'. xchange MList_null_keep.  
    hpull. intros EL. hsimpl. subst~. }
Qed.

charguer's avatar
charguer committed
264

charguer's avatar
charguer committed
265
(* ********************************************************************** *)
charguer's avatar
charguer committed
266 267
(* * Mutable list increment verification, using characteristic formulae *)

charguer's avatar
charguer committed
268
(** Remark: in Ltac script below, "=>" is an alias for "intros" *)
charguer's avatar
charguer committed
269

charguer's avatar
charguer committed
270
Lemma mlist_incr_spec'' : forall L p, 
charguer's avatar
charguer committed
271
  app mlist_length [val_loc p]
charguer's avatar
charguer committed
272 273 274
    (p ~> MList L)
    (fun r => \[r = val_int (length L)] \* p ~> MList L).
Proof using.
charguer's avatar
charguer committed
275 276 277
  intros L. induction_wf: list_sub_wf L. intros p. xcf.
  xlet. { xapp. } 
  intros X. xpull ;=> EX.
charguer's avatar
charguer committed
278 279 280 281 282
  subst X. xif ;=> C; case_if as C'; clear C.
  { xchange (MList_not_null p). { auto. } xpull ;=> x p' L' EL.
    xlet. { xapp. }
    intros p''. xpull ;=> E. subst p''.
    xlet. { xapp IH. { subst~. } }
charguer's avatar
charguer committed
283
      { intros r. xpull ;=> Er. xchange (MList_uncons p). 
charguer's avatar
charguer committed
284
        subst r. xapp. subst. rew_length. fequals. math. } }  
charguer's avatar
charguer committed
285
  { xval. inverts C'. xchange MList_null_keep.  
charguer's avatar
charguer committed
286 287
    hpull ;=> EL. hsimpl. subst~. }
Qed.
charguer's avatar
charguer committed
288

charguer's avatar
charguer committed
289 290 291 292
End MLCFDemo.



charguer's avatar
charguer committed
293
(* ********************************************************************** *)
charguer's avatar
charguer committed
294 295 296 297 298 299 300 301
(* * Demos of characteristic formulae *)

Module MLCFLiftedDemo.
Import MLCFLiftedTactics.
Open Scope charac.



charguer's avatar
charguer committed
302
(* ********************************************************************** *)
charguer's avatar
charguer committed
303
(* * Mutable lists *)
charguer's avatar
charguer committed
304

charguer's avatar
charguer committed
305 306 307 308 309 310 311 312 313 314 315
(** Layout in memory:

  type 'a mlist = { mutable hd : 'a ; mutable tl : 'a mlist }
  // empty lists represented using null

*)



(** Record contents *)

charguer's avatar
charguer committed
316 317
(* TODO: use MLCFlifted *)

charguer's avatar
charguer committed
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 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
Notation "`'{ f1 := x1 }" := 
  ((f1, Dyn x1)::nil)
  (at level 0, f1 at level 0) 
  : trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::nil)
  (at level 0, f1 at level 0, f2 at level 0) 
  : trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0) 
  : trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : trm_scope.
Open Scope trm_scope.

(*
Definition hd : field := 0.
Definition tl : field := 1.
*)

Fixpoint MList A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
  match L with
  | nil => \[p = null]
  | x::L' => Hexists (p':loc), (p ~> Record`'{ hd := x; tl := p' }) \* (p' ~> MList L')
  end.

Section Properties.
Context (A:Type) `{EA:Enc A}.
Implicit Types L : list A.
Implicit Types p : loc.

(** Conversion lemmas for empty lists *)

Lemma MList_nil : forall p,
  p ~> MList nil = \[p = null].
Proof using. intros. xunfold~ MList. Qed.

Lemma MList_unnil : 
  \[] ==> null ~> MList nil.
Proof using. intros. rewrite MList_nil. hsimpl~. Qed.

Lemma MList_null : forall L,
  (null ~> MList L) = \[L = nil].
Proof using. 
  intros. destruct L.
  { xunfold MList. applys himpl_antisym; hsimpl~. }
  { xunfold MList. applys himpl_antisym. 
charguer's avatar
charguer committed
368
    { hpull ;=> p'. hchange (hRecord_not_null null); auto_false.
charguer's avatar
charguer committed
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 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
      hpull; auto_false. }
    { hpull. } } 
Qed.  

Lemma MList_null_keep : forall L,
  null ~> MList L ==>
  null ~> MList L \* \[L = nil].
Proof using. 
  intros. destruct L.
  { hsimpl~. }
  { rewrite MList_null. hsimpl. }
Qed.

(** Conversion lemmas for non-empty lists *)

Lemma MList_cons : forall p x L',
  p ~> MList (x::L') = 
  Hexists p', (p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L'.
Proof using. intros. xunfold MList at 1. simple~. Qed.

Lemma MList_uncons : forall p p' x L',
  (p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L' ==> 
  p ~> MList (x::L').
Proof using. intros. rewrite MList_cons. hsimpl. Qed.

Lemma MList_not_null_keep : forall p L,
  p <> null -> 
  p ~> MList L ==> p ~> MList L \* \[L <> nil].
Proof using. 
  intros. destruct L.
  { hchanges -> (MList_nil p). }
  { hsimpl. auto_false. }
Qed.

Lemma MList_not_null : forall p L,
  p <> null -> 
  p ~> MList L ==> Hexists x p' L',  
       \[L = x::L'] 
    \* (p ~> Record`'{ hd := x; tl := p' }) 
    \* p' ~> MList L'.
Proof using.
  intros. hchange~ (@MList_not_null_keep p). hpull. intros. 
  destruct L; tryfalse.
  hchange (MList_cons p). hsimpl~.
Qed.

End Properties.

Implicit Arguments MList_null_keep [A [EA]].
Implicit Arguments MList_cons [A [EA]].
Implicit Arguments MList_uncons [A [EA]].
Implicit Arguments MList_not_null [A [EA]].
Implicit Arguments MList_not_null_keep [A [EA]].

Global Opaque MList.



charguer's avatar
charguer committed
427
(* ********************************************************************** *)
charguer's avatar
charguer committed
428 429
(* TODO: prove spec of primitives *)

charguer's avatar
charguer committed
430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456
Open Scope charac.

(** Args contents *)


Notation "`[ x1 x2 ]" :=
  ((Dyn x1)::(Dyn x2)::nil)
  (at level 0, x1 at level 0, x2 at level 0) 
  : trm_scope.
Notation "`[ x1 ]" := 
  ((Dyn x1)::nil)
  (at level 0, x1 at level 0) 
  : trm_scope.
(*
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0) 
  : trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : trm_scope.
*)
Open Scope trm_scope.



charguer's avatar
charguer committed
457 458

Parameter Rule_add : forall (n1 n2:int),
charguer's avatar
charguer committed
459
  App prim_add `[n1 n2]
charguer's avatar
charguer committed
460 461 462 463
    \[] 
    (fun (r:int) => \[r = (n1 + n2)]).

Parameter Rule_neq : forall (v1 v2:loc),
charguer's avatar
charguer committed
464
  App prim_neq `[v1 v2]
charguer's avatar
charguer committed
465 466 467
    \[] 
    (fun (r:int) => \[r = (If v1 = v2 then 0 else 1)]).

charguer's avatar
charguer committed
468 469
Parameter Rule_get_tl : forall (p:loc) A `{EA:Enc A} (x:A) (p':loc),
  App prim_get `[p (tl:field)]
charguer's avatar
charguer committed
470 471 472 473
    (p ~> Record `'{ hd := x; tl := p'})
    (fun (r:loc) => \[r = p'] \* p ~> Record `'{ hd := x; tl := p'}).


charguer's avatar
charguer committed
474
Hint Extern 1 (RegisterSpec (App (val_prim prim_get) `[_ tl] _ _)) =>
charguer's avatar
charguer committed
475 476
  Provide Rule_get_tl.

charguer's avatar
charguer committed
477
Hint Extern 1 (RegisterSpec (App (val_prim prim_neq) `[_ _] _ _)) => 
charguer's avatar
charguer committed
478 479
  Provide Rule_neq.

charguer's avatar
charguer committed
480
Hint Extern 1 (RegisterSpec (App (val_prim prim_add) `[_ _] _ _)) =>
charguer's avatar
charguer committed
481 482 483 484 485
  Provide Rule_add.




charguer's avatar
charguer committed
486
(* ********************************************************************** *)
charguer's avatar
charguer committed
487 488 489 490
(* * Mutable list increment verification, using lifted characteristic formulae *)


Lemma mlist_incr_spec : forall A `{EA:Enc A} (L:list A) (p:loc), 
charguer's avatar
charguer committed
491
  App mlist_length `[p]
charguer's avatar
charguer committed
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
    (p ~> MList L)
    (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
  intros. gen p. induction_wf: list_sub_wf L; intros. xcf.
  xlet. { xapp. }
  intros X. xpull ;=> EX.
  subst X. xif ;=> C; case_if as C'; clear C.
  { xchange (MList_not_null p). { auto. } xpull ;=> x p' L' EL.
    xlet. { xapp. }
    intros p''. xpull ;=> E. subst p''.
    xlet. { xapp IH. { subst~. } }
      { intros r. xpull ;=> Er. xchange (MList_uncons p). 
        subst r. xapp. subst. rew_length. fequals. math. } }  
  { xval. xchanges MList_null_keep ;=> EL. hsimpl. subst~. }
Qed.
charguer's avatar
charguer committed
507 508 509



charguer's avatar
charguer committed
510
End MLCFLiftedDemo.
charguer's avatar
charguer committed
511 512 513 514