source: src/common/Globalenvs.ma @ 2500

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

Tame global environments a little.

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