CFApp.v 22.1 KB
Newer Older
charguer's avatar
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
3
Require Import LibCore LibEpsilon Shared.
Require Import CFHeaps.
charguer's avatar
charguer committed
4
5

Hint Extern 1 (_ ===> _) => apply rel_le_refl.
charguer's avatar
charguer committed
6
7
8
9
10
(* TODO: make this a local hint? xauto should take care of this. *)




charguer's avatar
charguer committed
11
12
13
14
15
16
17
18
19
20
21
(********************************************************************)
(* ** Overview *)

(**  

  CFML exports an axiomatic operation [eval f v h v' h'] which describes th 
  e big-step evaluation of a one-argument function on the entire heap.

  Based on [eval], we define [app_basic f x H Q], which is a like [eval]
  modulo frame and weakening and garbage collection.
  
charguer's avatar
charguer committed
22
  On top of [app_basic], we define [app f xs H Q], which describes the
charguer's avatar
charguer committed
23
24
25
26
27
28
29
  evaluation of a call to [f] on the arguments described by the list [xs].

  We also define a predicate [curried n f] which asserts that the function
  [f] is a curried function with [n] arguments, hence its [n-1] first
  applications are partial.

  The characteristic formula generated for a function application
charguer's avatar
charguer committed
30
  [f x y z] is "app f [x y z]".
charguer's avatar
charguer committed
31
32
33

  The characteristic formula generated for a function definition
  [let f x y z = t] is:
charguer's avatar
charguer committed
34
  [curried 3 f /\ (forall x y z H Q, CF(t) H Q -> app f [x y z] H Q)].
charguer's avatar
charguer committed
35
36
37
38

  These definitions are correct and sufficient to reasoning about all
  function calls, including partial and over applications.

charguer's avatar
charguer committed
39
40
41

  This file also contains axiomatization of record operations.

charguer's avatar
charguer committed
42
43
44
*)


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
65
66
67
(********************************************************************)
(* ** Axioms for applications *)

(** Note: these axioms could in theory be realized by constructing
    a deep embedding of the target programming language.  
    See Arthur Chargueraud's PhD thesis for full details. *)

(** The type Func, used to represent functions *)

Axiom func : Type. 

(** The type Func is inhabited *)

Axiom func_inhab : Inhab func. 

Existing Instance func_inhab.

(** The evaluation predicate for functions: [eval f v h v' h'], 
    asserts that the evaluation of the application of [f] to [v]
    in a heap [h] terminates and produces a value [v'] in a heap [h']. *)

Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.

charguer's avatar
charguer committed
68
69

(********************************************************************)
charguer's avatar
charguer committed
70
(* ** Definition and properties of the primitive app predicate *)
charguer's avatar
charguer committed
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

(** The primitive predicate [app_basic], which makes a [local]
    version of [eval]. *)

Definition app_basic (f:func) A (x:A) B (H:hprop) (Q:B->hprop) :=  
  forall h i, \# h i -> H h -> 
    exists v' h' g, \# h' g i /\ Q v' h' /\
      eval f x (h \+ i) v' (h' \+ g \+ i).

(** [app_basic f x] is a local formula *)

Lemma app_basic_local : forall A B f (x:A),
  is_local (@app_basic f A x B).
Proof using.
(*
  asserts Hint1: (forall h1 h2, \# h1 h2 -> \# h2 h1).
    intros. auto. 
  asserts Hint2: (forall h1 h2 h3, \# h1 h2 -> \# h1 h3 -> \# h1 (heap_union h2 h3)).
    intros. rew_disjoint*.
  asserts Hint3: (forall h1 h2 h3, \# h1 h2 -> \# h2 h3 -> \# h1 h3 -> \# h1 h2 h3) .
    intros. rew_disjoint*.
  intros. extens. intros H Q. iff M. apply~ local_erase.
  introv Dhi Hh. destruct (M h Hh) as (H1&H2&Q'&D12&N&HQ).
  destruct D12 as (h1&h2&?&?&?&?).
  destruct~ (N h1 (heap_union i h2)) as (v'&h1'&i'&?&HQ'&E).
  subst h. rew_disjoint*.
  sets h': (heap_union h1' h2).
  forwards Hh': (HQ v' h'). subst h'. exists h1' h2. rew_disjoint*.
  destruct Hh' as (h3'&h4'&?&?&?&?).
  (* todo: optimize the assertions *)
  asserts Hint4: (forall h : heap, \# h h1' -> \# h h2 -> \# h h3'). 
    intros h0 H01 H02. asserts: (\# h0 h'). unfold h'. rew_disjoint*. rewrite H10 in H11. rew_disjoint*.
  asserts Hint5: (forall h : heap, \# h h1' -> \# h h2 -> \# h h4'). 
    intros h0 H01 H02. asserts: (\# h0 h'). unfold h'. rew_disjoint*. rewrite H10 in H11. rew_disjoint*.
  exists v' h3' (heap_union h4' i'). splits.
    subst h h'. rew_disjoint*.
    auto.
    subst h h'. rew_disjoint. intuition. applys_eq E 1 3.
      rewrite* <- heap_union_assoc. rewrite~ (@heap_union_comm h2).
      do 2 rewrite* (@heap_union_assoc h3'). rewrite <- H10.
      do 2 rewrite <- heap_union_assoc. fequal.
      rewrite heap_union_comm. rewrite~ <- heap_union_assoc. rew_disjoint*.
*)
Admitted. (* faster *)
(*
Qed.
*)

Hint Resolve app_basic_local.



(********************************************************************)
(* ** Generic notation for list of dyns *)

charguer's avatar
charguer committed
126
127
128
(* useful for reading goals *)
Local Notation "'Dyn' x" := (@dyn _ x)  (at level 0).

charguer's avatar
charguer committed
129
130

Notation "[ x1 ]" := ((dyn x1)::nil)
charguer's avatar
charguer committed
131
  (at level 0, x1 at level 0) : dynlist.
charguer's avatar
charguer committed
132
133
134
135
136
137
138
139
140
Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
  (at level 0, x1 at level 0, x2 at level 0) : dynlist.
Notation "[ x1 x2 x3 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : dynlist.

charguer's avatar
charguer committed
141
142
(*Bind Scope dynlist with list.*)
Delimit Scope dynlist with dynlist.
charguer's avatar
charguer committed
143
144
145


(********************************************************************)
charguer's avatar
charguer committed
146
(* ** Definition of [app] and properties *)
charguer's avatar
charguer committed
147

charguer's avatar
charguer committed
148
149
(** Definition of [app f xs], recursive.
    Can be written, e.g. Notation [app f [x y z] H Q] *)
charguer's avatar
charguer committed
150

charguer's avatar
charguer committed
151
Fixpoint app_def (f:func) (xs:list dynamic) {B} (H:hprop) (Q:B->hprop) : Prop :=
charguer's avatar
charguer committed
152
153
154
155
156
  match xs with
  | nil => False
  | (dyn x)::nil => app_basic f x H Q
  | (dyn x)::xs => 
     app_basic f x H
charguer's avatar
charguer committed
157
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q])
charguer's avatar
charguer committed
158
159
  end.

charguer's avatar
charguer committed
160
161
162
163
(*
TODO: does not seem to work, hence the work-around using the notation below
Arguments app f%dummy_scope xs%dynlist B%type_scope H%heap_scope Q%heap_scope.
*)
charguer's avatar
charguer committed
164

charguer's avatar
charguer committed
165
166
Notation "'app' f xs" :=
  (@app_def f (xs)%dynlist _)  (* (@app_def f (xs)%dynlist _) *)
charguer's avatar
charguer committed
167
  (at level 80, f at level 0, xs at level 0) : charac.
charguer's avatar
charguer committed
168
Open Scope charac.
charguer's avatar
charguer committed
169

charguer's avatar
cp    
charguer committed
170
171
172
173
174
175
(** [app_keep f xs H Q] is the same as [app f xs H (Q \*+ H)] *)

Notation "'app_keep' f xs H Q" :=
  (app f xs H%h (Q \*+ H))
  (at level 80, f at level 0, xs at level 0, H at level 0) : charac.

charguer's avatar
charguer committed
176
177
178

(** Reformulation of the definition *)

charguer's avatar
charguer committed
179
Lemma app_ge_2_unfold : 
charguer's avatar
charguer committed
180
181
  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
  (xs <> nil) ->
charguer's avatar
charguer committed
182
    app f ((dyn x)::xs) H Q 
charguer's avatar
charguer committed
183
  = app_basic f x H
charguer's avatar
charguer committed
184
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q]).
charguer's avatar
charguer committed
185
186
187
188
Proof using. 
  intros. destruct xs. false. auto.
Qed.

charguer's avatar
charguer committed
189
Lemma app_ge_2_unfold' : 
charguer's avatar
charguer committed
190
191
  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
  (length xs >= 1)%nat ->
charguer's avatar
charguer committed
192
    app f ((dyn x)::xs) H Q 
charguer's avatar
charguer committed
193
  = app_basic f x H
charguer's avatar
charguer committed
194
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q]).
charguer's avatar
charguer committed
195
Proof using. 
charguer's avatar
charguer committed
196
  intros. rewrite~ app_ge_2_unfold. destruct xs; rew_list in *.
charguer's avatar
charguer committed
197
198
199
200
  math.
  introv N. false.
Qed.

charguer's avatar
charguer committed
201
Lemma app_ge_2_unfold_extens : 
charguer's avatar
charguer committed
202
203
  forall (f:func) A (x:A) (xs:list dynamic) B,
  (xs <> nil) ->
charguer's avatar
charguer committed
204
    app_def f ((dyn x)::xs) (B:=B)
charguer's avatar
charguer committed
205
  = (fun H Q => app_basic f x H
charguer's avatar
charguer committed
206
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q])).
charguer's avatar
charguer committed
207
Proof using. 
charguer's avatar
charguer committed
208
  introv N. applys func_ext_2. intros H Q. rewrite~ app_ge_2_unfold.
charguer's avatar
charguer committed
209
210
Qed.

charguer's avatar
charguer committed
211
(** Weaken-frame-gc for [app] -- auxiliary lemma for [app_local]. *)
charguer's avatar
charguer committed
212

charguer's avatar
charguer committed
213
214
Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop),  
  app f xs H1 Q1 ->
charguer's avatar
charguer committed
215
216
  H ==> (H1 \* H2) ->
  (Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) ->
charguer's avatar
charguer committed
217
  app f xs H Q.
charguer's avatar
charguer committed
218
219
220
Proof using.
  intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false.
  tests E: (xs = nil).
charguer's avatar
cp    
charguer committed
221
    simpls. applys~ local_frame_gc M. 
charguer's avatar
charguer committed
222
    rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
charguer's avatar
cp    
charguer committed
223
     applys~ local_frame M. intros g.
charguer's avatar
charguer committed
224
225
226
     hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
Qed.

charguer's avatar
charguer committed
227
228
Lemma app_weaken : forall B f xs H (Q Q':B->hprop),  
  app f xs H Q ->
charguer's avatar
charguer committed
229
  Q ===> Q' -> 
charguer's avatar
charguer committed
230
  app f xs H Q'.  
charguer's avatar
charguer committed
231
Proof using.   
charguer's avatar
charguer committed
232
  introv M W. applys* app_wgframe. hsimpl. intros r. hsimpl~ \[].
charguer's avatar
charguer committed
233
234
235
236
Qed.

(* DEPRECATED

charguer's avatar
charguer committed
237
238
239
Lemma app_frame : forall B f xs H H' (Q:B->hprop),  
  app f xs H Q ->
  app f xs (H \* H') (Q \*+ H').
charguer's avatar
charguer committed
240
241
242
Proof using.
  intros B f xs. gen f. induction xs as [|[A x] xs]; introv M. false.
  tests E: (xs = nil).
charguer's avatar
cp    
charguer committed
243
    simpls. applys~ local_frame M.
charguer's avatar
charguer committed
244
    rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
charguer's avatar
cp    
charguer committed
245
     applys~ local_frame M. intros g.
charguer's avatar
charguer committed
246
247
248
     hextract as HR LR. hsimpl (HR \* H'). applys* IHxs. 
Qed.

charguer's avatar
charguer committed
249
250
Lemma app_weaken : forall B f xs H (Q Q':B->hprop),  
  app f xs H Q ->
charguer's avatar
charguer committed
251
  Q ===> Q' -> 
charguer's avatar
charguer committed
252
  app f xs H Q'.
charguer's avatar
charguer committed
253
254
255
256
Proof using.
  intros B f xs. gen f. induction xs as [|[A x] xs]; introv M W. false.
  tests E: (xs = nil).
    simpls. applys~ local_weaken_post M.
charguer's avatar
charguer committed
257
    rewrite~ app_ge_2_unfold'. rewrite~ app_ge_2_unfold' in M.
charguer's avatar
charguer committed
258
259
260
261
262
     applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs. 
Qed.

*)

charguer's avatar
charguer committed
263
(** Local property for [app] *)
charguer's avatar
charguer committed
264

charguer's avatar
charguer committed
265
266
Lemma app_local : forall f xs B,
  xs <> nil -> is_local (app_def f xs (B:=B)).
charguer's avatar
charguer committed
267
268
269
270
271
Proof using.
  introv N. apply is_local_prove. intros H Q.
  destruct xs as [|[A1 x1] xs]; tryfalse.
  destruct xs as [|[A2 x2] xs].
  { simpl. rewrite~ <- app_basic_local. iff*. }
charguer's avatar
charguer committed
272
  { rewrite app_ge_2_unfold_extens; auto_false.
charguer's avatar
charguer committed
273
274
275
276
277
278
279
    iff M.
    apply local_erase. auto.
    rewrite app_basic_local.
    intros h Hh. specializes M Hh. 
    destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits.
    eauto. eauto.
    intros g. hextract as H' L. hsimpl (H' \* H2).
charguer's avatar
charguer committed
280
    applys app_wgframe L. hsimpl. hchange R3. hsimpl. }
charguer's avatar
charguer committed
281
282
Qed.

charguer's avatar
charguer committed
283
Hint Resolve app_local.
charguer's avatar
charguer committed
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298


(********************************************************************)
(* ** Definition of [curried]  *)

(** [curried n f] asserts that [n-1] first applications of [f] are total *)

Fixpoint curried (n:nat) (f:func) : Prop :=
  match n with
  | O => False
  | S O => True
  | S n => forall A (x:A),
     app_basic f x \[]
       (fun g => \[ curried n g
          /\ forall xs B H (Q:B->hprop), length xs = n ->
charguer's avatar
charguer committed
299
               app f ((dyn x)::xs) H Q -> app g xs H Q])
charguer's avatar
charguer committed
300
301
302
303
304
305
306
307
308
309
  end.

(** Unfolding lemma for [curried] *)

Lemma curried_ge_2_unfold : forall n f,
  (n > 1)%nat -> 
    curried n f
  = forall A (x:A), app_basic f x \[]
    (fun g => \[    curried (pred n) g 
                 /\ forall xs B H (Q:B->hprop), length xs = (pred n) ->
charguer's avatar
charguer committed
310
                       app f ((dyn x)::xs) H Q -> app g xs H Q]).
charguer's avatar
charguer committed
311
312
313
314
315
316
317
318
Proof using.
  introv N. destruct n. math. destruct n. math. auto.
Qed.


(********************************************************************)
(* ** Lemma for over-applications *)

charguer's avatar
charguer committed
319
320
(** [app f (xs++ys)] can be expressed as [app f xs] that returns 
    a function [g] such that the behavior is that of [app g ys]. *)
charguer's avatar
charguer committed
321

charguer's avatar
charguer committed
322
Lemma app_over_app : forall xs ys f B H (Q:B->hprop), 
charguer's avatar
charguer committed
323
  (length xs > 0)%nat -> (length ys > 0)%nat ->
charguer's avatar
charguer committed
324
325
326
    app f (xs++ys) H Q 
  = app f xs H (fun g => Hexists H', H' \*
                                   \[ app g ys H' Q ]).
charguer's avatar
charguer committed
327
328
329
330
331
Proof using.
  induction xs. rew_list. math. introv N1 N2. rew_list.
  destruct a as [A x].
  destruct xs.
    rew_list. simpl. destruct ys. rew_list in *. math. auto.
charguer's avatar
charguer committed
332
  sets_eq xs': (d :: xs). do 2 (rewrite app_ge_2_unfold;
charguer's avatar
charguer committed
333
334
335
336
337
338
339
340
   [ | subst; rew_list; auto_false ]).
  fequal. apply func_ext_1. intros g. 
  apply func_equal_1. auto. apply func_ext_1. intros H'.
  fequal. fequal. apply IHxs. subst. rew_list. math. math.
Qed. 

(** Alternative formulation *)

charguer's avatar
charguer committed
341
Lemma app_over_take : forall n xs f B H (Q:B->hprop), 
charguer's avatar
charguer committed
342
  (0 < n < length xs)%nat ->
charguer's avatar
charguer committed
343
344
345
    app f xs H Q 
  = app f (take n xs) H (fun g => Hexists H', H' \*
                                   \[ app g (drop n xs) H' Q ]).
charguer's avatar
charguer committed
346
347
348
349
Proof using.
  introv N.
  forwards* (M&E1&E2): take_and_drop n xs. math.
  set (xs' := xs) at 1. change xs with xs' in M. rewrite M.
charguer's avatar
charguer committed
350
  subst xs'. rewrite app_over_app; try math. auto.
charguer's avatar
charguer committed
351
352
353
354
355
356
357
Qed.


(********************************************************************)
(* ** Lemma for partial-applications *)

(** When [curried n f] holds and the number of the arguments [xs]
charguer's avatar
charguer committed
358
359
    is less than [n], then [app f xs] is a function [g] such that
    [app g ys] has the same behavior as [app f (xs++ys)]. *)
charguer's avatar
charguer committed
360

charguer's avatar
charguer committed
361
Lemma app_partial : forall n xs f,
charguer's avatar
charguer committed
362
  curried n f -> (0 < length xs < n)%nat ->
charguer's avatar
charguer committed
363
  app f xs \[] (fun g => \[ 
charguer's avatar
charguer committed
364
365
    curried (n - length xs)%nat g /\
    forall ys B H (Q:B->hprop), (length xs + length ys = n)%nat ->
charguer's avatar
charguer committed
366
      app f (xs++ys) H Q -> app g ys H Q]).
charguer's avatar
charguer committed
367
368
369
370
371
Proof using.
  intros n. induction_wf IH: lt_wf n. introv C N.
  destruct xs as [|[A x] zs]. rew_list in N. math.
  rewrite curried_ge_2_unfold in C; [|math]. 
  tests E: (zs = nil).
charguer's avatar
charguer committed
372
  { unfold app_def at 1. eapply local_weaken_post. auto. applys (rm C).
charguer's avatar
charguer committed
373
374
375
376
    intros g. hextract as [M1 M2]. hsimpl. split. 
      rew_list. applys_eq M1 2. math.
      introv E AK. rew_list in *. applys M2. math. auto. }
  { asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. }
charguer's avatar
charguer committed
377
    rew_list in N. rewrite~ app_ge_2_unfold.
charguer's avatar
charguer committed
378
379
    eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *)
    intros h. hextract as [M1 M2]. hsimpl.
charguer's avatar
charguer committed
380
    applys app_weaken. applys (rm IH) M1. math. math. clear IH.
charguer's avatar
charguer committed
381
382
383
384
385
    intros g. hextract as [N1 N2]. hsimpl. split. 
    { rew_list. applys_eq N1 2. math. }
    { introv P1 P2. rew_list in P1. 
      applys N2. math.
      applys M2. rew_list; math.
charguer's avatar
charguer committed
386
      rew_list in P2. applys P2. } }
charguer's avatar
charguer committed
387
388
389
Qed.


charguer's avatar
charguer committed
390
(********************************************************************)
charguer's avatar
charguer committed
391
392
(* ** Packaging *)

charguer's avatar
charguer committed
393
394
395
396
397
398
399
400

(** [spec f n P] asserts that [curried f n] is true and that  
    the proposition [P] is a valid specification for [f]. 
    This formulation is useful for conciseness and tactics. *)

Definition spec (f:func) (n:nat) (P:Prop) :=
  curried n f /\ P.

charguer's avatar
xlet    
charguer committed
401
Global Opaque app_def curried.
charguer's avatar
xapp    
charguer committed
402

charguer's avatar
charguer committed
403
404

(********************************************************************)
charguer's avatar
charguer committed
405
(* ** Record axiomatization *)
charguer's avatar
charguer committed
406

charguer's avatar
charguer committed
407
408
409
(** Representation predicate [r ~> record_repr L], where [L]
    is an association list from fields (natural numbers) to
    dependent pairs (a value accompanied with its type). *)
charguer's avatar
charguer committed
410
411
412
413
414
415
416
417
418
419
420

Definition record_descr := list (nat * dynamic).

Axiom record_repr_one : forall (f:nat) A (v:A) (r:loc), hprop.

Fixpoint record_repr (L:record_descr) (r:loc) : hprop :=
  match L with
  | nil => \[]
  | (f, dyn v)::L' => r ~> record_repr_one f v \* r ~> record_repr L'
  end. 

charguer's avatar
charguer committed
421
422
423
424
425
  (* DEPRECATED
  Axiom record_repr : record_descr -> loc -> hprop. 
  Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop := 
    r ~> record_repr ((f, dyn v)::nil).
  *)
charguer's avatar
charguer committed
426

charguer's avatar
charguer committed
427
428
429
(* Axiomatic specification of [new] on a list of fields;
   [app_record_new L] is a characteristic formula describing
   the allocation of a record. *)
charguer's avatar
charguer committed
430

charguer's avatar
records    
charguer committed
431
432
Definition app_record_new (L:record_descr) : ~~loc :=
  local (fun H Q => (fun r => H \* r ~> record_repr L) ===> Q).
charguer's avatar
charguer committed
433

charguer's avatar
charguer committed
434
435
436
437
  (* Remark: taking the definition below would be a bit of a hack,
     and it turns out that Coq rejects the definition for universe
     reasons, because a value of type [dynamic] cannot be stored
     into a heap cell, which is itself made of a dynamic value. 
charguer's avatar
charguer committed
438

charguer's avatar
charguer committed
439
440
441
442
       Axiom record_new : func.
       Axiom record_new_spec : forall (r:loc) (L:record_descr),
         app record_new [L] \[] (# r ~> record_repr L). 
  *)
charguer's avatar
charguer committed
443

charguer's avatar
charguer committed
444
(* Axiomatic specification of [get] on a single-field *)
charguer's avatar
charguer committed
445

charguer's avatar
charguer committed
446
Axiom record_get : func.
charguer's avatar
charguer committed
447

charguer's avatar
charguer committed
448
449
450
451
Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A),
  app_keep record_get [r f] 
    (r ~> record_repr_one f v) 
    \[= v].
charguer's avatar
charguer committed
452

charguer's avatar
charguer committed
453
(* Axiomatic specification of [set] on a single-field *)
charguer's avatar
charguer committed
454

charguer's avatar
charguer committed
455
Axiom record_set : func.
charguer's avatar
charguer committed
456

charguer's avatar
charguer committed
457
458
459
460
Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B),
  app record_set [r f w] 
    (r ~> record_repr_one f v) 
    (# r ~> record_repr_one f w).
charguer's avatar
charguer committed
461
462
463
464




charguer's avatar
charguer committed
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
(********************************************************************)
(* ** Record notation *)

(** Notation for the contents of the fields *)

Notation "`{ f1 := x1 }'" := 
  ((f1, dyn x1)::nil)
  (at level 0, f1 at level 0) 
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::nil)
  (at level 0, f1 at level 0, f2 at level 0) 
  : record_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) 
  : record_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)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::(f7, dyn x7)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0, f7 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::(f7, dyn x7)::(f8, dyn x8)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
  : record_scope.

Delimit Scope record_scope with record.
Open Scope record_scope.
charguer's avatar
charguer committed
512

charguer's avatar
charguer committed
513
514
515
Notation "'rec' L" :=
  (@record_repr (L)%record)  (* (@app_def f (xs)%dynlist _) *)
  (at level 69) : charac.
charguer's avatar
charguer committed
516

charguer's avatar
charguer committed
517
Open Scope charac.
charguer's avatar
charguer committed
518

charguer's avatar
charguer committed
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
(** Notation for characteristic formulae *)

Notation "`{ f1 := x1 }" :=
  (rec `{ f1 := x1 }')
  (at level 0, f1 at level 0) 
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 }" :=
  (rec `{ f1 := x1 ; f2 := x2 }')
  (at level 0, f1 at level 0, f2 at level 0) 
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5; 
  f6 := x6 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5;
   f6 := x6 ; f7 := x7 }') 
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0, f7 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5;
   f6 := x6 ; f7 := x7 ; f8 := x8 }') 
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, 
   f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
  : charac.


(********************************************************************)
(* ** Computated derived specifications for [get] and [set] on records *)
charguer's avatar
charguer committed
564
565
566
567

Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic :=
  match L with
  | nil => None
charguer's avatar
charguer committed
568
569
570
571
  | (f',d')::T' => 
     if Nat.eq_dec f f' 
       then Some d' 
       else record_get_compute_dyn f T'
charguer's avatar
charguer committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
  end.

Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop :=
  match record_get_compute_dyn f L with
  | None => None 
  | Some (dyn v) => Some (forall r,
     app_keep record_get [r f] (r ~> record_repr L) \[= v])
  end.

Lemma record_get_compute_spec_correct : forall f L (P:Prop),
  record_get_compute_spec f L = Some P -> P.
Proof using.
  introv M. unfolds record_get_compute_spec. 
  sets_eq <- do E: (record_get_compute_dyn f L).
  destruct do as [[T v]|]; inverts M.
charguer's avatar
charguer committed
587
  induction L as [|[f' [D' d']] T']; [false|]. 
charguer's avatar
charguer committed
588
  simpl in E.
charguer's avatar
charguer committed
589
  intros r. do 2 xunfold record_repr at 1. simpl. case_if.
charguer's avatar
charguer committed
590
591
592
593
594
595
  { inverts E.
    eapply local_frame. 
    { apply app_local. auto_false. }
    { apply record_get_spec. }
    { hsimpl. } 
    { hsimpl~. } }
charguer's avatar
charguer committed
596
  { specializes IHT' (rm E).
charguer's avatar
charguer committed
597
598
    eapply local_frame. 
    { apply app_local. auto_false. }
charguer's avatar
charguer committed
599
    { apply IHT'. }
charguer's avatar
charguer committed
600
601
602
603
    { hsimpl. } 
    { hsimpl~. } }
Qed. (* todo: could use xapply in this proof *)

charguer's avatar
charguer committed
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631

Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option record_descr :=
  match L with
  | nil => None
  | (f',d')::T' => 
     if Nat.eq_dec f f' 
       then Some ((f,d)::T') 
       else match record_set_compute_dyn f d T' with
            | None => None
            | Some L' => Some ((f',d')::L')
            end
  end.

Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Prop :=
  match record_set_compute_dyn f (dyn w) L with
  | None => None 
  | Some L' => Some (forall r,
     app record_set [r f w] (r ~> record_repr L) (# r ~> record_repr L'))
  end.

Lemma record_set_compute_spec_correct : forall f A (w:A) L (P:Prop),
  record_set_compute_spec f w L = Some P -> P.
Proof using.
  introv M. unfolds record_set_compute_spec. 
  sets_eq <- do E: (record_set_compute_dyn f (dyn w) L).
  destruct do as [L'|]; inverts M. 
  gen L'. induction L as [|[f' [T' v']] T]; intros; [false|].
  simpl in E.
charguer's avatar
charguer committed
632
  xunfold record_repr at 1. simpl. case_if.
charguer's avatar
charguer committed
633
634
635
636
637
  { inverts E.
    eapply local_frame. 
    { apply app_local. auto_false. }
    { apply record_set_spec. }
    { hsimpl. } 
charguer's avatar
charguer committed
638
    { xunfold record_repr at 2. simpl. hsimpl~. } }
charguer's avatar
charguer committed
639
640
641
642
643
644
  { cases (record_set_compute_dyn f Dyn (w) T) as C; [|false].
    inverts E. specializes~ IHT r.
    eapply local_frame. 
    { apply app_local. auto_false. }
    { apply IHT. }
    { hsimpl. } 
charguer's avatar
charguer committed
645
    { xunfold record_repr at 2. simpl. hsimpl~. } }
charguer's avatar
charguer committed
646
647
648
649
Qed. (* todo: could use xapply in this proof *)


(* DEPRECATED
charguer's avatar
charguer committed
650
651
652
653
654
655
656
657
658
  Lemma record_get_compute_spec_correct' : forall f L,
    match record_get_compute_spec f L with 
    | None => True
    | Some P => P
    end.
  Proof using.
    intros. cases (record_get_compute_spec f L).
    applys* record_get_compute_spec_correct. auto.
  Qed.
charguer's avatar
charguer committed
659
*)
charguer's avatar
charguer committed
660
661


charguer's avatar
records    
charguer committed
662
Global Opaque record_repr.
charguer's avatar
charguer committed
663
664
665
666
667





charguer's avatar
charguer committed
668
669
670
671
672
673