source: src/common/Globalenvs.ma @ 2645

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