source: src/common/Globalenvs.ma @ 2895

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

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

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