source: src/common/Globalenvs.ma @ 2314

Last change on this file since 2314 was 2226, checked in by campbell, 8 years ago

Whole program proof.

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