source: src/common/Globalenvs.ma @ 2768

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

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

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