source: src/common/Globalenvs.ma @ 2439

Last change on this file since 2439 was 2439, checked in by campbell, 7 years ago

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File size: 74.0 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 "common/Errors.ma".
37include "common/AST.ma".
38(*include "Values.ma".*)
39include "common/FrontEndMem.ma".
40
41   (* * The type of global environments.  The parameter [F] is the type
42       of function descriptions. *)
43(* Functions are given negative block numbers *)
44record genv_t (F:Type[0]) : Type[0] ≝ {
45  functions: positive_map F;
46  nextfunction: Pos;
47  symbols: identifier_map SymbolTag block;
48  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
49                 ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
50}.
51
52(* We deal with shadowed names by overwriting their global environment entry
53   and getting rid of any function mapping (the latter is necessary so that we
54   get a reverse mapping).  In fact, the parser will prevent these anyway, but
55   adding the uniqueness of these names throughout would be more trouble than
56   it's worth. *)
57   
58definition drop_fn : ∀F:Type[0]. ident → genv_t F → genv_t F ≝
59λF,id,g.
60let fns ≝
61  match lookup ?? (symbols … g) id with
62  [ None ⇒ functions … g
63  | Some b' ⇒
64      match b' with
65      [ mk_block r x ⇒
66        match r with
67        [ Code ⇒
68          match x with
69          [ neg p ⇒ pm_set … p (None ?) (functions … g)
70          | _ ⇒ functions … g
71          ]
72        | _ ⇒ functions … g
73        ]
74      | _ ⇒ functions … g
75      ]
76  ]
77in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
78whd in match fns; -fns
79#b #L
80cases (functions_inv ? g b ?)
81[ #id' #L'
82  cases (identifier_eq … id id')
83  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
84  | #NE %{id'} >lookup_remove_miss /2/
85  ]
86| cases (lookup ?? (symbols F g) id) in L;
87  [ normalize //
88  | * * * [ 2,3,5,6: #b' ] normalize //
89    #H cut (b ≠ b')
90    [ % #E destruct >lookup_opt_pm_set_hit in H; * /2/ ]
91    #NE >lookup_opt_pm_set_miss in H; //
92  ]
93] qed.
94
95lemma drop_fn_id : ∀F,id,ge.
96  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
97#F #id * #fns #next #syms #inv
98whd in match (drop_fn ???);
99@lookup_remove_hit
100qed.
101
102lemma drop_fn_lfn : ∀F,id,ge,b,f.
103  lookup_opt ? b (functions … (drop_fn F id ge)) = Some ? f →
104  lookup_opt ? b (functions … ge) = Some ? f.
105#F #id #ge #b #f
106whd in match (drop_fn ???);
107cases (lookup ??? id)
108[ normalize //
109| * * * [2,3,5,6: #b' ] normalize //
110  cases (decidable_eq_pos b b')
111  [ #E destruct >lookup_opt_pm_set_hit #E destruct
112  | #NE >lookup_opt_pm_set_miss //
113  ]
114] qed.
115
116definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝
117λF,name_fun,g.
118  let blk_id ≝ nextfunction ? g in
119  let b ≝ mk_block Code (neg blk_id) in
120  let g' ≝ drop_fn F (\fst name_fun) g in
121  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
122              (succ blk_id)
123              (add ?? (symbols … g') (\fst name_fun) b) ?.
124#b' #L whd in match b;
125cases (decidable_eq_pos blk_id b')
126[ #E destruct
127  %{(\fst name_fun)} @lookup_add_hit
128| #NE
129  cases (functions_inv ? g' b' ?)
130  [ #id #L' %{id} >lookup_add_miss
131    [ @L'
132    | % #E destruct
133      >drop_fn_id in L'; #E destruct
134    ]
135  | >lookup_opt_insert_miss in L; /2/
136  ]
137] qed.
138
139definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
140λF,name,b,g.
141  let g' ≝ drop_fn F name g in
142  mk_genv_t F (functions … g')
143              (nextfunction … g')
144              (add ?? (symbols … g') name b)
145              ?.
146#b' #L
147cases (functions_inv ? g' b' ?)
148[ #id #L' %{id} >lookup_add_miss
149  [ @L'
150  | % #E destruct
151    >drop_fn_id in L'; #E destruct
152  ]
153| @L
154] qed.
155
156(* Construct environment and initial memory store *)
157definition empty_mem ≝ empty. (* XXX*)
158definition empty : ∀F. genv_t F ≝
159  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??) ?.
160#b #L normalize in L; cases L #L cases (L (refl ??))
161qed.
162
163definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
164λF,init,fns.
165  foldr ?? (add_funct F) init fns.
166
167(* Return the address of the given global symbol, if any. *)
168definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
169λF,ge. lookup ?? (symbols … ge).
170
171(* init *)
172
173definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝
174λF,ge,m,b,p,id.
175  (* store checks that the address came from something capable of representing
176     addresses of the memory region in question - here there are no real
177     pointers, so use the real region. *)
178  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
179  match id with
180  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
181  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
182  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
183  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
184  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
185  | Init_addrof (*r'*) symb ofs ⇒
186      match find_symbol … ge symb with
187      [ None ⇒ None ?
188      | Some b' ⇒ (*
189        match pointer_compat_dec b' r' with
190        [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs))))
191        (*| inr _ ⇒ None ?
192        ]*)
193      ]
194  | Init_space n ⇒ Some ? m
195  | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*))
196  ].
197(*cases b //
198qed.*)
199
200definition size_init_data : init_data → nat ≝
201 λi_data.match i_data with
202  [ Init_int8 _ ⇒ 1
203  | Init_int16 _ ⇒ 2
204  | Init_int32 _ ⇒ 4
205  | Init_float32 _ ⇒ 4
206  | Init_float64 _ ⇒ 8
207  | Init_space n ⇒ max n 0
208  | Init_null (*r*) ⇒ size_pointer (*r*)
209  | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)].
210
211let rec store_init_data_list (F:Type[0]) (ge:genv_t F)
212                              (m: mem) (b: block) (p: Z) (idl: list init_data)
213                              on idl : option mem ≝
214  match idl with
215  [ nil ⇒ Some ? m
216  | cons id idl' ⇒
217      match store_init_data F ge m b p id with
218      [ None ⇒ None ?
219      | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'
220      ]
221  ].
222
223definition size_init_data_list : list init_data → nat ≝
224  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.
225
226(* Nonessential properties that may require arithmetic
227nremark size_init_data_list_pos:
228  ∀i_data. OZ ≤ size_init_data_list i_data.
229#i_data;elim i_data;//;
230#a;#tl;cut (OZ ≤ size_init_data a)
231##[cases a;normalize;//;
232   #x;cases x;normalize;//;
233##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
234   cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
235   ##[cases (size_init_data a) in Hsize IH;
236      ##[##1,2:/3/
237      ##|normalize;#n;#Hfalse;elim Hfalse]
238   ##|#Hdisc;cases Hdisc
239      ##[#Heq;nrewrite > Heq;//;
240      ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2;
241         (* TODO: arithmetics *) napply daemon]
242   ##]
243##]
244qed.
245*)
246
247
248(* init *)
249
250axiom InitDataStoreFailed : String.
251
252definition add_globals : ∀F,V:Type[0].
253       (V → (list init_data)) →
254       genv_t F × mem → list (ident × region × V) →
255       (genv_t F × mem) ≝
256λF,V,extract_init,init_env,vars.
257  foldl ??
258    (λg_st: genv_t F × mem. λid_init: ident × region × V.
259      let 〈id, r, init_info〉 ≝ id_init in
260      let init ≝ extract_init init_info in
261      let 〈g,st〉 ≝ g_st in
262        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
263          let g' ≝ add_symbol ? id b g in
264            〈g', st'〉
265        )
266    init_env vars.
267
268definition init_globals : ∀F,V:Type[0].
269       (V → (list init_data)) →
270       genv_t F → mem → list (ident × region × V) →
271       res mem ≝
272λF,V,extract_init,g,m,vars.
273  foldl ??
274    (λst: res mem. λid_init: ident × region × V.
275      let 〈id, r, init_info〉 ≝ id_init in
276      let init ≝ extract_init init_info in
277        do st ← st;
278        match find_symbol … g id with
279        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
280        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
281        ] )
282    (OK ? m) vars.
283
284definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝
285λF,V,init_info,p.
286  add_globals … init_info
287   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
288   (prog_vars ?? p).
289
290(* Return the global environment for the given program. *)
291definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝
292λF,V,i,p.
293  \fst (globalenv_allocmem F V i p).
294
295(* Return the global environment for the given program with no data initialisation. *)
296definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
297λF,p.
298  globalenv F nat (λn.[Init_space n]) p.
299
300(* Return the initial memory state for the given program. *)
301definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝
302λF,V,i,p.
303  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
304  init_globals ? V i g m (prog_vars ?? p).
305
306(* Setup memory when data initialisation is not required (has the benefit
307   of being total. *)
308definition alloc_mem: ∀F. program F nat → mem ≝
309λF,p.
310  \snd (globalenv_allocmem F nat (λn. [Init_space n]) p).
311
312(* Return the function description associated with the given address, if any. *)
313definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝
314λF,ge,b. match block_region b with [ Code ⇒
315           match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge)
316         | _ ⇒ None ? ] | _ ⇒ None ? ].
317
318(* Same as [find_funct_ptr] but the function address is given as
319   a value, which must be a pointer with offset 0. *)
320definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝
321λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then find_funct_ptr … ge (pblock ptr) else None ? | _ ⇒ None ? ].
322
323
324(* Turn a memory block into the original symbol. *)
325definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
326λF,genv,b.
327  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).
328
329
330lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
331  find_funct F ge v = Some F f →
332  ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
333#F #ge *
334[ #f #E normalize in E; destruct
335| #sz #i #f #E normalize in E; destruct
336| #f #fn #E normalize in E; destruct
337| (*#r*) #f #E normalize in E; destruct
338| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
339  @eq_offset_elim #Eoff
340  #E whd in E:(??%?); destruct
341  (*%{pty}*) %{b} (*%{c}*) % // @E
342] qed.
343 
344lemma add_globals_match : ∀A,B,V,W,initV,initW.
345  ∀P:(ident × region × V) → (ident × region × W) → Prop.
346  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
347  ∀vars,ge,ge',m,vars'.
348  symbols ? ge = symbols … ge' →
349  All2 … P vars vars' →
350  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧ 
351  \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars').
352#A #B #V #W #initV #initW #P #varsOK
353#vars elim vars
354[ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ]
355| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
356  * * #id' #r' #w #tl' #E * #p #TL
357  whd in match (add_globals A ????);
358  change with (add_globals A ????) in match (foldl ?????);
359  whd in match (add_globals B ????);
360  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
361  cases (varsOK … p) #E1 #E2
362  destruct >E2 cases (alloc ????) #m' #b
363  @IH /2/
364  whd in match (add_symbol ????); whd in match (drop_fn ???);
365  whd in match (add_symbol ????); whd in match (drop_fn ???);
366  >E %
367] qed.
368
369
370lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
371  (∀f,g. P f g → \fst f = \fst g) →
372  ∀fns,fns'.
373  All2 … P fns fns' →
374  let ge ≝ add_functs A (empty ?) fns in
375  let ge' ≝ add_functs B (empty ?) fns' in
376  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
377#A #B #P #fnOK #fns elim fns
378[ * [ #_ % % | #h #t * ]
379| * #id #f #tl #IH * [ * ]
380  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
381  whd in match (add_functs ???);
382  change with (add_functs ???) in match (foldr ?????);
383  whd in match (add_functs B ??);
384  change with (add_functs ???) in match (foldr (ident × B) ????);
385  cases (IH tl' H) #E1 #E2
386  % [ >E1 %
387    | whd in match (drop_fn ???);
388      whd in match (drop_fn ???);
389      >E1 >E2 % ]
390] qed.
391
392lemma matching_fns_get_same_blocks :  ∀A,B,P.
393  (∀f,g. P f g → \fst f = \fst g) →
394  ∀fns,fns'.
395  All2 … P fns fns' →
396  let ge ≝ add_functs A (empty ?) fns in
397  let ge' ≝ add_functs B (empty ?) fns' in
398  symbols … ge = symbols … ge'.
399#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
400qed.
401
402lemma symbol_of_block_rev : ∀F,genv,b,id.
403  symbol_for_block F genv b = Some ? id →
404  find_symbol F genv id = Some ? b.
405#F #genv #b #id #H whd in H:(??%?);
406@(find_lookup … (λid,b'. eq_block b b'))
407lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
408cases (find ????) in H ⊢ %;
409[ normalize #E destruct
410| * #id' #b' normalize in ⊢ (% → ?); #E destruct
411  #H lapply (H … (refl ??))
412  @eq_block_elim
413  [ #E destruct //
414  | #_ *
415  ]
416] qed.
417
418(* The mapping of blocks to symbols is total for functions. *)
419
420definition symbol_of_function_block : ∀F,ge,b. find_funct_ptr F ge b ≠ None ? → ident ≝
421λF,ge,b,FFP.
422match symbol_for_block F ge b return λx. symbol_for_block ??? = x → ? with
423[ None ⇒ λH. ⊥
424| Some id ⇒ λ_. id
425] (refl ? (symbol_for_block F ge b)).
426whd in H:(??%?);
427cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
428cases (functions_inv … ge b FFP)
429#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
430lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
431cases (find ????)
432[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
433| * #id' #b' #_ normalize #_ #E destruct
434] qed.
435
436
437(*
438(* * ** Properties of the operations. *)
439
440  find_funct_inv:
441    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
442    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
443  find_funct_find_funct_ptr:
444    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
445    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
446
447  find_symbol_exists:
448    ∀F,V: Type[0]. ∀p: program F V.
449           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
450    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
451    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
452  find_funct_ptr_exists:
453    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
454    list_norepet ? (prog_funct_names ?? p) →
455    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
456    in_list ? 〈id, f〉 (prog_funct ?? p) →
457    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
458           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
459
460  find_funct_ptr_inversion:
461    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
462    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
463    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
464  find_funct_inversion:
465    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
466    find_funct ? (globalenv ?? p) v = Some ? f →
467    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
468  find_funct_ptr_symbol_inversion:
469    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
470    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
471    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
472    in_list ? 〈id, f〉 (prog_funct ?? p);
473
474  find_funct_ptr_prop:
475    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
476    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
477    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
478    P f;
479  find_funct_prop:
480    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
481    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
482    find_funct ? (globalenv ?? p) v = Some ? f →
483    P f;
484
485  initmem_nullptr:
486    ∀F,V: Type[0]. ∀p: program F V.
487    let m ≝ init_mem ?? p in
488    valid_block m nullptr ∧
489    (blocks m) nullptr = empty_block 0 0 Any;
490(*  initmem_inject_neutral:
491    ∀F,V: Type[0]. ∀p: program F V.
492    mem_inject_neutral (init_mem ?? p);*)
493  find_funct_ptr_negative:
494    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
495    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
496  find_symbol_not_fresh:
497    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
498    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
499  find_symbol_not_nullptr:
500    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
501    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
502  global_addresses_distinct:
503    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
504    id1≠id2 →
505    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
506    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
507    b1≠b2;
508
509(* * Commutation properties between program transformations
510  and operations over global environments. *)
511
512  find_funct_ptr_rev_transf:
513    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
514    ∀b : block. ∀tf : B.
515    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
516    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
517  find_funct_rev_transf:
518    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
519    ∀v : val. ∀tf : B.
520    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
521    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
522
523(* * Commutation properties between partial program transformations
524  and operations over global environments. *)
525
526  find_funct_ptr_transf_partial:
527    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
528    transform_partial_program … transf p = OK ? p' →
529    ∀b: block. ∀f: A.
530    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
531    ∃f'.
532    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
533  find_funct_transf_partial:
534    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
535    transform_partial_program … transf p = OK ? p' →
536    ∀v: val. ∀f: A.
537    find_funct ? (globalenv ?? p) v = Some ? f →
538    ∃f'.
539    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
540  find_symbol_transf_partial:
541    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
542    transform_partial_program … transf p = OK ? p' →
543    ∀s: ident.
544    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
545  init_mem_transf_partial:
546    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
547    transform_partial_program … transf p = OK ? p' →
548    init_mem ?? p' = init_mem ?? p;
549  find_funct_ptr_rev_transf_partial:
550    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
551    transform_partial_program … transf p = OK ? p' →
552    ∀b : block. ∀tf : B.
553    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
554    ∃f : A.
555      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
556  find_funct_rev_transf_partial:
557    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
558    transform_partial_program … transf p = OK ? p' →
559    ∀v : val. ∀tf : B.
560    find_funct ? (globalenv ?? p') v = Some ? tf →
561    ∃f : A.
562      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;
563
564  find_funct_ptr_transf_partial2:
565    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
566           ∀p: program A V. ∀p': program B W.
567    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
568    ∀b: block. ∀f: A.
569    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
570    ∃f'.
571    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
572  find_funct_transf_partial2:
573    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
574           ∀p: program A V. ∀p': program B W.
575    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
576    ∀v: val. ∀f: A.
577    find_funct ? (globalenv ?? p) v = Some ? f →
578    ∃f'.
579    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
580  find_symbol_transf_partial2:
581    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
582           ∀p: program A V. ∀p': program B W.
583    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
584    ∀s: ident.
585    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
586  init_mem_transf_partial2:
587    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
588           ∀p: program A V. ∀p': program B W.
589    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
590    init_mem ?? p' = init_mem ?? p;
591  find_funct_ptr_rev_transf_partial2:
592    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
593           ∀p: program A V. ∀p': program B W.
594    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
595    ∀b: block. ∀tf: B.
596    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
597    ∃f : A.
598      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
599  find_funct_rev_transf_partial2:
600    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
601           ∀p: program A V. ∀p': program B W.
602    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
603    ∀v: val. ∀tf: B.
604    find_funct ? (globalenv ?? p') v = Some ? tf →
605    ∃f : A.
606      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;
607
608(* * Commutation properties between matching between programs
609  and operations over global environments. *)
610*) *)
611
612(* First, show that nextfunction only depends on the number of functions: *)
613
614let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
615match n with
616[ O ⇒ p
617| S m ⇒ succ (nat_plus_pos m p)
618].
619
620lemma nextfunction_length : ∀A,l,ge.
621  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
622#A #l elim l // #h #t #IH #ge
623whd in ⊢ (??%%); >IH //
624qed.
625
626lemma alloc_pair : ∀m,m',l,h,l',h',r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].
627  nextblock m = nextblock m' →
628  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
629  P (alloc m l h r) (alloc m' l' h' r).
630* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H %
631qed.
632
633lemma vars_irrelevant_to_find_funct_ptr :
634  ∀F,G,V,W.
635  ∀P:F → G → Prop.
636  ∀init,init',b,vars,vars',ge,ge',m,m',f.
637  (find_funct_ptr F ge b = Some ? f → ∃f'. find_funct_ptr G ge' b = Some ? f' ∧ P f f') →
638  symbols F ge = symbols G ge' →
639  nextblock m = nextblock m' →
640  All2 … (λx,y. \fst x = \fst y) vars vars' →
641  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f →
642  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
643#F #G #V #W #P #init #init'
644* * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]
645#vars elim vars
646[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
647    | #x #tl #ge #ge' #m #m' #f #_ #_ #_ *
648    ]
649| * * #id #r #v #tl #IH *
650  [ #ge #ge' #m #m' #f #_ #_ #_ *
651  | * * #id' #r' #v' #tl'
652    #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH
653    whd in match (add_globals ?????); whd in match (add_globals G ????);
654    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
655    @(alloc_pair … Enext) #m1 #m2 #b #Enext'
656    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
657    #FFP
658    @(IH … MATCH FFP)
659    [ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
660      whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?));
661      >Esym
662      cases (lookup … id')
663      [ @FFP1
664      | * * * try @FFP1 #p try @FFP1
665        normalize
666        cases (decidable_eq_pos blk p)
667        [ #E destruct >lookup_opt_pm_set_hit #E destruct
668        | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE)
669          @FFP1
670        ]
671      ]
672    | whd in match (add_symbol ????); whd in match (drop_fn ???);
673      whd in match (add_symbol ????); whd in match (drop_fn ???);
674      >Esym %
675    | assumption
676    ]
677  ]
678] qed.
679
680(* Now link functions in related programs, but without dealing with the type
681   casts yet. *)
682
683lemma symbols_drop_fn_eq : ∀A,B,ge,ge',id.
684  symbols A ge = symbols B ge' →
685  symbols A (drop_fn A id ge) = symbols B (drop_fn B id ge').
686#A #B #ge #ge' #id #E
687whd in ⊢ (??(??%)(??%));
688>E %
689qed.
690
691lemma ge_add_functs : ∀A,B,fns,fns'.
692  All2 ?? (λx,y. \fst x = \fst y) fns fns' →
693  symbols A (add_functs A (empty ?) fns) = symbols B (add_functs B (empty ?) fns') ∧
694  nextfunction A (add_functs A (empty ?) fns) = nextfunction B (add_functs B (empty ?) fns').
695#A #B
696#fns elim fns
697[ * [ #_ % % | #h #t * ]
698| * #id #a #tl #IH * * #id' #b #tl' * #E destruct #TL
699  whd in match (add_functs ???); whd in match (add_functs B ??);
700  cases (IH ? TL) #S #N >N % [2: % ]
701  >(symbols_drop_fn_eq A B (foldr ??? (empty A) tl) (foldr ?? (add_funct B) (empty B) tl'))
702  [ %
703  | @S
704  ]
705] qed.
706
707lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
708  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
709  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
710#F #ge #id #b #f
711whd in match (drop_fn F id ge);
712cases (lookup … id)
713[ #_ % #E destruct
714| * * * [2,3,5,6: #b'] normalize
715  [4: cases (decidable_eq_pos b b')
716    [ #E destruct >lookup_opt_pm_set_hit #E destruct
717    | #NE #_ @(not_to_not … NE) #E destruct //
718    ]
719  | *: #_ % #E destruct
720  ]
721] qed.
722
723lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
724  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
725  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
726#F #ge #id #b
727whd in match (drop_fn F id ge);
728cases (lookup … id)
729[ //
730| * * * //
731  #b' normalize #NE
732  @lookup_opt_pm_set_miss
733  @(not_to_not … NE)
734  #E destruct %
735] qed.
736
737lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
738  All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
739  All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') →
740  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
741  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
742#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
743#Mfns
744cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
745[ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
746whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
747whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
748@vars_irrelevant_to_find_funct_ptr
749[ letin varnames ≝ (map ??? vars)
750  generalize in match fns' in Mfns ⊢ %;
751  elim fns
752  [ #fns' #Mfns whd in ⊢ (??%? → ?); #E destruct
753  | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl
754    whd in ⊢ (??%? → ?);
755    whd in match (functions ??);
756    change with (add_functs ???) in match (foldr ?????);
757    cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … Mtl) * #idA #a * #idB #b * // ]
758    #SYMS #NEXT
759    cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl)))
760    [ #E destruct >lookup_opt_insert_hit #E destruct
761      %{fn'} % // whd in ⊢ (??%?);
762      whd in match (functions ??);
763      change with (add_functs ???) in match (foldr ???? tl');
764      >NEXT >lookup_opt_insert_hit @refl
765    | #NE >lookup_opt_insert_miss //
766      #FFP cases (IH tl' Mtl ?)
767      [ #fn'' * #FFP' #P' %{fn''} %
768        [ whd in ⊢ (??%?);
769          >lookup_opt_insert_miss [2: <NEXT // ]
770          lapply (lookup_drop_fn_different ????? FFP)
771          >SYMS
772          #L >lookup_drop_fn_irrelevant // @FFP'
773        | @P'
774        ]
775      | @(drop_fn_lfn … FFP)
776      ]
777    ]
778  ]
779| cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ]
780  #S #_ @S
781| @refl
782] qed.
783
784(* lazy proof *)
785lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P.
786  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
787  All ? (λx. P (\snd x)) (prog_funct ?? p) →
788  P f.
789#A #V #b #p #f #initV #P #FFP #ALL
790cut (All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
791[ elim (prog_funct … p) in ALL ⊢ %;
792  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
793cut (All2 ?? (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p))
794[ elim (prog_vars … p) [ // | * #x #x' #tl #TL /2/ ] ]
795#VARS2 #FNS2
796cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FNS2 VARS2 FFP)
797#x * //
798qed.
799
800
801discriminator Prod.
802
803(* Now prove the full version. *)
804
805lemma find_funct_ptr_match:
806    ∀M:matching.∀initV,initW.
807    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
808    ∀MATCH:match_program … M p p'.
809    ∀b: block. ∀f: m_A M (prog_var_names … p).
810    find_funct_ptr … (globalenv … initV p) b = Some ? f →
811    ∃tf : m_B M (prog_var_names … p').
812    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
813[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
814* #A #B #V #W #match_fn #match_var #initV #initW
815#p #p' * #Mvars #Mfn #Mmain
816#b #f #FFP
817@(find_funct_ptr_All2 A B V W ????????? FFP)
818[ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
819  #E
820  @(All2_mp … Mfn)
821  * #id #f * #id' #f'
822  <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
823  normalize #H @(match_funct_entry_inv … H)
824  #vs #id1 #f1 #f2 #M % //
825| @(All2_mp … Mvars)
826  * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct //
827qed.
828
829lemma
830  find_funct_ptr_transf_partial2:
831    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
832           ∀p: program A V. ∀p': program B W.
833    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
834    ∀b: block. ∀f: A ?.
835    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
836    ∃f'.
837    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
838#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
839cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
840[2: @iW
841| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
842#TF %{f'} % //
843-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
844qed.
845
846lemma match_funct_entry_id : ∀M,vs,vs',f,g.
847  match_funct_entry M vs vs' f g → \fst f = \fst g.
848#M #vs #vs' #f #g * //
849qed.
850
851lemma
852  find_symbol_match:
853    ∀M:matching.
854    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
855    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
856    match_program … M p p' →
857    ∀s: ident.
858    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
859* #A #B #V #W #match_fun #match_var #initV #initW #initsize
860* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
861whd in ⊢ (??%%);
862@sym_eq
863@(eq_f ??(λx. lookup SymbolTag block x s))
864whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
865whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
866change with (add_globals ?????) in match (foldl ?????);
867change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
868@(proj1 … (add_globals_match … Mvars))
869[ @(matching_fns_get_same_blocks … Mfns)
870  #f #g @match_funct_entry_id
871| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
872] qed.
873 
874lemma
875  find_symbol_transf_partial2:
876    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
877    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
878           ∀p: program A V. ∀p': program B W.
879    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
880    ∀s: ident.
881    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
882#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
883@(find_symbol_match … (transform_partial_program2_match … TPP2))
884#v0 #w0 * #id #r #v #w @sizeOK
885qed.
886
887lemma
888  find_funct_ptr_transf:
889    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
890    ∀b: block. ∀f: A ?.
891    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
892    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
893#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
894cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
895[ 2: @iV
896| #f' * #FFP'
897  whd in ⊢ (???(match % with [_⇒?]) → ?);  (* XXX this line only required to workaround unification bug *)
898  generalize in match (matching_vars ????);
899  whd in match (prog_var_names ???); whd in match (prog_vars ???);
900  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
901] qed.
902
903lemma
904  find_funct_transf:
905    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
906    ∀v: val. ∀f: A ?.
907    find_funct ? (globalenv … iV p) v = Some ? f →
908    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
909#A #B #V #iV #tf #p #v #f #FF
910cases (find_funct_find_funct_ptr ???? FF)
911#b * #E destruct #FFP
912change with (find_funct_ptr ???) in ⊢ (??%?);
913@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
914qed.
915
916lemma
917  find_symbol_transf:
918    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
919    ∀s: ident.
920    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
921    find_symbol ? (globalenv … iV p) s.
922#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
923#v0 #w0 * //
924qed.
925
926lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
927  symbols A ge = symbols … ge' →
928  store_init_data A ge m b o d = store_init_data B ge' m b o d.
929#A #B #ge #ge' #m #b #o #d #SYM
930whd in ⊢ (??%%);
931cases d try #d' try @refl
932#n whd in ⊢ (??%%);
933whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
934qed.
935
936lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
937  symbols A ge = symbols … ge' →
938  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
939#A #B #ge #ge' #b #SYM #d elim d
940[ //
941| #hd #tl #IH #m #o
942  whd in ⊢ (??%%);
943  >(store_init_data_symbols … SYM)
944  cases (store_init_data ??????)
945  [ %
946  | #m' @IH
947  ]
948] qed.
949
950lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
951  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
952  ∀ge:genv_t A. ∀ge':genv_t B.
953  symbols … ge = symbols … ge' →
954   ∀m. ∀vars,vars'.
955  All2 … P vars vars' →
956  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
957#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
958whd in ⊢ (? → ? → ??%%);
959generalize in match (OK ? m);
960elim vars
961[ #rm *
962  [ #_ %
963  | #h #t *
964  ]
965| * #idr #v #tl #IH #rm
966  * [ * ]
967  * #idr' #w #tl'
968  * #p cases (varsOK … p) #E1 #E2 destruct #TL
969  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
970  whd in ⊢ (??(????%?)(????%?));
971  [ whd in match (find_symbol ?? id);
972    whd in match (find_symbol B ? id);
973    >SYM cases (lookup ??? id)
974    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
975  ] @IH //
976] qed.
977
978lemma
979  init_mem_match:
980    ∀M:matching.
981    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
982    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
983    match_program … M p p' →
984    init_mem … iW p' = init_mem … iV p.
985* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
986whd in ⊢ (??%%);
987change with (add_globals ?????) in match (globalenv_allocmem ??? p');
988change with (add_globals ?????) in match (globalenv_allocmem ??? p);
989cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
990[ 8: @(matching_fns_get_same_blocks … Mfns)
991     #f0 #g0 * //
992| cases (add_globals ?????) #ge1 #m1
993  cases (add_globals ?????) #ge2 #m2
994  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
995  [ #v0 #w0 * #id #r #v #w /3/
996  | @SYM
997  ]
998| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
999| *: skip
1000] qed.
1001
1002lemma
1003  init_mem_transf:
1004    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
1005    init_mem … iV (transform_program … p transf) = init_mem … iV p.
1006#A #B #C #iV #transf #p
1007@(init_mem_match … (transform_program_match … transf ?))
1008//
1009qed.
1010
1011lemma
1012  init_mem_transf_gen:
1013    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
1014    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
1015#tag #A #B #C #iV #g #transf #p
1016@(init_mem_match … (transform_program_gen_match … transf ?))
1017//
1018qed.
1019   
1020
1021(* Package up transform_program results for global envs nicely. *)
1022
1023record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
1024  rg_find_symbol: ∀s.
1025    find_symbol … ge s = find_symbol … ge' s;
1026  rg_find_funct: ∀v,f.
1027    find_funct … ge v = Some ? f →
1028    find_funct … ge' v = Some ? (t f);
1029  rg_find_funct_ptr: ∀b,f.
1030    find_funct_ptr … ge b = Some ? f →
1031    find_funct_ptr … ge' b = Some ? (t f)
1032}.
1033
1034theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
1035  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
1036#A #B #V #iV #p #tf %
1037[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
1038| @(find_funct_transf A B V iV tf p)
1039| @(find_funct_ptr_transf A B V iV p tf)
1040] qed.
1041
1042record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
1043  rgg_find_symbol: ∀s.
1044    find_symbol … ge s = find_symbol … ge' s;
1045  rgg_find_funct_ptr: ∀b,f.
1046    find_funct_ptr … ge b = Some ? f →
1047    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
1048  rgg_find_funct: ∀v,f.
1049    find_funct … ge v = Some ? f →
1050    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
1051}.
1052
1053include "utilities/bool.ma".
1054
1055theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
1056  related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))).
1057#tag #A #B #V #iV #g #p #tf %
1058[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
1059  #v #w * //
1060| #b #f #FFP
1061  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
1062  [ 2: @iV
1063  | #fn' * #FFP'
1064    generalize in match (matching_vars ????);
1065    whd in match (prog_var_names ???); whd in match (prog_vars ???);
1066    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
1067  | skip
1068  ]
1069| * [5: #ptr #fn whd in match (find_funct ???);
1070     @if_elim #Eoff #FFP
1071     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
1072       [ 2: @iV
1073       | #fn' * #FFP'
1074         generalize in match (matching_vars ????);
1075         whd in match (prog_var_names ???); whd in match (prog_vars ???);
1076         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
1077         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
1078       ]
1079     | destruct
1080     ]
1081    | *: normalize #A #B try #C try #D destruct
1082    ]
1083] qed.
1084
1085
1086(*
1087
1088  find_funct_ptr_match:
1089    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
1090           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
1091    match_program … match_fun match_var p p' →
1092    ∀b: block. ∀f: A.
1093    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
1094    ∃tf : B.
1095    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
1096  find_funct_ptr_rev_match:
1097    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
1098           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
1099    match_program … match_fun match_var p p' →
1100    ∀b: block. ∀tf: B.
1101    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
1102    ∃f : A.
1103    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
1104  find_funct_match:
1105    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
1106           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
1107    match_program … match_fun match_var p p' →
1108    ∀v: val. ∀f: A.
1109    find_funct ? (globalenv ?? p) v = Some ? f →
1110    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
1111  find_funct_rev_match:
1112    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
1113           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
1114    match_program … match_fun match_var p p' →
1115    ∀v: val. ∀tf: B.
1116    find_funct ? (globalenv ?? p') v = Some ? tf →
1117    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
1118  find_symbol_match:
1119    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
1120           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
1121    match_program … match_fun match_var p p' →
1122    ∀s: ident.
1123    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
1124*)
1125(*
1126Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
1127  ZMap.get b g.(functions).
1128
1129Definition find_funct (g: genv) (v: val) : option F :=
1130  match v with
1131  | Vptr b ofs =>
1132      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
1133  | _ =>
1134      None
1135  end.
1136
1137Definition find_symbol ? (g: genv) (symb: ident) : option block :=
1138  PTree.get symb g.(symbols).
1139
1140Lemma find_funct_inv:
1141  forall (ge: t) (v: val) (f: F),
1142  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
1143Proof.
1144  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
1145  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
1146  exists b. congruence.
1147  discriminate.
1148Qed.
1149
1150Lemma find_funct_find_funct_ptr:
1151  forall (ge: t) (b: block),
1152  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
1153Proof.
1154  intros. simpl.
1155  generalize (Int.eq_spec Int.zero Int.zero).
1156  case (Int.eq Int.zero Int.zero); intros.
1157  auto. tauto.
1158Qed.
1159*)
1160
1161(*
1162##[ #A B C transf p b f; elim p; #fns main vars;
1163    elim fns;
1164    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
1165    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
1166        nrewrite > (?:nextfunction ?? = length ? t);
1167        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1168            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1169        ##| nrewrite > (?:nextfunction ?? = length ? t);
1170          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
1171              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1172          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
1173            ##[ #H; destruct (H); //;
1174            ##| #H; napply IH; napply H;
1175            ##]
1176          ##]
1177        ##]
1178    ##]
1179##| #A B C transf p v f; elim v;
1180    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
1181    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
1182    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
1183        whd in ⊢ (??%? → ??%?);
1184        ##[ elim p; #fns main vars; elim fns;
1185          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
1186          ##| #h t; elim h; #f fn IH;
1187              whd in ⊢ (??%? → ??%?);
1188              nrewrite > (?:nextfunction ?? = length ? t);
1189              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1190                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1191              ##| nrewrite > (?:nextfunction ?? = length ? t);
1192                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
1193                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1194                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
1195                  ##[ destruct (H); //;
1196                  ##| napply IH; napply H;
1197                  ##]
1198                ##]
1199              ##]
1200          ##]
1201       ##| #H; destruct;
1202       ##]
1203    ##]
1204##| #A B C transf p id; elim p; #fns main vars;
1205    elim fns;
1206    ##[ normalize; //
1207    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
1208        elim (ident_eq fid id); #e;
1209        ##[ whd in ⊢ (??%%);
1210          nrewrite > (?:nextfunction ?? = length ? t);
1211          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1212              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1213          ##| nrewrite > (?:nextfunction ?? = length ? t);
1214            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
1215                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1216            ##| //
1217            ##]
1218          ##]
1219        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
1220        ##]
1221    ##]
1222##| //;
1223##| #A B C transf p b tf; elim p; #fns main vars;
1224    elim fns;
1225    ##[ normalize; #H; destruct;
1226    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1227        nrewrite > (?:nextfunction ?? = length ? t);
1228        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1229            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1230        ##| nrewrite > (?:nextfunction ?? = length ? t);
1231          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
1232              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1233          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1234            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
1235            ##| #H; napply IH; napply H;
1236            ##]
1237          ##]
1238        ##]
1239    ##]
1240##| #A B C transf p v tf; elim p; #fns main vars; elim v;
1241  ##[ normalize; #H; destruct;
1242  ##| ##2,3: #x; normalize; #H; destruct;
1243  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
1244    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1245      elim fns;
1246      ##[ normalize; #H; destruct;
1247      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1248          nrewrite > (?:nextfunction ?? = length ? t);
1249          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1250              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1251          ##| nrewrite > (?:nextfunction ?? = length ? t);
1252            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
1253                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1254            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1255              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
1256              ##| #H; napply IH; napply H;
1257              ##]
1258            ##]
1259          ##]
1260      ##]
1261    ##| normalize; #H; destruct;
1262    ##]
1263 ##]
1264##] qed.
1265         
1266
1267Lemma functions_globalenv:
1268  forall (p: program F V),
1269  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
1270Proof.
1271  assert (forall init vars,
1272     functions (fst (add_globals init vars)) = functions (fst init)).
1273  induction vars; simpl.
1274  reflexivity.
1275  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
1276  simpl. exact IHvars.
1277
1278  unfold add_globals; simpl.
1279  intros. unfold globalenv; unfold globalenv_initmem.
1280  rewrite H. reflexivity.
1281Qed.
1282
1283Lemma initmem_nullptr:
1284  forall (p: program F V),
1285  let m := init_mem p in
1286  valid_block m nullptr /\
1287  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
1288Proof.
1289  pose (P := fun m => valid_block m nullptr /\
1290        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
1291  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
1292  induction vars; simpl; intros.
1293  auto.
1294  destruct a as [[id1 in1] inf1].
1295  destruct (add_globals init vars) as [g st].
1296  simpl in *. destruct IHvars. split.
1297  red; simpl. red in H0. omega.
1298  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
1299
1300  intro. unfold init_mem, globalenv_initmem. apply H.
1301  red; simpl. split. compute. auto. reflexivity.
1302Qed.
1303
1304Lemma initmem_inject_neutral:
1305  forall (p: program F V),
1306  mem_inject_neutral (init_mem p).
1307Proof.
1308  assert (forall g0 vars g1 m,
1309      add_globals (g0, Mem.empty) vars = (g1, m) →
1310      mem_inject_neutral m).
1311  Opaque alloc_init_data.
1312  induction vars; simpl.
1313  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
1314  simpl in H1. rewrite Mem.getN_init in H1.
1315  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
1316  destruct a as [[id1 init1] info1].
1317  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
1318  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
1319  intros. inv H.
1320  eapply Mem.alloc_init_data_neutral; eauto.
1321  intros. caseEq (globalenv_initmem p). intros g m EQ.
1322  unfold init_mem; rewrite EQ; simpl.
1323  unfold globalenv_initmem in EQ. eauto.
1324Qed.     
1325
1326Remark nextfunction_add_functs_neg:
1327  forall fns, nextfunction (add_functs empty fns) < 0.
1328Proof.
1329  induction fns; simpl; intros. omega. unfold Zpred. omega.
1330Qed.
1331
1332Theorem find_funct_ptr_negative:
1333  forall (p: program F V) (b: block) (f: F),
1334  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
1335Proof.
1336  intros until f.
1337  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
1338    induction fns; simpl.
1339    rewrite ZMap.gi. congruence.
1340    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
1341    intro. rewrite e. apply nextfunction_add_functs_neg.
1342    auto.
1343  unfold find_funct_ptr. rewrite functions_globalenv.
1344  intros. eauto.
1345Qed.
1346
1347Remark find_symbol_add_functs_negative:
1348  forall (fns: list (ident * F)) s b,
1349  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
1350Proof.
1351  induction fns; simpl; intros until b.
1352  rewrite PTree.gempty. congruence.
1353  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
1354  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
1355  eauto.
1356Qed.
1357
1358Remark find_symbol_add_symbols_not_fresh:
1359  forall fns vars g m s b,
1360  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
1361  (symbols g)!s = Some ? b →
1362  b < nextblock m.
1363Proof.
1364  induction vars; simpl; intros until b.
1365  intros. inversion H. subst g m. simpl.
1366  generalize (find_symbol_add_functs_negative fns s H0). omega.
1367  Transparent alloc_init_data.
1368  destruct a as [[id1 init1] info1].
1369  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
1370  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
1371  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
1372  intro EQ; inversion EQ. omega.
1373  intro. generalize (IHvars _ _ _ _ ADG H). omega.
1374Qed.
1375
1376Theorem find_symbol_not_fresh:
1377  forall (p: program F V) (id: ident) (b: block),
1378  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
1379Proof.
1380  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
1381  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
1382                      (prog_vars p)); intros g m EQ.
1383  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
1384Qed.
1385
1386Lemma find_symbol_exists:
1387  forall (p: program F V)
1388         (id: ident) (init: list init_data) (v: V),
1389  In (id, init, v) (prog_vars p) →
1390  ∃b. find_symbol ? (globalenv p) id = Some ? b.
1391Proof.
1392  intros until v.
1393  assert (forall initm vl, In (id, init, v) vl →
1394           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
1395  induction vl; simpl; intros.
1396  elim H.
1397  destruct a as [[id0 init0] v0].
1398  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
1399  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
1400  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
1401  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
1402Qed.
1403
1404Remark find_symbol_above_nextfunction:
1405  forall (id: ident) (b: block) (fns: list (ident * F)),
1406  let g := add_functs empty fns in
1407  PTree.get id g.(symbols) = Some ? b →
1408  b > g.(nextfunction).
1409Proof.
1410  induction fns; simpl.
1411  rewrite PTree.gempty. congruence.
1412  rewrite PTree.gsspec. case (peq id (fst a)); intro.
1413  intro EQ. inversion EQ. unfold Zpred. omega.
1414  intros. generalize (IHfns H). unfold Zpred; omega.
1415Qed.
1416
1417Remark find_symbol_add_globals:
1418  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
1419  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
1420  find_symbol ? (fst (add_globals ge_m vars)) id =
1421  find_symbol ? (fst ge_m) id.
1422Proof.
1423  unfold find_symbol; induction vars; simpl; intros.
1424  auto.
1425  destruct a as [[id0 init0] var0]. simpl in *.
1426  caseEq (add_globals ge_m vars); intros ge' m' EQ.
1427  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
1428  apply IHvars. tauto. intuition congruence.
1429Qed.
1430
1431Lemma find_funct_ptr_exists:
1432  forall (p: program F V) (id: ident) (f: F),
1433  list_norepet (prog_funct_names p) →
1434  list_disjoint (prog_funct_names p) (prog_var_names p) →
1435  In (id, f) (prog_funct p) →
1436  ∃b. find_symbol ? (globalenv p) id = Some ? b
1437         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
1438Proof.
1439  intros until f.
1440  assert (forall (fns: list (ident * F)),
1441           list_norepet (map (@fst ident F) fns) →
1442           In (id, f) fns →
1443           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
1444                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
1445  unfold find_symbol, find_funct_ptr. induction fns; intros.
1446  elim H0.
1447  destruct a as [id0 f0]; simpl in *. inv H.
1448  unfold add_funct; simpl.
1449  rewrite PTree.gsspec. destruct (peq id id0).
1450  subst id0. econstructor; split. eauto.
1451  replace f0 with f. apply ZMap.gss.
1452  elim H0; intro. congruence. elim H3.
1453  change id with (@fst ident F (id, f)). apply List.in_map. auto.
1454  exploit IHfns; eauto. elim H0; intro. congruence. auto.
1455  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
1456  generalize (find_symbol_above_nextfunction _ _ X).
1457  unfold block; unfold ZIndexed.t; intro; omega.
1458
1459  intros. exploit H; eauto. intros [b [X Y]].
1460  exists b; split.
1461  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
1462  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
1463  unfold prog_funct_names. change id with (fst (id, f)).
1464  apply List.in_map; auto.
1465  unfold find_funct_ptr. rewrite functions_globalenv.
1466  assumption.
1467Qed.
1468
1469Lemma find_funct_ptr_inversion:
1470  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1471  find_funct_ptr ? (globalenv p) b = Some ? f →
1472  ∃id. In (id, f) (prog_funct p).
1473Proof.
1474  intros until f.
1475  assert (forall fns: list (ident * F),
1476    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
1477    ∃id. In (id, f) fns).
1478  unfold find_funct_ptr. induction fns; simpl.
1479  rewrite ZMap.gi. congruence.
1480  destruct a as [id0 f0]; simpl.
1481  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
1482  intro. inv H. exists id0; auto.
1483  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
1484  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
1485Qed.
1486
1487Lemma find_funct_ptr_prop:
1488  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1489  (forall id f, In (id, f) (prog_funct p) → P f) →
1490  find_funct_ptr ? (globalenv p) b = Some ? f →
1491  P f.
1492Proof.
1493  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
1494Qed.
1495
1496Lemma find_funct_inversion:
1497  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1498  find_funct (globalenv p) v = Some ? f →
1499  ∃id. In (id, f) (prog_funct p).
1500Proof.
1501  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
1502  rewrite find_funct_find_funct_ptr ? in H.
1503  eapply find_funct_ptr_inversion; eauto.
1504Qed.
1505
1506Lemma find_funct_prop:
1507  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1508  (forall id f, In (id, f) (prog_funct p) → P f) →
1509  find_funct (globalenv p) v = Some ? f →
1510  P f.
1511Proof.
1512  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
1513Qed.
1514
1515Lemma find_funct_ptr_symbol_inversion:
1516  forall (p: program F V) (id: ident) (b: block) (f: F),
1517  find_symbol ? (globalenv p) id = Some ? b →
1518  find_funct_ptr ? (globalenv p) b = Some ? f →
1519  In (id, f) p.(prog_funct).
1520Proof.
1521  intros until f.
1522  assert (forall fns,
1523           let g := add_functs empty fns in
1524           PTree.get id g.(symbols) = Some ? b →
1525           ZMap.get b g.(functions) = Some ? f →
1526           In (id, f) fns).
1527    induction fns; simpl.
1528    rewrite ZMap.gi. congruence.
1529    set (g := add_functs empty fns).
1530    rewrite PTree.gsspec. rewrite ZMap.gsspec.
1531    case (peq id (fst a)); intro.
1532    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
1533    intro EQ2. left. destruct a. simpl in *. congruence.
1534    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
1535    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
1536  assert (forall g0 m0, b < 0 →
1537          forall vars g m,
1538          add_globals (g0, m0) vars = (g, m) →
1539          PTree.get id g.(symbols) = Some ? b →
1540          PTree.get id g0.(symbols) = Some ? b).
1541    induction vars; simpl.
1542    intros. inv H1. auto.
1543    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
1544    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
1545    unfold add_symbol; intros A B. rewrite <- B. simpl.
1546    rewrite PTree.gsspec. case (peq id id1); intros.
1547    assert (b > 0). inv H1. apply nextblock_pos.
1548    omegaContradiction.
1549    eauto.
1550  intros.
1551  generalize (find_funct_ptr_negative _ _ H2). intro.
1552  pose (g := add_functs empty (prog_funct p)).
1553  apply H. 
1554  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
1555  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
1556  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
1557Qed.
1558
1559Theorem find_symbol_not_nullptr:
1560  forall (p: program F V) (id: ident) (b: block),
1561  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
1562Proof.
1563  intros until b.
1564  assert (forall fns,
1565          find_symbol ? (add_functs empty fns) id = Some ? b →
1566          b <> nullptr).
1567    unfold find_symbol; induction fns; simpl.
1568    rewrite PTree.gempty. congruence.
1569    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
1570    destruct (peq id id1); intros.
1571    inversion H. generalize (nextfunction_add_functs_neg fns).
1572    unfold block, nullptr; omega.
1573    auto.
1574  set (g0 := add_functs empty p.(prog_funct)).
1575  assert (forall vars g m,
1576          add_globals (g0, Mem.empty) vars = (g, m) →
1577          find_symbol ? g id = Some ? b →
1578          b <> nullptr).
1579    induction vars; simpl; intros until m.
1580    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
1581    destruct a as [[id1 init1] info1].
1582    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
1583    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
1584    destruct (peq id id1); intros.
1585    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
1586    eauto.
1587  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
1588Qed.
1589
1590Theorem global_addresses_distinct:
1591  forall (p: program F V) id1 id2 b1 b2,
1592  id1<>id2 →
1593  find_symbol ? (globalenv p) id1 = Some ? b1 →
1594  find_symbol ? (globalenv p) id2 = Some ? b2 →
1595  b1<>b2.
1596Proof.
1597  intros.
1598  assert (forall fns,
1599    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
1600    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
1601    b1 <> b2).
1602  unfold find_symbol. induction fns; simpl; intros.
1603  rewrite PTree.gempty in H2. discriminate.
1604  destruct a as [id f]; simpl in *.
1605  rewrite PTree.gsspec in H2.
1606  destruct (peq id1 id). subst id. inv H2.
1607  rewrite PTree.gso in H3; auto.
1608  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
1609  rewrite PTree.gsspec in H3.
1610  destruct (peq id2 id). subst id. inv H3.
1611  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
1612  eauto.
1613  set (ge0 := add_functs empty p.(prog_funct)).
1614  assert (forall (vars: list (ident * list init_data * V)) ge m,
1615    add_globals (ge0, Mem.empty) vars = (ge, m) →
1616    find_symbol ? ge id1 = Some ? b1 →
1617    find_symbol ? ge id2 = Some ? b2 →
1618    b1 <> b2).
1619  unfold find_symbol. induction vars; simpl.
1620  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
1621  intros ge m. destruct a as [[id init] info].
1622  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
1623  unfold add_symbol. simpl. intros.
1624  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
1625  rewrite PTree.gso in H4; auto.
1626  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
1627  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
1628  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
1629  eauto.
1630  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
1631  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
1632  fold ge_m. apply surjective_pairing. auto. auto.
1633Qed.
1634
1635End GENV.
1636
1637(* Global environments and program transformations. *)
1638
1639Section MATCH_PROGRAM.
1640
1641Variable A B V W: Type.
1642Variable match_fun: A → B → Prop.
1643Variable match_var: V → W → Prop.
1644Variable p: program A V.
1645Variable p': program B W.
1646Hypothesis match_prog:
1647  match_program match_fun match_var p p'.
1648
1649Lemma add_functs_match:
1650  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1651  list_forall2 (match_funct_etry match_fun) fns tfns →
1652  let r := add_functs (empty A) fns in
1653  let tr := add_functs (empty B) tfns in
1654  nextfunction tr = nextfunction r /\
1655  symbols tr = symbols r /\
1656  forall (b: block) (f: A),
1657  ZMap.get b (functions r) = Some ? f →
1658  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1659Proof.
1660  induction 1; simpl.
1661
1662  split. reflexivity. split. reflexivity.
1663  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1664
1665  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1666  simpl. red in H. destruct H.
1667  destruct IHlist_forall2 as [X [Y Z]].
1668  rewrite X. rewrite Y. 
1669  split. auto.
1670  split. congruence.
1671  intros b f.
1672  repeat (rewrite ZMap.gsspec).
1673  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1674  intro EQ; inv EQ. exists fn2; auto.
1675  auto.
1676Qed.
1677
1678Lemma add_functs_rev_match:
1679  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1680  list_forall2 (match_funct_etry match_fun) fns tfns →
1681  let r := add_functs (empty A) fns in
1682  let tr := add_functs (empty B) tfns in
1683  nextfunction tr = nextfunction r /\
1684  symbols tr = symbols r /\
1685  forall (b: block) (tf: B),
1686  ZMap.get b (functions tr) = Some ? tf →
1687  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1688Proof.
1689  induction 1; simpl.
1690
1691  split. reflexivity. split. reflexivity.
1692  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1693
1694  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1695  simpl. red in H. destruct H.
1696  destruct IHlist_forall2 as [X [Y Z]].
1697  rewrite X. rewrite Y. 
1698  split. auto.
1699  split. congruence.
1700  intros b f.
1701  repeat (rewrite ZMap.gsspec).
1702  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1703  intro EQ; inv EQ. exists fn1; auto.
1704  auto.
1705Qed.
1706
1707Lemma mem_add_globals_match:
1708  forall (g1: genv A) (g2: genv B) (m: mem)
1709         (vars: list (ident * list init_data * V))
1710         (tvars: list (ident * list init_data * W)),
1711  list_forall2 (match_var_etry match_var) vars tvars →
1712  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1713Proof.
1714  induction 1; simpl.
1715  auto.
1716  destruct a1 as [[id1 init1] info1].
1717  destruct b1 as [[id2 init2] info2].
1718  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1719  generalize IHlist_forall2.
1720  destruct (add_globals (g1, m) al).
1721  destruct (add_globals (g2, m) bl).
1722  simpl. intro. subst m1. auto.
1723Qed.
1724
1725Lemma symbols_add_globals_match:
1726  forall (g1: genv A) (g2: genv B) (m: mem),
1727  symbols g1 = symbols g2 →
1728  forall (vars: list (ident * list init_data * V))
1729         (tvars: list (ident * list init_data * W)),
1730  list_forall2 (match_var_etry match_var) vars tvars →
1731  symbols (fst (add_globals (g1, m) vars)) =
1732  symbols (fst (add_globals (g2, m) tvars)).
1733Proof.
1734  induction 2; simpl.
1735  auto.
1736  destruct a1 as [[id1 init1] info1].
1737  destruct b1 as [[id2 init2] info2].
1738  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1739  generalize IHlist_forall2.
1740  generalize (mem_add_globals_match g1 g2 m H1).
1741  destruct (add_globals (g1, m) al).
1742  destruct (add_globals (g2, m) bl).
1743  simpl. intros. congruence.
1744Qed.
1745
1746Theorem find_funct_ptr_match:
1747  forall (b: block) (f: A),
1748  find_funct_ptr ? (globalenv p) b = Some ? f →
1749  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1750Proof.
1751  intros until f. destruct match_prog as [X [Y Z]].
1752  destruct (add_functs_match X) as [P [Q R]].
1753  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1754  auto.
1755Qed.
1756
1757Theorem find_funct_ptr_rev_match:
1758  forall (b: block) (tf: B),
1759  find_funct_ptr ? (globalenv p') b = Some ? tf →
1760  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1761Proof.
1762  intros until tf. destruct match_prog as [X [Y Z]].
1763  destruct (add_functs_rev_match X) as [P [Q R]].
1764  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1765  auto.
1766Qed.
1767
1768Theorem find_funct_match:
1769  forall (v: val) (f: A),
1770  find_funct (globalenv p) v = Some ? f →
1771  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1772Proof.
1773  intros until f. unfold find_funct.
1774  case v; try (intros; discriminate).
1775  intros b ofs.
1776  case (Int.eq ofs Int.zero); try (intros; discriminate).
1777  apply find_funct_ptr_match.
1778Qed.
1779
1780Theorem find_funct_rev_match:
1781  forall (v: val) (tf: B),
1782  find_funct (globalenv p') v = Some ? tf →
1783  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1784Proof.
1785  intros until tf. unfold find_funct.
1786  case v; try (intros; discriminate).
1787  intros b ofs.
1788  case (Int.eq ofs Int.zero); try (intros; discriminate).
1789  apply find_funct_ptr_rev_match.
1790Qed.
1791
1792Lemma symbols_init_match:
1793  symbols (globalenv p') = symbols (globalenv p).
1794Proof.
1795  unfold globalenv. unfold globalenv_initmem.
1796  destruct match_prog as [X [Y Z]].
1797  destruct (add_functs_match X) as [P [Q R]].
1798  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1799Qed.
1800
1801Theorem find_symbol_match:
1802  forall (s: ident),
1803  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1804Proof.
1805  intros. unfold find_symbol.
1806  rewrite symbols_init_match. auto.
1807Qed.
1808
1809Theorem init_mem_match:
1810  init_mem p' = init_mem p.
1811Proof.
1812  unfold init_mem. unfold globalenv_initmem.
1813  destruct match_prog as [X [Y Z]].
1814  symmetry. apply mem_add_globals_match. auto.
1815Qed.
1816
1817End MATCH_PROGRAM.
1818
1819Section TRANSF_PROGRAM_PARTIAL2.
1820
1821Variable A B V W: Type.
1822Variable transf_fun: A → res B.
1823Variable transf_var: V → res W.
1824Variable p: program A V.
1825Variable p': program B W.
1826Hypothesis transf_OK:
1827  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1828
1829Remark prog_match:
1830  match_program
1831    (fun fd tfd => transf_fun fd = OK ? tfd)
1832    (fun info tinfo => transf_var info = OK ? tinfo)
1833    p p'.
1834Proof.
1835  apply transform_partial_program2_match; auto.
1836Qed.
1837
1838Theorem find_funct_ptr_transf_partial2:
1839  forall (b: block) (f: A),
1840  find_funct_ptr ? (globalenv p) b = Some ? f →
1841  ∃f'.
1842  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1843Proof.
1844  intros.
1845  exploit find_funct_ptr_match. eexact prog_match. eauto.
1846  intros [tf [X Y]]. exists tf; auto.
1847Qed.
1848
1849Theorem find_funct_ptr_rev_transf_partial2:
1850  forall (b: block) (tf: B),
1851  find_funct_ptr ? (globalenv p') b = Some ? tf →
1852  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1853Proof.
1854  intros.
1855  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1856Qed.
1857
1858Theorem find_funct_transf_partial2:
1859  forall (v: val) (f: A),
1860  find_funct (globalenv p) v = Some ? f →
1861  ∃f'.
1862  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1863Proof.
1864  intros.
1865  exploit find_funct_match. eexact prog_match. eauto.
1866  intros [tf [X Y]]. exists tf; auto.
1867Qed.
1868
1869Theorem find_funct_rev_transf_partial2:
1870  forall (v: val) (tf: B),
1871  find_funct (globalenv p') v = Some ? tf →
1872  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1873Proof.
1874  intros.
1875  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1876Qed.
1877
1878Theorem find_symbol_transf_partial2:
1879  forall (s: ident),
1880  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1881Proof.
1882  intros. eapply find_symbol_match. eexact prog_match.
1883Qed.
1884
1885Theorem init_mem_transf_partial2:
1886  init_mem p' = init_mem p.
1887Proof.
1888  intros. eapply init_mem_match. eexact prog_match.
1889Qed.
1890
1891End TRANSF_PROGRAM_PARTIAL2.
1892
1893Section TRANSF_PROGRAM_PARTIAL.
1894
1895Variable A B V: Type.
1896Variable transf: A → res B.
1897Variable p: program A V.
1898Variable p': program B V.
1899Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1900
1901Remark transf2_OK:
1902  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1903Proof.
1904  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1905  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1906  rewrite map_partial_identity; auto.
1907Qed.
1908
1909Theorem find_funct_ptr_transf_partial:
1910  forall (b: block) (f: A),
1911  find_funct_ptr ? (globalenv p) b = Some ? f →
1912  ∃f'.
1913  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1914Proof.
1915  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1916Qed.
1917
1918Theorem find_funct_ptr_rev_transf_partial:
1919  forall (b: block) (tf: B),
1920  find_funct_ptr ? (globalenv p') b = Some ? tf →
1921  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1922Proof.
1923  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1924Qed.
1925
1926Theorem find_funct_transf_partial:
1927  forall (v: val) (f: A),
1928  find_funct (globalenv p) v = Some ? f →
1929  ∃f'.
1930  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1931Proof.
1932  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1933Qed.
1934
1935Theorem find_funct_rev_transf_partial:
1936  forall (v: val) (tf: B),
1937  find_funct (globalenv p') v = Some ? tf →
1938  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1939Proof.
1940  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1941Qed.
1942
1943Theorem find_symbol_transf_partial:
1944  forall (s: ident),
1945  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1946Proof.
1947  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1948Qed.
1949
1950Theorem init_mem_transf_partial:
1951  init_mem p' = init_mem p.
1952Proof.
1953  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1954Qed.
1955
1956End TRANSF_PROGRAM_PARTIAL.
1957
1958Section TRANSF_PROGRAM.
1959
1960Variable A B V: Type.
1961Variable transf: A → B.
1962Variable p: program A V.
1963Let tp := transform_program transf p.
1964
1965Remark transf_OK:
1966  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1967Proof.
1968  unfold tp, transform_program, transform_partial_program.
1969  rewrite map_partial_total. reflexivity.
1970Qed.
1971
1972Theorem find_funct_ptr_transf:
1973  forall (b: block) (f: A),
1974  find_funct_ptr ? (globalenv p) b = Some ? f →
1975  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1976Proof.
1977  intros.
1978  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1979  as [f' [X Y]]. congruence.
1980Qed.
1981
1982Theorem find_funct_ptr_rev_transf:
1983  forall (b: block) (tf: B),
1984  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1985  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1986Proof.
1987  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1988  intros [f [X Y]]. exists f; split. auto. congruence.
1989Qed.
1990
1991Theorem find_funct_transf:
1992  forall (v: val) (f: A),
1993  find_funct (globalenv p) v = Some ? f →
1994  find_funct (globalenv tp) v = Some ? (transf f).
1995Proof.
1996  intros.
1997  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1998  as [f' [X Y]]. congruence.
1999Qed.
2000
2001Theorem find_funct_rev_transf:
2002  forall (v: val) (tf: B),
2003  find_funct (globalenv tp) v = Some ? tf →
2004  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
2005Proof.
2006  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
2007  intros [f [X Y]]. exists f; split. auto. congruence.
2008Qed.
2009
2010Theorem find_symbol_transf:
2011  forall (s: ident),
2012  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
2013Proof.
2014  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
2015Qed.
2016
2017Theorem init_mem_transf:
2018  init_mem tp = init_mem p.
2019Proof.
2020  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
2021Qed.
2022
2023End TRANSF_PROGRAM.
2024
2025End Genv.
2026*)
2027
Note: See TracBrowser for help on using the repository browser.