source: src/common/Globalenvs.ma @ 3367

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

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

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