source: src/common/Globalenvs.ma @ 2624

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

Properly evict unused and axiomatised Floats.

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