source: C-semantics/Globalenvs.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 9 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

File size: 42.6 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Global environments are a component of the dynamic semantics of
17  all languages involved in the compiler.  A global environment
18  maps symbol names (names of functions and of global variables)
19  to the corresponding memory addresses.  It also maps memory addresses
20  of functions to the corresponding function descriptions. 
21
22  Global environments, along with the initial memory state at the beginning
23  of program execution, are built from the program of interest, as follows:
24- A distinct memory address is assigned to each function of the program.
25  These function addresses use negative numbers to distinguish them from
26  addresses of memory blocks.  The associations of function name to function
27  address and function address to function description are recorded in
28  the global environment.
29- For each global variable, a memory block is allocated and associated to
30  the name of the variable.
31
32  These operations reflect (at a high level of abstraction) what takes
33  place during program linking and program loading in a real operating
34  system. *)
35
36include "Errors.ma".
37include "AST.ma".
38include "Values.ma".
39include "Mem.ma".
40
41(* FIXME: unimplemented stuff in AST.ma
42naxiom transform_program: ∀A,B,V:Type. (A → B) → program A V → program B V.
43naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V).
44naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W).
45naxiom match_program: ∀A,B,V,W:Type. program A V → program B W → Prop.
46*)
47
48nrecord GENV : Type[1] ≝ {
49(* * ** Types and operations *)
50
51  genv_t : Type → Type;
52   (* * The type of global environments.  The parameter [F] is the type
53       of function descriptions. *)
54
55  globalenv: ∀F,V: Type. program F V → genv_t F;
56   (* * Return the global environment for the given program. *)
57
58  init_mem: ∀F,V: Type. program F V → mem;
59   (* * Return the initial memory state for the given program. *)
60
61  find_funct_ptr: ∀F: Type. genv_t F → block → option F;
62   (* * Return the function description associated with the given address,
63       if any. *)
64
65  find_funct: ∀F: Type. genv_t F → val → option F;
66   (* * Same as [find_funct_ptr] but the function address is given as
67       a value, which must be a pointer with offset 0. *)
68
69  find_symbol: ∀F: Type. genv_t F → ident → option block
70   (* * Return the address of the given global symbol, if any. *)
71}.
72(* * ** Properties of the operations. *)
73(*
74  find_funct_inv:
75    ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F.
76    find_funct ? ge v = Some ? f → ∃b. v = Vptr b zero;
77  find_funct_find_funct_ptr:
78    ∀F: Type. ∀ge: t F. ∀b: block.
79    find_funct ? ge (Vptr b zero) = find_funct_ptr ? ge b;
80
81  find_symbol_exists:
82    ∀F,V: Type. ∀p: program F V.
83           ∀id: ident. ∀init: list init_data. ∀v: V.
84    in_list ? 〈〈id, init〉, v〉 (prog_vars ?? p) →
85    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
86  find_funct_ptr_exists:
87    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀f: F.
88    list_norepet ? (prog_funct_names ?? p) →
89    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
90    in_list ? 〈id, f〉 (prog_funct ?? p) →
91    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b
92           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
93
94  find_funct_ptr_inversion:
95    ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
96    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
97    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
98  find_funct_inversion:
99    ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
100    find_funct ? (globalenv ?? p) v = Some ? f →
101    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
102  find_funct_ptr_symbol_inversion:
103    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block. ∀f: F.
104    find_symbol ? (globalenv ?? p) id = Some ? b →
105    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
106    in_list ? 〈id, f〉 (prog_funct ?? p);
107
108  find_funct_ptr_prop:
109    ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
110    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
111    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
112    P f;
113  find_funct_prop:
114    ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
115    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
116    find_funct ? (globalenv ?? p) v = Some ? f →
117    P f;
118
119  initmem_nullptr:
120    ∀F,V: Type. ∀p: program F V.
121    let m ≝ init_mem ?? p in
122    valid_block m nullptr ∧
123    (blocks m) nullptr = empty_block 0 0;
124  initmem_inject_neutral:
125    ∀F,V: Type. ∀p: program F V.
126    mem_inject_neutral (init_mem ?? p);
127  find_funct_ptr_negative:
128    ∀F,V: Type. ∀p: program F V. ∀b: block. ∀f: F.
129    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
130  find_symbol_not_fresh:
131    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block.
132    find_symbol ? (globalenv ?? p) id = Some ? b → b < nextblock (init_mem ?? p);
133  find_symbol_not_nullptr:
134    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block.
135    find_symbol ? (globalenv ?? p) id = Some ? b → b ≠ nullptr;
136  global_addresses_distinct:
137    ∀F,V: Type. ∀p: program F V. ∀id1,id2,b1,b2.
138    id1≠id2 →
139    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
140    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
141    b1≠b2(*;
142
143(* * Commutation properties between program transformations
144  and operations over global environments. *)
145
146  find_funct_ptr_transf:
147    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
148    ∀b: block. ∀f: A.
149    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
150    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);
151  find_funct_transf:
152    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
153    ∀v: val. ∀f: A.
154    find_funct ? (globalenv ?? p) v = Some ? f →
155    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);
156  find_symbol_transf:
157    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
158    ∀s: ident.
159    find_symbol ? (globalenv ?? (transform_program … transf p)) s =
160    find_symbol ? (globalenv ?? p) s;
161  init_mem_transf:
162    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
163    init_mem ?? (transform_program … transf p) = init_mem ?? p;
164  find_funct_ptr_rev_transf:
165    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
166    ∀b : block. ∀tf : B.
167    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
168    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
169  find_funct_rev_transf:
170    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
171    ∀v : val. ∀tf : B.
172    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
173    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
174
175(* * Commutation properties between partial program transformations
176  and operations over global environments. *)
177
178  find_funct_ptr_transf_partial:
179    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
180    transform_partial_program … transf p = OK ? p' →
181    ∀b: block. ∀f: A.
182    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
183    ∃f'.
184    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
185  find_funct_transf_partial:
186    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
187    transform_partial_program … transf p = OK ? p' →
188    ∀v: val. ∀f: A.
189    find_funct ? (globalenv ?? p) v = Some ? f →
190    ∃f'.
191    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
192  find_symbol_transf_partial:
193    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
194    transform_partial_program … transf p = OK ? p' →
195    ∀s: ident.
196    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
197  init_mem_transf_partial:
198    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
199    transform_partial_program … transf p = OK ? p' →
200    init_mem ?? p' = init_mem ?? p;
201  find_funct_ptr_rev_transf_partial:
202    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
203    transform_partial_program … transf p = OK ? p' →
204    ∀b : block. ∀tf : B.
205    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
206    ∃f : A.
207      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
208  find_funct_rev_transf_partial:
209    ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
210    transform_partial_program … transf p = OK ? p' →
211    ∀v : val. ∀tf : B.
212    find_funct ? (globalenv ?? p') v = Some ? tf →
213    ∃f : A.
214      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf;
215
216  find_funct_ptr_transf_partial2:
217    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
218           ∀p: program A V. ∀p': program B W.
219    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
220    ∀b: block. ∀f: A.
221    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
222    ∃f'.
223    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
224  find_funct_transf_partial2:
225    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
226           ∀p: program A V. ∀p': program B W.
227    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
228    ∀v: val. ∀f: A.
229    find_funct ? (globalenv ?? p) v = Some ? f →
230    ∃f'.
231    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
232  find_symbol_transf_partial2:
233    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
234           ∀p: program A V. ∀p': program B W.
235    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
236    ∀s: ident.
237    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
238  init_mem_transf_partial2:
239    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
240           ∀p: program A V. ∀p': program B W.
241    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
242    init_mem ?? p' = init_mem ?? p;
243  find_funct_ptr_rev_transf_partial2:
244    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
245           ∀p: program A V. ∀p': program B W.
246    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
247    ∀b: block. ∀tf: B.
248    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
249    ∃f : A.
250      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
251  find_funct_rev_transf_partial2:
252    ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
253           ∀p: program A V. ∀p': program B W.
254    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
255    ∀v: val. ∀tf: B.
256    find_funct ? (globalenv ?? p') v = Some ? tf →
257    ∃f : A.
258      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;
259
260(* * Commutation properties between matching between programs
261  and operations over global environments. *)
262
263  find_funct_ptr_match:
264    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
265           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
266    match_program … match_fun match_var p p' →
267    ∀b: block. ∀f: A.
268    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
269    ∃tf : B.
270    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
271  find_funct_ptr_rev_match:
272    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
273           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
274    match_program … match_fun match_var p p' →
275    ∀b: block. ∀tf: B.
276    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
277    ∃f : A.
278    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
279  find_funct_match:
280    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
281           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
282    match_program … match_fun match_var p p' →
283    ∀v: val. ∀f: A.
284    find_funct ? (globalenv ?? p) v = Some ? f →
285    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
286  find_funct_rev_match:
287    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
288           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
289    match_program … match_fun match_var p p' →
290    ∀v: val. ∀tf: B.
291    find_funct ? (globalenv ?? p') v = Some ? tf →
292    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
293  find_symbol_match:
294    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
295           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
296    match_program … match_fun match_var p p' →
297    ∀s: ident.
298    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
299  init_mem_match:
300    ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
301           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
302    match_program … match_fun match_var p p' →
303    init_mem ?? p' = init_mem ?? p*)
304}.
305*)
306
307(* XXX: temporary definition
308   NB: only global functions, no global variables *)
309nrecord genv (F:Type) : Type ≝ {
310  functions: block → option F;
311  nextfunction: Z;
312  symbols: ident → option block
313}.
314
315ndefinition Genv : GENV ≝ mk_GENV
316  genv  (* genv_t *)
317  (λF,V,p. foldr ??
318    (λf,ge. match f with [ mk_pair id def ⇒
319            let b ≝ nextfunction ? ge in
320            mk_genv ? (λb'. if eqZb b b' then Some ? def else (functions ? ge b'))
321                      (Zsucc b)
322                      (λi. match ident_eq id i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? ge i)])
323            ])
324   (mk_genv ? (λ_.None ?) 0 (λ_.None ?)) (prog_funct ?? p))  (* globalenv *)
325  (λF,V,p. empty)  (* init_mem *)
326  (λF,ge. functions ? ge) (* find_funct_ptr *)
327  (λF,ge,v. match v with [ Vptr b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
328  (λF,ge. symbols ? ge) (* find_symbol *)
329.
330
331(*
332(** The rest of this library is a straightforward implementation of
333  the module signature above. *)
334
335Module Genv: GENV.
336
337Section GENV.
338
339Variable F: Type.                    (* The type of functions *)
340Variable V: Type.                    (* The type of information over variables *)
341
342Record genv : Type := mkgenv {
343  functions: ZMap.t (option F);     (* mapping function ptr → function *)
344  nextfunction: Z;
345  symbols: PTree.t block                (* mapping symbol → block *)
346}.
347
348Definition t := genv.
349
350Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=
351  let b := g.(nextfunction) in
352  mkgenv (ZMap.set b (Some ? (snd name_fun)) g.(functions))
353         (Zpred b)
354         (PTree.set (fst name_fun) b g.(symbols)).
355
356Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
357  mkgenv g.(functions)
358         g.(nextfunction)
359         (PTree.set name b g.(symbols)).
360
361Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
362  ZMap.get b g.(functions).
363
364Definition find_funct (g: genv) (v: val) : option F :=
365  match v with
366  | Vptr b ofs =>
367      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
368  | _ =>
369      None
370  end.
371
372Definition find_symbol ? (g: genv) (symb: ident) : option block :=
373  PTree.get symb g.(symbols).
374
375Lemma find_funct_inv:
376  forall (ge: t) (v: val) (f: F),
377  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
378Proof.
379  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
380  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
381  exists b. congruence.
382  discriminate.
383Qed.
384
385Lemma find_funct_find_funct_ptr:
386  forall (ge: t) (b: block),
387  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
388Proof.
389  intros. simpl.
390  generalize (Int.eq_spec Int.zero Int.zero).
391  case (Int.eq Int.zero Int.zero); intros.
392  auto. tauto.
393Qed.
394
395(* Construct environment and initial memory store *)
396
397Definition empty : genv :=
398  mkgenv (ZMap.init None) (-1) (PTree.empty block).
399
400Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
401  List.fold_right add_funct init fns.
402
403Definition add_globals
404       (init: genv * mem) (vars: list (ident * list init_data * V))
405       : genv * mem :=
406  List.fold_right
407    (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>
408       match id_init, g_st with
409       | ((id, init), info), (g, st) =>
410           let (st', b) := Mem.alloc_init_data st init in
411           (add_symbol id b g, st')
412       end)
413    init vars.
414
415Definition globalenv_initmem (p: program F V) : (genv * mem) :=
416  add_globals
417    (add_functs empty p.(prog_funct), Mem.empty)
418    p.(prog_vars).
419
420Definition globalenv (p: program F V) : genv :=
421  fst (globalenv_initmem p).
422Definition init_mem  (p: program F V) : mem :=
423  snd (globalenv_initmem p).
424
425Lemma functions_globalenv:
426  forall (p: program F V),
427  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
428Proof.
429  assert (forall init vars,
430     functions (fst (add_globals init vars)) = functions (fst init)).
431  induction vars; simpl.
432  reflexivity.
433  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
434  simpl. exact IHvars.
435
436  unfold add_globals; simpl.
437  intros. unfold globalenv; unfold globalenv_initmem.
438  rewrite H. reflexivity.
439Qed.
440
441Lemma initmem_nullptr:
442  forall (p: program F V),
443  let m := init_mem p in
444  valid_block m nullptr /\
445  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
446Proof.
447  pose (P := fun m => valid_block m nullptr /\
448        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
449  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
450  induction vars; simpl; intros.
451  auto.
452  destruct a as [[id1 in1] inf1].
453  destruct (add_globals init vars) as [g st].
454  simpl in *. destruct IHvars. split.
455  red; simpl. red in H0. omega.
456  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
457
458  intro. unfold init_mem, globalenv_initmem. apply H.
459  red; simpl. split. compute. auto. reflexivity.
460Qed.
461
462Lemma initmem_inject_neutral:
463  forall (p: program F V),
464  mem_inject_neutral (init_mem p).
465Proof.
466  assert (forall g0 vars g1 m,
467      add_globals (g0, Mem.empty) vars = (g1, m) →
468      mem_inject_neutral m).
469  Opaque alloc_init_data.
470  induction vars; simpl.
471  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
472  simpl in H1. rewrite Mem.getN_init in H1.
473  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
474  destruct a as [[id1 init1] info1].
475  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
476  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
477  intros. inv H.
478  eapply Mem.alloc_init_data_neutral; eauto.
479  intros. caseEq (globalenv_initmem p). intros g m EQ.
480  unfold init_mem; rewrite EQ; simpl.
481  unfold globalenv_initmem in EQ. eauto.
482Qed.     
483
484Remark nextfunction_add_functs_neg:
485  forall fns, nextfunction (add_functs empty fns) < 0.
486Proof.
487  induction fns; simpl; intros. omega. unfold Zpred. omega.
488Qed.
489
490Theorem find_funct_ptr_negative:
491  forall (p: program F V) (b: block) (f: F),
492  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
493Proof.
494  intros until f.
495  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
496    induction fns; simpl.
497    rewrite ZMap.gi. congruence.
498    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
499    intro. rewrite e. apply nextfunction_add_functs_neg.
500    auto.
501  unfold find_funct_ptr. rewrite functions_globalenv.
502  intros. eauto.
503Qed.
504
505Remark find_symbol_add_functs_negative:
506  forall (fns: list (ident * F)) s b,
507  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
508Proof.
509  induction fns; simpl; intros until b.
510  rewrite PTree.gempty. congruence.
511  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
512  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
513  eauto.
514Qed.
515
516Remark find_symbol_add_symbols_not_fresh:
517  forall fns vars g m s b,
518  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
519  (symbols g)!s = Some ? b →
520  b < nextblock m.
521Proof.
522  induction vars; simpl; intros until b.
523  intros. inversion H. subst g m. simpl.
524  generalize (find_symbol_add_functs_negative fns s H0). omega.
525  Transparent alloc_init_data.
526  destruct a as [[id1 init1] info1].
527  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
528  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
529  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
530  intro EQ; inversion EQ. omega.
531  intro. generalize (IHvars _ _ _ _ ADG H). omega.
532Qed.
533
534Theorem find_symbol_not_fresh:
535  forall (p: program F V) (id: ident) (b: block),
536  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
537Proof.
538  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
539  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
540                      (prog_vars p)); intros g m EQ.
541  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
542Qed.
543
544Lemma find_symbol_exists:
545  forall (p: program F V)
546         (id: ident) (init: list init_data) (v: V),
547  In (id, init, v) (prog_vars p) →
548  ∃b. find_symbol ? (globalenv p) id = Some ? b.
549Proof.
550  intros until v.
551  assert (forall initm vl, In (id, init, v) vl →
552           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
553  induction vl; simpl; intros.
554  elim H.
555  destruct a as [[id0 init0] v0].
556  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
557  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
558  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
559  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
560Qed.
561
562Remark find_symbol_above_nextfunction:
563  forall (id: ident) (b: block) (fns: list (ident * F)),
564  let g := add_functs empty fns in
565  PTree.get id g.(symbols) = Some ? b →
566  b > g.(nextfunction).
567Proof.
568  induction fns; simpl.
569  rewrite PTree.gempty. congruence.
570  rewrite PTree.gsspec. case (peq id (fst a)); intro.
571  intro EQ. inversion EQ. unfold Zpred. omega.
572  intros. generalize (IHfns H). unfold Zpred; omega.
573Qed.
574
575Remark find_symbol_add_globals:
576  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
577  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
578  find_symbol ? (fst (add_globals ge_m vars)) id =
579  find_symbol ? (fst ge_m) id.
580Proof.
581  unfold find_symbol; induction vars; simpl; intros.
582  auto.
583  destruct a as [[id0 init0] var0]. simpl in *.
584  caseEq (add_globals ge_m vars); intros ge' m' EQ.
585  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
586  apply IHvars. tauto. intuition congruence.
587Qed.
588
589Lemma find_funct_ptr_exists:
590  forall (p: program F V) (id: ident) (f: F),
591  list_norepet (prog_funct_names p) →
592  list_disjoint (prog_funct_names p) (prog_var_names p) →
593  In (id, f) (prog_funct p) →
594  ∃b. find_symbol ? (globalenv p) id = Some ? b
595         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
596Proof.
597  intros until f.
598  assert (forall (fns: list (ident * F)),
599           list_norepet (map (@fst ident F) fns) →
600           In (id, f) fns →
601           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
602                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
603  unfold find_symbol, find_funct_ptr. induction fns; intros.
604  elim H0.
605  destruct a as [id0 f0]; simpl in *. inv H.
606  unfold add_funct; simpl.
607  rewrite PTree.gsspec. destruct (peq id id0).
608  subst id0. econstructor; split. eauto.
609  replace f0 with f. apply ZMap.gss.
610  elim H0; intro. congruence. elim H3.
611  change id with (@fst ident F (id, f)). apply List.in_map. auto.
612  exploit IHfns; eauto. elim H0; intro. congruence. auto.
613  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
614  generalize (find_symbol_above_nextfunction _ _ X).
615  unfold block; unfold ZIndexed.t; intro; omega.
616
617  intros. exploit H; eauto. intros [b [X Y]].
618  exists b; split.
619  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
620  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
621  unfold prog_funct_names. change id with (fst (id, f)).
622  apply List.in_map; auto.
623  unfold find_funct_ptr. rewrite functions_globalenv.
624  assumption.
625Qed.
626
627Lemma find_funct_ptr_inversion:
628  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
629  find_funct_ptr ? (globalenv p) b = Some ? f →
630  ∃id. In (id, f) (prog_funct p).
631Proof.
632  intros until f.
633  assert (forall fns: list (ident * F),
634    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
635    ∃id. In (id, f) fns).
636  unfold find_funct_ptr. induction fns; simpl.
637  rewrite ZMap.gi. congruence.
638  destruct a as [id0 f0]; simpl.
639  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
640  intro. inv H. exists id0; auto.
641  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
642  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
643Qed.
644
645Lemma find_funct_ptr_prop:
646  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
647  (forall id f, In (id, f) (prog_funct p) → P f) →
648  find_funct_ptr ? (globalenv p) b = Some ? f →
649  P f.
650Proof.
651  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
652Qed.
653
654Lemma find_funct_inversion:
655  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
656  find_funct (globalenv p) v = Some ? f →
657  ∃id. In (id, f) (prog_funct p).
658Proof.
659  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
660  rewrite find_funct_find_funct_ptr ? in H.
661  eapply find_funct_ptr_inversion; eauto.
662Qed.
663
664Lemma find_funct_prop:
665  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
666  (forall id f, In (id, f) (prog_funct p) → P f) →
667  find_funct (globalenv p) v = Some ? f →
668  P f.
669Proof.
670  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
671Qed.
672
673Lemma find_funct_ptr_symbol_inversion:
674  forall (p: program F V) (id: ident) (b: block) (f: F),
675  find_symbol ? (globalenv p) id = Some ? b →
676  find_funct_ptr ? (globalenv p) b = Some ? f →
677  In (id, f) p.(prog_funct).
678Proof.
679  intros until f.
680  assert (forall fns,
681           let g := add_functs empty fns in
682           PTree.get id g.(symbols) = Some ? b →
683           ZMap.get b g.(functions) = Some ? f →
684           In (id, f) fns).
685    induction fns; simpl.
686    rewrite ZMap.gi. congruence.
687    set (g := add_functs empty fns).
688    rewrite PTree.gsspec. rewrite ZMap.gsspec.
689    case (peq id (fst a)); intro.
690    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
691    intro EQ2. left. destruct a. simpl in *. congruence.
692    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
693    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
694  assert (forall g0 m0, b < 0 →
695          forall vars g m,
696          add_globals (g0, m0) vars = (g, m) →
697          PTree.get id g.(symbols) = Some ? b →
698          PTree.get id g0.(symbols) = Some ? b).
699    induction vars; simpl.
700    intros. inv H1. auto.
701    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
702    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
703    unfold add_symbol; intros A B. rewrite <- B. simpl.
704    rewrite PTree.gsspec. case (peq id id1); intros.
705    assert (b > 0). inv H1. apply nextblock_pos.
706    omegaContradiction.
707    eauto.
708  intros.
709  generalize (find_funct_ptr_negative _ _ H2). intro.
710  pose (g := add_functs empty (prog_funct p)).
711  apply H. 
712  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
713  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
714  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
715Qed.
716
717Theorem find_symbol_not_nullptr:
718  forall (p: program F V) (id: ident) (b: block),
719  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
720Proof.
721  intros until b.
722  assert (forall fns,
723          find_symbol ? (add_functs empty fns) id = Some ? b →
724          b <> nullptr).
725    unfold find_symbol; induction fns; simpl.
726    rewrite PTree.gempty. congruence.
727    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
728    destruct (peq id id1); intros.
729    inversion H. generalize (nextfunction_add_functs_neg fns).
730    unfold block, nullptr; omega.
731    auto.
732  set (g0 := add_functs empty p.(prog_funct)).
733  assert (forall vars g m,
734          add_globals (g0, Mem.empty) vars = (g, m) →
735          find_symbol ? g id = Some ? b →
736          b <> nullptr).
737    induction vars; simpl; intros until m.
738    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
739    destruct a as [[id1 init1] info1].
740    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
741    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
742    destruct (peq id id1); intros.
743    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
744    eauto.
745  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
746Qed.
747
748Theorem global_addresses_distinct:
749  forall (p: program F V) id1 id2 b1 b2,
750  id1<>id2 →
751  find_symbol ? (globalenv p) id1 = Some ? b1 →
752  find_symbol ? (globalenv p) id2 = Some ? b2 →
753  b1<>b2.
754Proof.
755  intros.
756  assert (forall fns,
757    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
758    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
759    b1 <> b2).
760  unfold find_symbol. induction fns; simpl; intros.
761  rewrite PTree.gempty in H2. discriminate.
762  destruct a as [id f]; simpl in *.
763  rewrite PTree.gsspec in H2.
764  destruct (peq id1 id). subst id. inv H2.
765  rewrite PTree.gso in H3; auto.
766  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
767  rewrite PTree.gsspec in H3.
768  destruct (peq id2 id). subst id. inv H3.
769  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
770  eauto.
771  set (ge0 := add_functs empty p.(prog_funct)).
772  assert (forall (vars: list (ident * list init_data * V)) ge m,
773    add_globals (ge0, Mem.empty) vars = (ge, m) →
774    find_symbol ? ge id1 = Some ? b1 →
775    find_symbol ? ge id2 = Some ? b2 →
776    b1 <> b2).
777  unfold find_symbol. induction vars; simpl.
778  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
779  intros ge m. destruct a as [[id init] info].
780  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
781  unfold add_symbol. simpl. intros.
782  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
783  rewrite PTree.gso in H4; auto.
784  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
785  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
786  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
787  eauto.
788  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
789  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
790  fold ge_m. apply surjective_pairing. auto. auto.
791Qed.
792
793End GENV.
794
795(* Global environments and program transformations. *)
796
797Section MATCH_PROGRAM.
798
799Variable A B V W: Type.
800Variable match_fun: A → B → Prop.
801Variable match_var: V → W → Prop.
802Variable p: program A V.
803Variable p': program B W.
804Hypothesis match_prog:
805  match_program match_fun match_var p p'.
806
807Lemma add_functs_match:
808  forall (fns: list (ident * A)) (tfns: list (ident * B)),
809  list_forall2 (match_funct_entry match_fun) fns tfns →
810  let r := add_functs (empty A) fns in
811  let tr := add_functs (empty B) tfns in
812  nextfunction tr = nextfunction r /\
813  symbols tr = symbols r /\
814  forall (b: block) (f: A),
815  ZMap.get b (functions r) = Some ? f →
816  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
817Proof.
818  induction 1; simpl.
819
820  split. reflexivity. split. reflexivity.
821  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
822
823  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
824  simpl. red in H. destruct H.
825  destruct IHlist_forall2 as [X [Y Z]].
826  rewrite X. rewrite Y. 
827  split. auto.
828  split. congruence.
829  intros b f.
830  repeat (rewrite ZMap.gsspec).
831  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
832  intro EQ; inv EQ. exists fn2; auto.
833  auto.
834Qed.
835
836Lemma add_functs_rev_match:
837  forall (fns: list (ident * A)) (tfns: list (ident * B)),
838  list_forall2 (match_funct_entry match_fun) fns tfns →
839  let r := add_functs (empty A) fns in
840  let tr := add_functs (empty B) tfns in
841  nextfunction tr = nextfunction r /\
842  symbols tr = symbols r /\
843  forall (b: block) (tf: B),
844  ZMap.get b (functions tr) = Some ? tf →
845  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
846Proof.
847  induction 1; simpl.
848
849  split. reflexivity. split. reflexivity.
850  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
851
852  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
853  simpl. red in H. destruct H.
854  destruct IHlist_forall2 as [X [Y Z]].
855  rewrite X. rewrite Y. 
856  split. auto.
857  split. congruence.
858  intros b f.
859  repeat (rewrite ZMap.gsspec).
860  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
861  intro EQ; inv EQ. exists fn1; auto.
862  auto.
863Qed.
864
865Lemma mem_add_globals_match:
866  forall (g1: genv A) (g2: genv B) (m: mem)
867         (vars: list (ident * list init_data * V))
868         (tvars: list (ident * list init_data * W)),
869  list_forall2 (match_var_entry match_var) vars tvars →
870  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
871Proof.
872  induction 1; simpl.
873  auto.
874  destruct a1 as [[id1 init1] info1].
875  destruct b1 as [[id2 init2] info2].
876  red in H. destruct H as [X [Y Z]]. subst id2 init2.
877  generalize IHlist_forall2.
878  destruct (add_globals (g1, m) al).
879  destruct (add_globals (g2, m) bl).
880  simpl. intro. subst m1. auto.
881Qed.
882
883Lemma symbols_add_globals_match:
884  forall (g1: genv A) (g2: genv B) (m: mem),
885  symbols g1 = symbols g2 →
886  forall (vars: list (ident * list init_data * V))
887         (tvars: list (ident * list init_data * W)),
888  list_forall2 (match_var_entry match_var) vars tvars →
889  symbols (fst (add_globals (g1, m) vars)) =
890  symbols (fst (add_globals (g2, m) tvars)).
891Proof.
892  induction 2; simpl.
893  auto.
894  destruct a1 as [[id1 init1] info1].
895  destruct b1 as [[id2 init2] info2].
896  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
897  generalize IHlist_forall2.
898  generalize (mem_add_globals_match g1 g2 m H1).
899  destruct (add_globals (g1, m) al).
900  destruct (add_globals (g2, m) bl).
901  simpl. intros. congruence.
902Qed.
903
904Theorem find_funct_ptr_match:
905  forall (b: block) (f: A),
906  find_funct_ptr ? (globalenv p) b = Some ? f →
907  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
908Proof.
909  intros until f. destruct match_prog as [X [Y Z]].
910  destruct (add_functs_match X) as [P [Q R]].
911  unfold find_funct_ptr. repeat rewrite functions_globalenv.
912  auto.
913Qed.
914
915Theorem find_funct_ptr_rev_match:
916  forall (b: block) (tf: B),
917  find_funct_ptr ? (globalenv p') b = Some ? tf →
918  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
919Proof.
920  intros until tf. destruct match_prog as [X [Y Z]].
921  destruct (add_functs_rev_match X) as [P [Q R]].
922  unfold find_funct_ptr. repeat rewrite functions_globalenv.
923  auto.
924Qed.
925
926Theorem find_funct_match:
927  forall (v: val) (f: A),
928  find_funct (globalenv p) v = Some ? f →
929  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
930Proof.
931  intros until f. unfold find_funct.
932  case v; try (intros; discriminate).
933  intros b ofs.
934  case (Int.eq ofs Int.zero); try (intros; discriminate).
935  apply find_funct_ptr_match.
936Qed.
937
938Theorem find_funct_rev_match:
939  forall (v: val) (tf: B),
940  find_funct (globalenv p') v = Some ? tf →
941  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
942Proof.
943  intros until tf. unfold find_funct.
944  case v; try (intros; discriminate).
945  intros b ofs.
946  case (Int.eq ofs Int.zero); try (intros; discriminate).
947  apply find_funct_ptr_rev_match.
948Qed.
949
950Lemma symbols_init_match:
951  symbols (globalenv p') = symbols (globalenv p).
952Proof.
953  unfold globalenv. unfold globalenv_initmem.
954  destruct match_prog as [X [Y Z]].
955  destruct (add_functs_match X) as [P [Q R]].
956  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
957Qed.
958
959Theorem find_symbol_match:
960  forall (s: ident),
961  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
962Proof.
963  intros. unfold find_symbol.
964  rewrite symbols_init_match. auto.
965Qed.
966
967Theorem init_mem_match:
968  init_mem p' = init_mem p.
969Proof.
970  unfold init_mem. unfold globalenv_initmem.
971  destruct match_prog as [X [Y Z]].
972  symmetry. apply mem_add_globals_match. auto.
973Qed.
974
975End MATCH_PROGRAM.
976
977Section TRANSF_PROGRAM_PARTIAL2.
978
979Variable A B V W: Type.
980Variable transf_fun: A → res B.
981Variable transf_var: V → res W.
982Variable p: program A V.
983Variable p': program B W.
984Hypothesis transf_OK:
985  transform_partial_program2 transf_fun transf_var p = OK ? p'.
986
987Remark prog_match:
988  match_program
989    (fun fd tfd => transf_fun fd = OK ? tfd)
990    (fun info tinfo => transf_var info = OK ? tinfo)
991    p p'.
992Proof.
993  apply transform_partial_program2_match; auto.
994Qed.
995
996Theorem find_funct_ptr_transf_partial2:
997  forall (b: block) (f: A),
998  find_funct_ptr ? (globalenv p) b = Some ? f →
999  ∃f'.
1000  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1001Proof.
1002  intros.
1003  exploit find_funct_ptr_match. eexact prog_match. eauto.
1004  intros [tf [X Y]]. exists tf; auto.
1005Qed.
1006
1007Theorem find_funct_ptr_rev_transf_partial2:
1008  forall (b: block) (tf: B),
1009  find_funct_ptr ? (globalenv p') b = Some ? tf →
1010  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1011Proof.
1012  intros.
1013  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1014Qed.
1015
1016Theorem find_funct_transf_partial2:
1017  forall (v: val) (f: A),
1018  find_funct (globalenv p) v = Some ? f →
1019  ∃f'.
1020  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1021Proof.
1022  intros.
1023  exploit find_funct_match. eexact prog_match. eauto.
1024  intros [tf [X Y]]. exists tf; auto.
1025Qed.
1026
1027Theorem find_funct_rev_transf_partial2:
1028  forall (v: val) (tf: B),
1029  find_funct (globalenv p') v = Some ? tf →
1030  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1031Proof.
1032  intros.
1033  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1034Qed.
1035
1036Theorem find_symbol_transf_partial2:
1037  forall (s: ident),
1038  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1039Proof.
1040  intros. eapply find_symbol_match. eexact prog_match.
1041Qed.
1042
1043Theorem init_mem_transf_partial2:
1044  init_mem p' = init_mem p.
1045Proof.
1046  intros. eapply init_mem_match. eexact prog_match.
1047Qed.
1048
1049End TRANSF_PROGRAM_PARTIAL2.
1050
1051Section TRANSF_PROGRAM_PARTIAL.
1052
1053Variable A B V: Type.
1054Variable transf: A → res B.
1055Variable p: program A V.
1056Variable p': program B V.
1057Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1058
1059Remark transf2_OK:
1060  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1061Proof.
1062  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1063  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1064  rewrite map_partial_identity; auto.
1065Qed.
1066
1067Theorem find_funct_ptr_transf_partial:
1068  forall (b: block) (f: A),
1069  find_funct_ptr ? (globalenv p) b = Some ? f →
1070  ∃f'.
1071  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1072Proof.
1073  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1074Qed.
1075
1076Theorem find_funct_ptr_rev_transf_partial:
1077  forall (b: block) (tf: B),
1078  find_funct_ptr ? (globalenv p') b = Some ? tf →
1079  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1080Proof.
1081  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1082Qed.
1083
1084Theorem find_funct_transf_partial:
1085  forall (v: val) (f: A),
1086  find_funct (globalenv p) v = Some ? f →
1087  ∃f'.
1088  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1089Proof.
1090  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1091Qed.
1092
1093Theorem find_funct_rev_transf_partial:
1094  forall (v: val) (tf: B),
1095  find_funct (globalenv p') v = Some ? tf →
1096  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1097Proof.
1098  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1099Qed.
1100
1101Theorem find_symbol_transf_partial:
1102  forall (s: ident),
1103  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1104Proof.
1105  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1106Qed.
1107
1108Theorem init_mem_transf_partial:
1109  init_mem p' = init_mem p.
1110Proof.
1111  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1112Qed.
1113
1114End TRANSF_PROGRAM_PARTIAL.
1115
1116Section TRANSF_PROGRAM.
1117
1118Variable A B V: Type.
1119Variable transf: A → B.
1120Variable p: program A V.
1121Let tp := transform_program transf p.
1122
1123Remark transf_OK:
1124  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1125Proof.
1126  unfold tp, transform_program, transform_partial_program.
1127  rewrite map_partial_total. reflexivity.
1128Qed.
1129
1130Theorem find_funct_ptr_transf:
1131  forall (b: block) (f: A),
1132  find_funct_ptr ? (globalenv p) b = Some ? f →
1133  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1134Proof.
1135  intros.
1136  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1137  as [f' [X Y]]. congruence.
1138Qed.
1139
1140Theorem find_funct_ptr_rev_transf:
1141  forall (b: block) (tf: B),
1142  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1143  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1144Proof.
1145  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1146  intros [f [X Y]]. exists f; split. auto. congruence.
1147Qed.
1148
1149Theorem find_funct_transf:
1150  forall (v: val) (f: A),
1151  find_funct (globalenv p) v = Some ? f →
1152  find_funct (globalenv tp) v = Some ? (transf f).
1153Proof.
1154  intros.
1155  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1156  as [f' [X Y]]. congruence.
1157Qed.
1158
1159Theorem find_funct_rev_transf:
1160  forall (v: val) (tf: B),
1161  find_funct (globalenv tp) v = Some ? tf →
1162  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1163Proof.
1164  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1165  intros [f [X Y]]. exists f; split. auto. congruence.
1166Qed.
1167
1168Theorem find_symbol_transf:
1169  forall (s: ident),
1170  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1171Proof.
1172  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1173Qed.
1174
1175Theorem init_mem_transf:
1176  init_mem tp = init_mem p.
1177Proof.
1178  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1179Qed.
1180
1181End TRANSF_PROGRAM.
1182
1183End Genv.
1184*)
Note: See TracBrowser for help on using the repository browser.