source: src/common/Globalenvs.ma @ 2117

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

Workaround for bug in Matita.

File size: 63.4 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 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  ].
103cases 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 #E whd in E:(??%?);
239  cases off in E ⊢ %; [ 2,3: #x ]
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[ 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
551discriminator Prod.
552
553(* Now prove the full version. *)
554
555lemma find_funct_ptr_match:
556    ∀M:matching.∀initV,initW.
557    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
558    ∀MATCH:match_program … M p p'.
559    ∀b: block. ∀f: m_A M (prog_var_names … p).
560    find_funct_ptr … (globalenv … initV p) b = Some ? f →
561    ∃tf : m_B M (prog_var_names … p').
562    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
563[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
564* #A #B #V #W #match_fn #match_var #initV #initW
565#p #p' * #Mvars #Mfn #Mmain
566#b #f #FFP
567@(find_funct_ptr_All2 A B V W ??????? FFP)
568lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
569#E
570@(All2_mp … Mfn)
571* #id #f * #id' #f'
572<E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
573normalize #H @(match_funct_entry_inv … H) //
574qed.
575
576lemma
577  find_funct_ptr_transf_partial2:
578    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
579           ∀p: program A V. ∀p': program B W.
580    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
581    ∀b: block. ∀f: A ?.
582    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
583    ∃f'.
584    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
585#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
586cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
587[2: @iW
588| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
589#TF %{f'} % //
590-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
591qed.
592
593lemma match_funct_entry_id : ∀M,vs,vs',f,g.
594  match_funct_entry M vs vs' f g → \fst f = \fst g.
595#M #vs #vs' #f #g * //
596qed.
597
598lemma
599  find_symbol_match:
600    ∀M:matching.
601    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
602    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
603    match_program … M p p' →
604    ∀s: ident.
605    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
606* #A #B #V #W #match_fun #match_var #initV #initW #initsize
607* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
608whd in ⊢ (??%%);
609@sym_eq
610@(eq_f ??(λx. lookup SymbolTag block x s))
611whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
612whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
613change with (add_globals ?????) in match (foldl ?????);
614change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
615@(proj1 … (add_globals_match … Mvars))
616[ @(matching_fns_get_same_blocks … Mfns)
617  #f #g @match_funct_entry_id
618| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
619] qed.
620 
621lemma
622  find_symbol_transf_partial2:
623    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
624    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
625           ∀p: program A V. ∀p': program B W.
626    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
627    ∀s: ident.
628    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
629#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
630@(find_symbol_match … (transform_partial_program2_match … TPP2))
631#v0 #w0 * #id #r #v #w @sizeOK
632qed.
633
634lemma
635  find_funct_ptr_transf:
636    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
637    ∀b: block. ∀f: A ?.
638    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
639    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
640#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
641cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
642[ 2: @iV
643| #f' * #FFP'
644  whd in ⊢ (???(match % with [_⇒?]) → ?);  (* XXX this line only required to workaround unification bug *)
645  generalize in match (matching_vars ????);
646  whd in match (prog_var_names ???); whd in match (prog_vars ???);
647  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
648] qed.
649
650lemma
651  find_funct_transf:
652    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
653    ∀v: val. ∀f: A ?.
654    find_funct ? (globalenv … iV p) v = Some ? f →
655    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
656#A #B #V #iV #tf #p #v #f #FF
657cases (find_funct_find_funct_ptr ???? FF)
658#r * #b * #pc * #E destruct #FFP
659change with (find_funct_ptr ???) in ⊢ (??%?);
660@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
661qed.
662
663lemma
664  find_symbol_transf:
665    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
666    ∀s: ident.
667    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
668    find_symbol ? (globalenv … iV p) s.
669#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
670#v0 #w0 * //
671qed.
672
673lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
674  symbols A ge = symbols … ge' →
675  store_init_data A ge m b o d = store_init_data B ge' m b o d.
676#A #B #ge #ge' #m #b #o #d #SYM
677whd in ⊢ (??%%);
678cases d #d' try @refl
679#id #n whd in ⊢ (??%%);
680whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
681qed.
682
683lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
684  symbols A ge = symbols … ge' →
685  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
686#A #B #ge #ge' #b #SYM #d elim d
687[ //
688| #hd #tl #IH #m #o
689  whd in ⊢ (??%%);
690  >(store_init_data_symbols … SYM)
691  cases (store_init_data ??????)
692  [ %
693  | #m' @IH
694  ]
695] qed.
696
697lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
698  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
699  ∀ge:genv_t A. ∀ge':genv_t B.
700  symbols … ge = symbols … ge' →
701   ∀m. ∀vars,vars'.
702  All2 … P vars vars' →
703  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
704#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
705whd in ⊢ (? → ? → ??%%);
706generalize in match (OK ? m);
707elim vars
708[ #rm *
709  [ #_ %
710  | #h #t *
711  ]
712| * #idr #v #tl #IH #rm
713  * [ * ]
714  * #idr' #w #tl'
715  * #p cases (varsOK … p) #E1 #E2 destruct #TL
716  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
717  whd in ⊢ (??(????%?)(????%?));
718  [ whd in match (find_symbol ?? id);
719    whd in match (find_symbol B ? id);
720    >SYM cases (lookup ??? id)
721    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
722  ] @IH //
723] qed.
724
725lemma
726  init_mem_match:
727    ∀M:matching.
728    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
729    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
730    match_program … M p p' →
731    init_mem … iW p' = init_mem … iV p.
732* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
733whd in ⊢ (??%%);
734change with (add_globals ?????) in match (globalenv_allocmem ??? p');
735change with (add_globals ?????) in match (globalenv_allocmem ??? p);
736cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
737[ 8: @(matching_fns_get_same_blocks … Mfns)
738     #f0 #g0 * //
739| cases (add_globals ?????) #ge1 #m1
740  cases (add_globals ?????) #ge2 #m2
741  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
742  [ #v0 #w0 * #id #r #v #w /3/
743  | @SYM
744  ]
745| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
746| *: skip
747] qed.
748
749lemma
750  init_mem_transf:
751    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
752    init_mem … iV (transform_program … p transf) = init_mem … iV p.
753#A #B #C #iV #transf #p
754@(init_mem_match … (transform_program_match … transf ?))
755//
756qed.
757   
758
759(* Package up transform_program results for global envs nicely. *)
760
761record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
762  rg_find_symbol: ∀s.
763    find_symbol … ge s = find_symbol … ge' s;
764  rg_find_funct: ∀v,f.
765    find_funct … ge v = Some ? f →
766    find_funct … ge' v = Some ? (t f);
767  rg_find_funct_ptr: ∀b,f.
768    find_funct_ptr … ge b = Some ? f →
769    find_funct_ptr … ge' b = Some ? (t f)
770}.
771
772theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
773  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
774#A #B #V #iV #p #tf %
775[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
776| @(find_funct_transf A B V iV tf p)
777| @(find_funct_ptr_transf A B V iV p tf)
778] qed.
779
780
781(*
782
783  find_funct_ptr_match:
784    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
785           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
786    match_program … match_fun match_var p p' →
787    ∀b: block. ∀f: A.
788    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
789    ∃tf : B.
790    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
791  find_funct_ptr_rev_match:
792    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
793           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
794    match_program … match_fun match_var p p' →
795    ∀b: block. ∀tf: B.
796    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
797    ∃f : A.
798    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
799  find_funct_match:
800    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
801           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
802    match_program … match_fun match_var p p' →
803    ∀v: val. ∀f: A.
804    find_funct ? (globalenv ?? p) v = Some ? f →
805    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
806  find_funct_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    ∀v: val. ∀tf: B.
811    find_funct ? (globalenv ?? p') v = Some ? tf →
812    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
813  find_symbol_match:
814    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
815           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
816    match_program … match_fun match_var p p' →
817    ∀s: ident.
818    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
819*)
820(*
821Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
822  ZMap.get b g.(functions).
823
824Definition find_funct (g: genv) (v: val) : option F :=
825  match v with
826  | Vptr b ofs =>
827      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
828  | _ =>
829      None
830  end.
831
832Definition find_symbol ? (g: genv) (symb: ident) : option block :=
833  PTree.get symb g.(symbols).
834
835Lemma find_funct_inv:
836  forall (ge: t) (v: val) (f: F),
837  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
838Proof.
839  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
840  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
841  exists b. congruence.
842  discriminate.
843Qed.
844
845Lemma find_funct_find_funct_ptr:
846  forall (ge: t) (b: block),
847  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
848Proof.
849  intros. simpl.
850  generalize (Int.eq_spec Int.zero Int.zero).
851  case (Int.eq Int.zero Int.zero); intros.
852  auto. tauto.
853Qed.
854*)
855
856(*
857##[ #A B C transf p b f; elim p; #fns main vars;
858    elim fns;
859    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
860    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
861        nrewrite > (?:nextfunction ?? = length ? t);
862        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
863            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
864        ##| nrewrite > (?:nextfunction ?? = length ? t);
865          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
866              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
867          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
868            ##[ #H; destruct (H); //;
869            ##| #H; napply IH; napply H;
870            ##]
871          ##]
872        ##]
873    ##]
874##| #A B C transf p v f; elim v;
875    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
876    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
877    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
878        whd in ⊢ (??%? → ??%?);
879        ##[ elim p; #fns main vars; elim fns;
880          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
881          ##| #h t; elim h; #f fn IH;
882              whd in ⊢ (??%? → ??%?);
883              nrewrite > (?:nextfunction ?? = length ? t);
884              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
885                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
886              ##| nrewrite > (?:nextfunction ?? = length ? t);
887                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
888                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
889                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
890                  ##[ destruct (H); //;
891                  ##| napply IH; napply H;
892                  ##]
893                ##]
894              ##]
895          ##]
896       ##| #H; destruct;
897       ##]
898    ##]
899##| #A B C transf p id; elim p; #fns main vars;
900    elim fns;
901    ##[ normalize; //
902    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
903        elim (ident_eq fid id); #e;
904        ##[ whd in ⊢ (??%%);
905          nrewrite > (?:nextfunction ?? = length ? t);
906          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
907              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
908          ##| nrewrite > (?:nextfunction ?? = length ? t);
909            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
910                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
911            ##| //
912            ##]
913          ##]
914        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
915        ##]
916    ##]
917##| //;
918##| #A B C transf p b tf; elim p; #fns main vars;
919    elim fns;
920    ##[ normalize; #H; destruct;
921    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
922        nrewrite > (?:nextfunction ?? = length ? t);
923        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
924            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
925        ##| nrewrite > (?:nextfunction ?? = length ? t);
926          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
927              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
928          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
929            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
930            ##| #H; napply IH; napply H;
931            ##]
932          ##]
933        ##]
934    ##]
935##| #A B C transf p v tf; elim p; #fns main vars; elim v;
936  ##[ normalize; #H; destruct;
937  ##| ##2,3: #x; normalize; #H; destruct;
938  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
939    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
940      elim fns;
941      ##[ normalize; #H; destruct;
942      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
943          nrewrite > (?:nextfunction ?? = length ? t);
944          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
945              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
946          ##| nrewrite > (?:nextfunction ?? = length ? t);
947            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
948                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
949            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
950              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
951              ##| #H; napply IH; napply H;
952              ##]
953            ##]
954          ##]
955      ##]
956    ##| normalize; #H; destruct;
957    ##]
958 ##]
959##] qed.
960         
961
962Lemma functions_globalenv:
963  forall (p: program F V),
964  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
965Proof.
966  assert (forall init vars,
967     functions (fst (add_globals init vars)) = functions (fst init)).
968  induction vars; simpl.
969  reflexivity.
970  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
971  simpl. exact IHvars.
972
973  unfold add_globals; simpl.
974  intros. unfold globalenv; unfold globalenv_initmem.
975  rewrite H. reflexivity.
976Qed.
977
978Lemma initmem_nullptr:
979  forall (p: program F V),
980  let m := init_mem p in
981  valid_block m nullptr /\
982  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
983Proof.
984  pose (P := fun m => valid_block m nullptr /\
985        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
986  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
987  induction vars; simpl; intros.
988  auto.
989  destruct a as [[id1 in1] inf1].
990  destruct (add_globals init vars) as [g st].
991  simpl in *. destruct IHvars. split.
992  red; simpl. red in H0. omega.
993  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
994
995  intro. unfold init_mem, globalenv_initmem. apply H.
996  red; simpl. split. compute. auto. reflexivity.
997Qed.
998
999Lemma initmem_inject_neutral:
1000  forall (p: program F V),
1001  mem_inject_neutral (init_mem p).
1002Proof.
1003  assert (forall g0 vars g1 m,
1004      add_globals (g0, Mem.empty) vars = (g1, m) →
1005      mem_inject_neutral m).
1006  Opaque alloc_init_data.
1007  induction vars; simpl.
1008  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
1009  simpl in H1. rewrite Mem.getN_init in H1.
1010  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
1011  destruct a as [[id1 init1] info1].
1012  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
1013  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
1014  intros. inv H.
1015  eapply Mem.alloc_init_data_neutral; eauto.
1016  intros. caseEq (globalenv_initmem p). intros g m EQ.
1017  unfold init_mem; rewrite EQ; simpl.
1018  unfold globalenv_initmem in EQ. eauto.
1019Qed.     
1020
1021Remark nextfunction_add_functs_neg:
1022  forall fns, nextfunction (add_functs empty fns) < 0.
1023Proof.
1024  induction fns; simpl; intros. omega. unfold Zpred. omega.
1025Qed.
1026
1027Theorem find_funct_ptr_negative:
1028  forall (p: program F V) (b: block) (f: F),
1029  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
1030Proof.
1031  intros until f.
1032  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
1033    induction fns; simpl.
1034    rewrite ZMap.gi. congruence.
1035    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
1036    intro. rewrite e. apply nextfunction_add_functs_neg.
1037    auto.
1038  unfold find_funct_ptr. rewrite functions_globalenv.
1039  intros. eauto.
1040Qed.
1041
1042Remark find_symbol_add_functs_negative:
1043  forall (fns: list (ident * F)) s b,
1044  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
1045Proof.
1046  induction fns; simpl; intros until b.
1047  rewrite PTree.gempty. congruence.
1048  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
1049  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
1050  eauto.
1051Qed.
1052
1053Remark find_symbol_add_symbols_not_fresh:
1054  forall fns vars g m s b,
1055  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
1056  (symbols g)!s = Some ? b →
1057  b < nextblock m.
1058Proof.
1059  induction vars; simpl; intros until b.
1060  intros. inversion H. subst g m. simpl.
1061  generalize (find_symbol_add_functs_negative fns s H0). omega.
1062  Transparent alloc_init_data.
1063  destruct a as [[id1 init1] info1].
1064  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
1065  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
1066  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
1067  intro EQ; inversion EQ. omega.
1068  intro. generalize (IHvars _ _ _ _ ADG H). omega.
1069Qed.
1070
1071Theorem find_symbol_not_fresh:
1072  forall (p: program F V) (id: ident) (b: block),
1073  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
1074Proof.
1075  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
1076  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
1077                      (prog_vars p)); intros g m EQ.
1078  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
1079Qed.
1080
1081Lemma find_symbol_exists:
1082  forall (p: program F V)
1083         (id: ident) (init: list init_data) (v: V),
1084  In (id, init, v) (prog_vars p) →
1085  ∃b. find_symbol ? (globalenv p) id = Some ? b.
1086Proof.
1087  intros until v.
1088  assert (forall initm vl, In (id, init, v) vl →
1089           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
1090  induction vl; simpl; intros.
1091  elim H.
1092  destruct a as [[id0 init0] v0].
1093  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
1094  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
1095  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
1096  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
1097Qed.
1098
1099Remark find_symbol_above_nextfunction:
1100  forall (id: ident) (b: block) (fns: list (ident * F)),
1101  let g := add_functs empty fns in
1102  PTree.get id g.(symbols) = Some ? b →
1103  b > g.(nextfunction).
1104Proof.
1105  induction fns; simpl.
1106  rewrite PTree.gempty. congruence.
1107  rewrite PTree.gsspec. case (peq id (fst a)); intro.
1108  intro EQ. inversion EQ. unfold Zpred. omega.
1109  intros. generalize (IHfns H). unfold Zpred; omega.
1110Qed.
1111
1112Remark find_symbol_add_globals:
1113  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
1114  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
1115  find_symbol ? (fst (add_globals ge_m vars)) id =
1116  find_symbol ? (fst ge_m) id.
1117Proof.
1118  unfold find_symbol; induction vars; simpl; intros.
1119  auto.
1120  destruct a as [[id0 init0] var0]. simpl in *.
1121  caseEq (add_globals ge_m vars); intros ge' m' EQ.
1122  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
1123  apply IHvars. tauto. intuition congruence.
1124Qed.
1125
1126Lemma find_funct_ptr_exists:
1127  forall (p: program F V) (id: ident) (f: F),
1128  list_norepet (prog_funct_names p) →
1129  list_disjoint (prog_funct_names p) (prog_var_names p) →
1130  In (id, f) (prog_funct p) →
1131  ∃b. find_symbol ? (globalenv p) id = Some ? b
1132         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
1133Proof.
1134  intros until f.
1135  assert (forall (fns: list (ident * F)),
1136           list_norepet (map (@fst ident F) fns) →
1137           In (id, f) fns →
1138           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
1139                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
1140  unfold find_symbol, find_funct_ptr. induction fns; intros.
1141  elim H0.
1142  destruct a as [id0 f0]; simpl in *. inv H.
1143  unfold add_funct; simpl.
1144  rewrite PTree.gsspec. destruct (peq id id0).
1145  subst id0. econstructor; split. eauto.
1146  replace f0 with f. apply ZMap.gss.
1147  elim H0; intro. congruence. elim H3.
1148  change id with (@fst ident F (id, f)). apply List.in_map. auto.
1149  exploit IHfns; eauto. elim H0; intro. congruence. auto.
1150  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
1151  generalize (find_symbol_above_nextfunction _ _ X).
1152  unfold block; unfold ZIndexed.t; intro; omega.
1153
1154  intros. exploit H; eauto. intros [b [X Y]].
1155  exists b; split.
1156  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
1157  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
1158  unfold prog_funct_names. change id with (fst (id, f)).
1159  apply List.in_map; auto.
1160  unfold find_funct_ptr. rewrite functions_globalenv.
1161  assumption.
1162Qed.
1163
1164Lemma find_funct_ptr_inversion:
1165  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1166  find_funct_ptr ? (globalenv p) b = Some ? f →
1167  ∃id. In (id, f) (prog_funct p).
1168Proof.
1169  intros until f.
1170  assert (forall fns: list (ident * F),
1171    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
1172    ∃id. In (id, f) fns).
1173  unfold find_funct_ptr. induction fns; simpl.
1174  rewrite ZMap.gi. congruence.
1175  destruct a as [id0 f0]; simpl.
1176  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
1177  intro. inv H. exists id0; auto.
1178  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
1179  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
1180Qed.
1181
1182Lemma find_funct_ptr_prop:
1183  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1184  (forall id f, In (id, f) (prog_funct p) → P f) →
1185  find_funct_ptr ? (globalenv p) b = Some ? f →
1186  P f.
1187Proof.
1188  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
1189Qed.
1190
1191Lemma find_funct_inversion:
1192  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1193  find_funct (globalenv p) v = Some ? f →
1194  ∃id. In (id, f) (prog_funct p).
1195Proof.
1196  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
1197  rewrite find_funct_find_funct_ptr ? in H.
1198  eapply find_funct_ptr_inversion; eauto.
1199Qed.
1200
1201Lemma find_funct_prop:
1202  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1203  (forall id f, In (id, f) (prog_funct p) → P f) →
1204  find_funct (globalenv p) v = Some ? f →
1205  P f.
1206Proof.
1207  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
1208Qed.
1209
1210Lemma find_funct_ptr_symbol_inversion:
1211  forall (p: program F V) (id: ident) (b: block) (f: F),
1212  find_symbol ? (globalenv p) id = Some ? b →
1213  find_funct_ptr ? (globalenv p) b = Some ? f →
1214  In (id, f) p.(prog_funct).
1215Proof.
1216  intros until f.
1217  assert (forall fns,
1218           let g := add_functs empty fns in
1219           PTree.get id g.(symbols) = Some ? b →
1220           ZMap.get b g.(functions) = Some ? f →
1221           In (id, f) fns).
1222    induction fns; simpl.
1223    rewrite ZMap.gi. congruence.
1224    set (g := add_functs empty fns).
1225    rewrite PTree.gsspec. rewrite ZMap.gsspec.
1226    case (peq id (fst a)); intro.
1227    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
1228    intro EQ2. left. destruct a. simpl in *. congruence.
1229    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
1230    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
1231  assert (forall g0 m0, b < 0 →
1232          forall vars g m,
1233          add_globals (g0, m0) vars = (g, m) →
1234          PTree.get id g.(symbols) = Some ? b →
1235          PTree.get id g0.(symbols) = Some ? b).
1236    induction vars; simpl.
1237    intros. inv H1. auto.
1238    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
1239    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
1240    unfold add_symbol; intros A B. rewrite <- B. simpl.
1241    rewrite PTree.gsspec. case (peq id id1); intros.
1242    assert (b > 0). inv H1. apply nextblock_pos.
1243    omegaContradiction.
1244    eauto.
1245  intros.
1246  generalize (find_funct_ptr_negative _ _ H2). intro.
1247  pose (g := add_functs empty (prog_funct p)).
1248  apply H. 
1249  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
1250  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
1251  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
1252Qed.
1253
1254Theorem find_symbol_not_nullptr:
1255  forall (p: program F V) (id: ident) (b: block),
1256  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
1257Proof.
1258  intros until b.
1259  assert (forall fns,
1260          find_symbol ? (add_functs empty fns) id = Some ? b →
1261          b <> nullptr).
1262    unfold find_symbol; induction fns; simpl.
1263    rewrite PTree.gempty. congruence.
1264    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
1265    destruct (peq id id1); intros.
1266    inversion H. generalize (nextfunction_add_functs_neg fns).
1267    unfold block, nullptr; omega.
1268    auto.
1269  set (g0 := add_functs empty p.(prog_funct)).
1270  assert (forall vars g m,
1271          add_globals (g0, Mem.empty) vars = (g, m) →
1272          find_symbol ? g id = Some ? b →
1273          b <> nullptr).
1274    induction vars; simpl; intros until m.
1275    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
1276    destruct a as [[id1 init1] info1].
1277    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
1278    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
1279    destruct (peq id id1); intros.
1280    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
1281    eauto.
1282  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
1283Qed.
1284
1285Theorem global_addresses_distinct:
1286  forall (p: program F V) id1 id2 b1 b2,
1287  id1<>id2 →
1288  find_symbol ? (globalenv p) id1 = Some ? b1 →
1289  find_symbol ? (globalenv p) id2 = Some ? b2 →
1290  b1<>b2.
1291Proof.
1292  intros.
1293  assert (forall fns,
1294    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
1295    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
1296    b1 <> b2).
1297  unfold find_symbol. induction fns; simpl; intros.
1298  rewrite PTree.gempty in H2. discriminate.
1299  destruct a as [id f]; simpl in *.
1300  rewrite PTree.gsspec in H2.
1301  destruct (peq id1 id). subst id. inv H2.
1302  rewrite PTree.gso in H3; auto.
1303  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
1304  rewrite PTree.gsspec in H3.
1305  destruct (peq id2 id). subst id. inv H3.
1306  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
1307  eauto.
1308  set (ge0 := add_functs empty p.(prog_funct)).
1309  assert (forall (vars: list (ident * list init_data * V)) ge m,
1310    add_globals (ge0, Mem.empty) vars = (ge, m) →
1311    find_symbol ? ge id1 = Some ? b1 →
1312    find_symbol ? ge id2 = Some ? b2 →
1313    b1 <> b2).
1314  unfold find_symbol. induction vars; simpl.
1315  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
1316  intros ge m. destruct a as [[id init] info].
1317  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
1318  unfold add_symbol. simpl. intros.
1319  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
1320  rewrite PTree.gso in H4; auto.
1321  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
1322  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
1323  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
1324  eauto.
1325  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
1326  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
1327  fold ge_m. apply surjective_pairing. auto. auto.
1328Qed.
1329
1330End GENV.
1331
1332(* Global environments and program transformations. *)
1333
1334Section MATCH_PROGRAM.
1335
1336Variable A B V W: Type.
1337Variable match_fun: A → B → Prop.
1338Variable match_var: V → W → Prop.
1339Variable p: program A V.
1340Variable p': program B W.
1341Hypothesis match_prog:
1342  match_program match_fun match_var p p'.
1343
1344Lemma add_functs_match:
1345  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1346  list_forall2 (match_funct_etry match_fun) fns tfns →
1347  let r := add_functs (empty A) fns in
1348  let tr := add_functs (empty B) tfns in
1349  nextfunction tr = nextfunction r /\
1350  symbols tr = symbols r /\
1351  forall (b: block) (f: A),
1352  ZMap.get b (functions r) = Some ? f →
1353  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1354Proof.
1355  induction 1; simpl.
1356
1357  split. reflexivity. split. reflexivity.
1358  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1359
1360  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1361  simpl. red in H. destruct H.
1362  destruct IHlist_forall2 as [X [Y Z]].
1363  rewrite X. rewrite Y. 
1364  split. auto.
1365  split. congruence.
1366  intros b f.
1367  repeat (rewrite ZMap.gsspec).
1368  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1369  intro EQ; inv EQ. exists fn2; auto.
1370  auto.
1371Qed.
1372
1373Lemma add_functs_rev_match:
1374  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1375  list_forall2 (match_funct_etry match_fun) fns tfns →
1376  let r := add_functs (empty A) fns in
1377  let tr := add_functs (empty B) tfns in
1378  nextfunction tr = nextfunction r /\
1379  symbols tr = symbols r /\
1380  forall (b: block) (tf: B),
1381  ZMap.get b (functions tr) = Some ? tf →
1382  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1383Proof.
1384  induction 1; simpl.
1385
1386  split. reflexivity. split. reflexivity.
1387  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1388
1389  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1390  simpl. red in H. destruct H.
1391  destruct IHlist_forall2 as [X [Y Z]].
1392  rewrite X. rewrite Y. 
1393  split. auto.
1394  split. congruence.
1395  intros b f.
1396  repeat (rewrite ZMap.gsspec).
1397  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1398  intro EQ; inv EQ. exists fn1; auto.
1399  auto.
1400Qed.
1401
1402Lemma mem_add_globals_match:
1403  forall (g1: genv A) (g2: genv B) (m: mem)
1404         (vars: list (ident * list init_data * V))
1405         (tvars: list (ident * list init_data * W)),
1406  list_forall2 (match_var_etry match_var) vars tvars →
1407  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1408Proof.
1409  induction 1; simpl.
1410  auto.
1411  destruct a1 as [[id1 init1] info1].
1412  destruct b1 as [[id2 init2] info2].
1413  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1414  generalize IHlist_forall2.
1415  destruct (add_globals (g1, m) al).
1416  destruct (add_globals (g2, m) bl).
1417  simpl. intro. subst m1. auto.
1418Qed.
1419
1420Lemma symbols_add_globals_match:
1421  forall (g1: genv A) (g2: genv B) (m: mem),
1422  symbols g1 = symbols g2 →
1423  forall (vars: list (ident * list init_data * V))
1424         (tvars: list (ident * list init_data * W)),
1425  list_forall2 (match_var_etry match_var) vars tvars →
1426  symbols (fst (add_globals (g1, m) vars)) =
1427  symbols (fst (add_globals (g2, m) tvars)).
1428Proof.
1429  induction 2; simpl.
1430  auto.
1431  destruct a1 as [[id1 init1] info1].
1432  destruct b1 as [[id2 init2] info2].
1433  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1434  generalize IHlist_forall2.
1435  generalize (mem_add_globals_match g1 g2 m H1).
1436  destruct (add_globals (g1, m) al).
1437  destruct (add_globals (g2, m) bl).
1438  simpl. intros. congruence.
1439Qed.
1440
1441Theorem find_funct_ptr_match:
1442  forall (b: block) (f: A),
1443  find_funct_ptr ? (globalenv p) b = Some ? f →
1444  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1445Proof.
1446  intros until f. destruct match_prog as [X [Y Z]].
1447  destruct (add_functs_match X) as [P [Q R]].
1448  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1449  auto.
1450Qed.
1451
1452Theorem find_funct_ptr_rev_match:
1453  forall (b: block) (tf: B),
1454  find_funct_ptr ? (globalenv p') b = Some ? tf →
1455  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1456Proof.
1457  intros until tf. destruct match_prog as [X [Y Z]].
1458  destruct (add_functs_rev_match X) as [P [Q R]].
1459  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1460  auto.
1461Qed.
1462
1463Theorem find_funct_match:
1464  forall (v: val) (f: A),
1465  find_funct (globalenv p) v = Some ? f →
1466  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1467Proof.
1468  intros until f. unfold find_funct.
1469  case v; try (intros; discriminate).
1470  intros b ofs.
1471  case (Int.eq ofs Int.zero); try (intros; discriminate).
1472  apply find_funct_ptr_match.
1473Qed.
1474
1475Theorem find_funct_rev_match:
1476  forall (v: val) (tf: B),
1477  find_funct (globalenv p') v = Some ? tf →
1478  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1479Proof.
1480  intros until tf. unfold find_funct.
1481  case v; try (intros; discriminate).
1482  intros b ofs.
1483  case (Int.eq ofs Int.zero); try (intros; discriminate).
1484  apply find_funct_ptr_rev_match.
1485Qed.
1486
1487Lemma symbols_init_match:
1488  symbols (globalenv p') = symbols (globalenv p).
1489Proof.
1490  unfold globalenv. unfold globalenv_initmem.
1491  destruct match_prog as [X [Y Z]].
1492  destruct (add_functs_match X) as [P [Q R]].
1493  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1494Qed.
1495
1496Theorem find_symbol_match:
1497  forall (s: ident),
1498  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1499Proof.
1500  intros. unfold find_symbol.
1501  rewrite symbols_init_match. auto.
1502Qed.
1503
1504Theorem init_mem_match:
1505  init_mem p' = init_mem p.
1506Proof.
1507  unfold init_mem. unfold globalenv_initmem.
1508  destruct match_prog as [X [Y Z]].
1509  symmetry. apply mem_add_globals_match. auto.
1510Qed.
1511
1512End MATCH_PROGRAM.
1513
1514Section TRANSF_PROGRAM_PARTIAL2.
1515
1516Variable A B V W: Type.
1517Variable transf_fun: A → res B.
1518Variable transf_var: V → res W.
1519Variable p: program A V.
1520Variable p': program B W.
1521Hypothesis transf_OK:
1522  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1523
1524Remark prog_match:
1525  match_program
1526    (fun fd tfd => transf_fun fd = OK ? tfd)
1527    (fun info tinfo => transf_var info = OK ? tinfo)
1528    p p'.
1529Proof.
1530  apply transform_partial_program2_match; auto.
1531Qed.
1532
1533Theorem find_funct_ptr_transf_partial2:
1534  forall (b: block) (f: A),
1535  find_funct_ptr ? (globalenv p) b = Some ? f →
1536  ∃f'.
1537  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1538Proof.
1539  intros.
1540  exploit find_funct_ptr_match. eexact prog_match. eauto.
1541  intros [tf [X Y]]. exists tf; auto.
1542Qed.
1543
1544Theorem find_funct_ptr_rev_transf_partial2:
1545  forall (b: block) (tf: B),
1546  find_funct_ptr ? (globalenv p') b = Some ? tf →
1547  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1548Proof.
1549  intros.
1550  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1551Qed.
1552
1553Theorem find_funct_transf_partial2:
1554  forall (v: val) (f: A),
1555  find_funct (globalenv p) v = Some ? f →
1556  ∃f'.
1557  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1558Proof.
1559  intros.
1560  exploit find_funct_match. eexact prog_match. eauto.
1561  intros [tf [X Y]]. exists tf; auto.
1562Qed.
1563
1564Theorem find_funct_rev_transf_partial2:
1565  forall (v: val) (tf: B),
1566  find_funct (globalenv p') v = Some ? tf →
1567  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1568Proof.
1569  intros.
1570  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1571Qed.
1572
1573Theorem find_symbol_transf_partial2:
1574  forall (s: ident),
1575  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1576Proof.
1577  intros. eapply find_symbol_match. eexact prog_match.
1578Qed.
1579
1580Theorem init_mem_transf_partial2:
1581  init_mem p' = init_mem p.
1582Proof.
1583  intros. eapply init_mem_match. eexact prog_match.
1584Qed.
1585
1586End TRANSF_PROGRAM_PARTIAL2.
1587
1588Section TRANSF_PROGRAM_PARTIAL.
1589
1590Variable A B V: Type.
1591Variable transf: A → res B.
1592Variable p: program A V.
1593Variable p': program B V.
1594Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1595
1596Remark transf2_OK:
1597  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1598Proof.
1599  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1600  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1601  rewrite map_partial_identity; auto.
1602Qed.
1603
1604Theorem find_funct_ptr_transf_partial:
1605  forall (b: block) (f: A),
1606  find_funct_ptr ? (globalenv p) b = Some ? f →
1607  ∃f'.
1608  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1609Proof.
1610  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1611Qed.
1612
1613Theorem find_funct_ptr_rev_transf_partial:
1614  forall (b: block) (tf: B),
1615  find_funct_ptr ? (globalenv p') b = Some ? tf →
1616  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1617Proof.
1618  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1619Qed.
1620
1621Theorem find_funct_transf_partial:
1622  forall (v: val) (f: A),
1623  find_funct (globalenv p) v = Some ? f →
1624  ∃f'.
1625  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1626Proof.
1627  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1628Qed.
1629
1630Theorem find_funct_rev_transf_partial:
1631  forall (v: val) (tf: B),
1632  find_funct (globalenv p') v = Some ? tf →
1633  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1634Proof.
1635  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1636Qed.
1637
1638Theorem find_symbol_transf_partial:
1639  forall (s: ident),
1640  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1641Proof.
1642  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1643Qed.
1644
1645Theorem init_mem_transf_partial:
1646  init_mem p' = init_mem p.
1647Proof.
1648  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1649Qed.
1650
1651End TRANSF_PROGRAM_PARTIAL.
1652
1653Section TRANSF_PROGRAM.
1654
1655Variable A B V: Type.
1656Variable transf: A → B.
1657Variable p: program A V.
1658Let tp := transform_program transf p.
1659
1660Remark transf_OK:
1661  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1662Proof.
1663  unfold tp, transform_program, transform_partial_program.
1664  rewrite map_partial_total. reflexivity.
1665Qed.
1666
1667Theorem find_funct_ptr_transf:
1668  forall (b: block) (f: A),
1669  find_funct_ptr ? (globalenv p) b = Some ? f →
1670  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1671Proof.
1672  intros.
1673  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1674  as [f' [X Y]]. congruence.
1675Qed.
1676
1677Theorem find_funct_ptr_rev_transf:
1678  forall (b: block) (tf: B),
1679  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1680  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1681Proof.
1682  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1683  intros [f [X Y]]. exists f; split. auto. congruence.
1684Qed.
1685
1686Theorem find_funct_transf:
1687  forall (v: val) (f: A),
1688  find_funct (globalenv p) v = Some ? f →
1689  find_funct (globalenv tp) v = Some ? (transf f).
1690Proof.
1691  intros.
1692  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1693  as [f' [X Y]]. congruence.
1694Qed.
1695
1696Theorem find_funct_rev_transf:
1697  forall (v: val) (tf: B),
1698  find_funct (globalenv tp) v = Some ? tf →
1699  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1700Proof.
1701  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1702  intros [f [X Y]]. exists f; split. auto. congruence.
1703Qed.
1704
1705Theorem find_symbol_transf:
1706  forall (s: ident),
1707  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1708Proof.
1709  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1710Qed.
1711
1712Theorem init_mem_transf:
1713  init_mem tp = init_mem p.
1714Proof.
1715  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1716Qed.
1717
1718End TRANSF_PROGRAM.
1719
1720End Genv.
1721*)
1722
Note: See TracBrowser for help on using the repository browser.