source: src/common/Globalenvs.ma @ 2540

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* * Global environments are a component of the dynamic semantics of 
  all languages involved in the compiler.  A global environment
  maps symbol names (names of functions and of global variables)
  to the corresponding memory addresses.  It also maps memory addresses
  of functions to the corresponding function descriptions.  

  Global environments, along with the initial memory state at the beginning
  of program execution, are built from the program of interest, as follows:
- A distinct memory address is assigned to each function of the program.
  These function addresses use negative numbers to distinguish them from
  addresses of memory blocks.  The associations of function name to function
  address and function address to function description are recorded in
  the global environment.
- For each global variable, a memory block is allocated and associated to
  the name of the variable.

  These operations reflect (at a high level of abstraction) what takes
  place during program linking and program loading in a real operating
  system. *)

include "common/Errors.ma".
include "common/AST.ma".
(*include "Values.ma".*)
include "common/FrontEndMem.ma".

   (* * The type of global environments.  The parameter [F] is the type
       of function descriptions. *)
(* Functions are given negative block numbers *)
record genv_t (F:Type[0]) : Type[0] ≝ {
  functions: positive_map F;
  nextfunction: Pos;
  symbols: identifier_map SymbolTag block;
  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
                 ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
}.

(* We deal with shadowed names by overwriting their global environment entry
   and getting rid of any function mapping (the latter is necessary so that we
   get a reverse mapping).  In fact, the parser will prevent these anyway, but
   adding the uniqueness of these names throughout would be more trouble than
   it's worth. *)
   
definition drop_fn : ∀F:Type[0]. ident → genv_t F → genv_t F ≝
λF,id,g.
let fns ≝
  match lookup ?? (symbols … g) id with
  [ None ⇒ functions … g
  | Some b' ⇒
      match b' with
      [ mk_block r x ⇒
        match r with
        [ Code ⇒
          match x with
          [ neg p ⇒ pm_set … p (None ?) (functions … g)
          | _ ⇒ functions … g
          ]
        | _ ⇒ functions … g
        ]
      | _ ⇒ functions … g
      ]
  ]
in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
whd in match fns; -fns
#b #L
cases (functions_inv ? g b ?)
[ #id' #L'
  cases (identifier_eq … id id')
  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
  | #NE %{id'} >lookup_remove_miss /2/
  ]
| cases (lookup ?? (symbols F g) id) in L;
  [ normalize //
  | * * * [ 2,3,5,6: #b' ] normalize //
    #H cut (b ≠ b')
    [ % #E destruct >lookup_opt_pm_set_hit in H; * /2/ ]
    #NE >lookup_opt_pm_set_miss in H; //
  ]
] qed.

lemma drop_fn_id : ∀F,id,ge.
  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
#F #id * #fns #next #syms #inv
whd in match (drop_fn ???);
@lookup_remove_hit
qed.

lemma drop_fn_lfn : ∀F,id,ge,b,f.
  lookup_opt ? b (functions … (drop_fn F id ge)) = Some ? f →
  lookup_opt ? b (functions … ge) = Some ? f.
#F #id #ge #b #f
whd in match (drop_fn ???);
cases (lookup ??? id)
[ normalize //
| * * * [2,3,5,6: #b' ] normalize //
  cases (decidable_eq_pos b b')
  [ #E destruct >lookup_opt_pm_set_hit #E destruct
  | #NE >lookup_opt_pm_set_miss //
  ]
] qed.

definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝
λF,name_fun,g.
  let blk_id ≝ nextfunction ? g in
  let b ≝ mk_block Code (neg blk_id) in
  let g' ≝ drop_fn F (\fst name_fun) g in
  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
              (succ blk_id)
              (add ?? (symbols … g') (\fst name_fun) b) ?.
#b' #L whd in match b;
cases (decidable_eq_pos blk_id b')
[ #E destruct
  %{(\fst name_fun)} @lookup_add_hit
| #NE
  cases (functions_inv ? g' b' ?)
  [ #id #L' %{id} >lookup_add_miss
    [ @L'
    | % #E destruct
      >drop_fn_id in L'; #E destruct
    ]
  | >lookup_opt_insert_miss in L; /2/
  ]
] qed.

definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
λF,name,b,g.
  let g' ≝ drop_fn F name g in
  mk_genv_t F (functions … g')
              (nextfunction … g')
              (add ?? (symbols … g') name b)
              ?.
#b' #L
cases (functions_inv ? g' b' ?)
[ #id #L' %{id} >lookup_add_miss
  [ @L'
  | % #E destruct
    >drop_fn_id in L'; #E destruct
  ]
| @L
] qed.

(* Construct environment and initial memory store *)
definition empty_mem ≝ empty. (* XXX*)
definition empty : ∀F. genv_t F ≝
  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??) ?.
#b #L normalize in L; cases L #L cases (L (refl ??))
qed. 

definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
λF,init,fns.
  foldr ?? (add_funct F) init fns.

(* Return the address of the given global symbol, if any. *)
definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
λF,ge. lookup ?? (symbols … ge).

(* init *)

definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝
λF,ge,m,b,p,id.
  (* store checks that the address came from something capable of representing
     addresses of the memory region in question - here there are no real
     pointers, so use the real region. *)
  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
  match id with
  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
  | Init_float32 n ⇒ None ? (*store (ASTfloat F32) m ptr (Vfloat n)*)
  | Init_float64 n ⇒ None ? (*store (ASTfloat F64) m ptr (Vfloat n) *)
  | Init_addrof (*r'*) symb ofs ⇒
      match find_symbol … ge symb with
      [ None ⇒ None ?
      | Some b' ⇒ (*
        match pointer_compat_dec b' r' with
        [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs))))
        (*| inr _ ⇒ None ?
        ]*)
      ]
  | Init_space n ⇒ Some ? m
  | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*))
  ].
(*cases b //
qed.*)

definition size_init_data : init_data → nat ≝ 
 λi_data.match i_data with
  [ Init_int8 _ ⇒ 1
  | Init_int16 _ ⇒ 2
  | Init_int32 _ ⇒ 4
  | Init_float32 _ ⇒ 4
  | Init_float64 _ ⇒ 8
  | Init_space n ⇒ max n 0
  | Init_null (*r*) ⇒ size_pointer (*r*)
  | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)].

let rec store_init_data_list (F:Type[0]) (ge:genv_t F) 
                              (m: mem) (b: block) (p: Z) (idl: list init_data)
                              on idl : option mem ≝
  match idl with
  [ nil ⇒ Some ? m
  | cons id idl' ⇒
      match store_init_data F ge m b p id with
      [ None ⇒ None ?
      | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'
      ]
  ].

definition size_init_data_list : list init_data → nat ≝ 
  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.

(* Nonessential properties that may require arithmetic
nremark size_init_data_list_pos:
  ∀i_data. OZ ≤ size_init_data_list i_data.
#i_data;elim i_data;//;
#a;#tl;cut (OZ ≤ size_init_data a)
##[cases a;normalize;//;
   #x;cases x;normalize;//;
##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
   cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
   ##[cases (size_init_data a) in Hsize IH;
      ##[##1,2:/3/
      ##|normalize;#n;#Hfalse;elim Hfalse]
   ##|#Hdisc;cases Hdisc
      ##[#Heq;nrewrite > Heq;//;
      ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2;
         (* TODO: arithmetics *) napply daemon]
   ##]
##]
qed.
*)


(* init *)

axiom InitDataStoreFailed : String.

definition add_globals : ∀F,V:Type[0].
       (V → (list init_data)) →
       genv_t F × mem → list (ident × region × V) →
       (genv_t F × mem) ≝
λF,V,extract_init,init_env,vars.
  foldl ??
    (λg_st: genv_t F × mem. λid_init: ident × region × V.
      let 〈id, r, init_info〉 ≝ id_init in
      let init ≝ extract_init init_info in
      let 〈g,st〉 ≝ g_st in
        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
          let g' ≝ add_symbol ? id b g in
            〈g', st'〉
        )
    init_env vars.

definition init_globals : ∀F,V:Type[0].
       (V → (list init_data)) →
       genv_t F → mem → list (ident × region × V) →
       res mem ≝
λF,V,extract_init,g,m,vars.
  foldl ??
    (λst: res mem. λid_init: ident × region × V.
      let 〈id, r, init_info〉 ≝ id_init in
      let init ≝ extract_init init_info in
        do st ← st;
        match find_symbol … g id with
        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
        ] )
    (OK ? m) vars.

definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝
λF,V,init_info,p.
  add_globals … init_info
   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
   (prog_vars ?? p).

(* Return the global environment for the given program. *)
definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝
λF,V,i,p.
  \fst (globalenv_allocmem F V i p).

(* Return the global environment for the given program with no data initialisation. *)
definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
λF,p.
  globalenv F nat (λn.[Init_space n]) p.

(* Return the initial memory state for the given program. *)
definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝
λF,V,i,p.
  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
  init_globals ? V i g m (prog_vars ?? p).

(* Setup memory when data initialisation is not required (has the benefit
   of being total. *)
definition alloc_mem: ∀F. program F nat → mem ≝
λF,p.
  \snd (globalenv_allocmem F nat (λn. [Init_space n]) p).

(* Return the function description associated with the given address, if any. *)
definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝
λF,ge,b. match block_region b with [ Code ⇒
           match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge)
         | _ ⇒ None ? ] | _ ⇒ None ? ].

(* Same as [find_funct_ptr] but the function address is given as
   a value, which must be a pointer with offset 0. *)
definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝
λ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 ? ].


(* Turn a memory block into the original symbol. *)
definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
λF,genv,b.
  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).


lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
  find_funct F ge v = Some F f →
  ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
#F #ge *
[ #f #E normalize in E; destruct
| #sz #i #f #E normalize in E; destruct
(*| #f #fn #E normalize in E; destruct*)
| (*#r*) #f #E normalize in E; destruct
| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
  @eq_offset_elim #Eoff
  #E whd in E:(??%?); destruct
  (*%{pty}*) %{b} (*%{c}*) % // @E
] qed.
  
lemma add_globals_match : ∀A,B,V,W,initV,initW.
  ∀P:(ident × region × V) → (ident × region × W) → Prop.
  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
  ∀vars,ge,ge',m,vars'.
  symbols ? ge = symbols … ge' →
  All2 … P vars vars' →
  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧  
  \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars').
#A #B #V #W #initV #initW #P #varsOK
#vars elim vars
[ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ]
| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
  * * #id' #r' #w #tl' #E * #p #TL
  whd in match (add_globals A ????);
  change with (add_globals A ????) in match (foldl ?????); 
  whd in match (add_globals B ????);
  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
  cases (varsOK … p) #E1 #E2
  destruct >E2 cases (alloc ????) #m' #b
  @IH /2/
  whd in match (add_symbol ????); whd in match (drop_fn ???);
  whd in match (add_symbol ????); whd in match (drop_fn ???);
  >E %
] qed.


lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
  (∀f,g. P f g → \fst f = \fst g) →
  ∀fns,fns'.
  All2 … P fns fns' →
  let ge ≝ add_functs A (empty ?) fns in
  let ge' ≝ add_functs B (empty ?) fns' in
  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
#A #B #P #fnOK #fns elim fns
[ * [ #_ % % | #h #t * ]
| * #id #f #tl #IH * [ * ]
  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
  whd in match (add_functs ???);
  change with (add_functs ???) in match (foldr ?????);
  whd in match (add_functs B ??);
  change with (add_functs ???) in match (foldr (ident × B) ????);
  cases (IH tl' H) #E1 #E2
  % [ >E1 %
    | whd in match (drop_fn ???);
      whd in match (drop_fn ???);
      >E1 >E2 % ]
] qed.

lemma matching_fns_get_same_blocks :  ∀A,B,P.
  (∀f,g. P f g → \fst f = \fst g) →
  ∀fns,fns'.
  All2 … P fns fns' →
  let ge ≝ add_functs A (empty ?) fns in
  let ge' ≝ add_functs B (empty ?) fns' in
  symbols … ge = symbols … ge'.
#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
qed.

lemma symbol_of_block_rev : ∀F,genv,b,id.
  symbol_for_block F genv b = Some ? id →
  find_symbol F genv id = Some ? b.
#F #genv #b #id #H whd in H:(??%?);
@(find_lookup … (λid,b'. eq_block b b'))
lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
cases (find ????) in H ⊢ %;
[ normalize #E destruct
| * #id' #b' normalize in ⊢ (% → ?); #E destruct
  #H lapply (H … (refl ??))
  @eq_block_elim
  [ #E destruct //
  | #_ *
  ]
] qed.

(* The mapping of blocks to symbols is total for functions. *)

definition symbol_of_function_block : ∀F,ge,b. find_funct_ptr F ge b ≠ None ? → ident ≝
λF,ge,b,FFP.
match symbol_for_block F ge b return λx. symbol_for_block ??? = x → ? with
[ None ⇒ λH. ⊥
| Some id ⇒ λ_. id
] (refl ? (symbol_for_block F ge b)).
whd in H:(??%?);
cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
cases (functions_inv … ge b FFP)
#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
cases (find ????)
[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
| * #id' #b' #_ normalize #_ #E destruct
] qed.


(*
(* * ** Properties of the operations. *)

  find_funct_inv:
    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
  find_funct_find_funct_ptr:
    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
*)
lemma find_symbol_exists:
    ∀F,V. ∀init. ∀p: program F V. ∀id.
    Exists ? (λx. x = id) (map … (λx. \fst x) (prog_funct ?? p) @ map … (λx. \fst (\fst x)) (prog_vars ?? p)) →
    ∃b. find_symbol ? (globalenv … init p) id = Some ? b.
#F #V #init * #vars #fns #main #id
whd in match (globalenv ????);
whd in match (globalenv_allocmem ????);
whd in match (prog_var_names ???);
generalize in match (F ?) in fns ⊢ %; -F #F #fns
#EX 
cut (Exists ident (λx.x = id) (map … (λx.\fst (\fst x)) vars) ∨
     ∃b. find_symbol ? (add_functs F (empty F) fns) id = Some ? b)
[ cases (Exists_append … EX)
  [ -EX #EX %2
    elim fns in EX ⊢ %;
    [ *
    | * #id' #f #tl #IH *
      [ #E destruct
        change with (foldr ?????) in match (add_functs F (empty F) ?);
        change with (lookup ????) in match (find_symbol ???);
        whd in match (foldr ?????);
        % [2: @lookup_add_hit | skip ]
      | #TL
        change with (foldr ?????) in match (add_functs F (empty F) ?);
        change with (lookup ????) in match (find_symbol ???);
        whd in match (foldr ?????);
        cases (identifier_eq ? id id')
        [ #E destruct
          % [2: @lookup_add_hit | skip ]
        | #NE >lookup_add_miss //
          whd in match (drop_fn ???);
          >lookup_remove_miss // @IH @TL
        ]
      ]
    ]
  | #EX %1 @EX
  ]
]
-EX
generalize in match (add_functs F (empty F) fns);
generalize in match empty_mem;
elim vars
[ #m #ge * [ * | // ]
| * * #id' #r' #v' #tl #IH #m #ge *
  [ *
    [ #E destruct
      (* Found one, but it might be shadowed later *)
      whd in match (foldl ?????); normalize nodelta
      cases (alloc ????) #m' #b normalize nodelta
      cut (find_symbol F (add_symbol F id b ge) id = Some ? b)
      [ change with (lookup ????) in ⊢ (??%?);
        whd in match add_symbol; normalize nodelta
        @lookup_add_hit ]
      #F @IH %2 %{b} @F
    | #TL whd in match (foldl ?????); normalize nodelta
      cases (alloc ????) #m' #b'
      @IH %1 @TL
    ]
  | #H whd in match (foldl ?????); normalize nodelta
    cases (alloc ????) #m' #b' normalize nodelta
    @IH %2
    cases (identifier_eq ? id id')
    [ #E destruct %{b'}
      whd in match add_symbol; normalize nodelta
      @lookup_add_hit
    | #NE cases H #b #H' %{b}
      whd in match add_symbol; normalize nodelta
      change with (lookup ???? = ?) >lookup_add_miss //
      whd in match (drop_fn ???); >lookup_remove_miss // @H'
    ]
  ]
] qed.

(*
  find_funct_ptr_exists:
    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
    list_norepet ? (prog_funct_names ?? p) →
    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
    in_list ? 〈id, f〉 (prog_funct ?? p) →
    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;

  find_funct_ptr_inversion:
    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
  find_funct_inversion:
    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
    find_funct ? (globalenv ?? p) v = Some ? f →
    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
  find_funct_ptr_symbol_inversion:
    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    in_list ? 〈id, f〉 (prog_funct ?? p);

  find_funct_ptr_prop:
    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    P f;
  find_funct_prop:
    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
    find_funct ? (globalenv ?? p) v = Some ? f →
    P f;

  initmem_nullptr:
    ∀F,V: Type[0]. ∀p: program F V.
    let m ≝ init_mem ?? p in
    valid_block m nullptr ∧
    (blocks m) nullptr = empty_block 0 0 Any;
(*  initmem_inject_neutral:
    ∀F,V: Type[0]. ∀p: program F V.
    mem_inject_neutral (init_mem ?? p);*)
  find_funct_ptr_negative:
    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
  find_symbol_not_fresh:
    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
  find_symbol_not_nullptr:
    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
  global_addresses_distinct:
    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
    id1≠id2 →
    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
    b1≠b2;

(* * Commutation properties between program transformations
  and operations over global environments. *)

  find_funct_ptr_rev_transf:
    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    ∀b : block. ∀tf : B.
    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
  find_funct_rev_transf:
    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    ∀v : val. ∀tf : B.
    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;

(* * Commutation properties between partial program transformations
  and operations over global environments. *)

  find_funct_ptr_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    ∀b: block. ∀f: A.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    ∃f'.
    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
  find_funct_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    ∀v: val. ∀f: A.
    find_funct ? (globalenv ?? p) v = Some ? f →
    ∃f'.
    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
  find_symbol_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    ∀s: ident.
    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
  init_mem_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    init_mem ?? p' = init_mem ?? p;
  find_funct_ptr_rev_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    ∀b : block. ∀tf : B.
    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
    ∃f : A.
      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
  find_funct_rev_transf_partial:
    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    transform_partial_program … transf p = OK ? p' →
    ∀v : val. ∀tf : B.
    find_funct ? (globalenv ?? p') v = Some ? tf →
    ∃f : A.
      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;

  find_funct_ptr_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    ∀b: block. ∀f: A.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    ∃f'.
    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
  find_funct_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    ∀v: val. ∀f: A.
    find_funct ? (globalenv ?? p) v = Some ? f →
    ∃f'.
    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
  find_symbol_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    ∀s: ident.
    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
  init_mem_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    init_mem ?? p' = init_mem ?? p;
  find_funct_ptr_rev_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    ∀b: block. ∀tf: B.
    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
    ∃f : A.
      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
  find_funct_rev_transf_partial2:
    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    ∀v: val. ∀tf: B.
    find_funct ? (globalenv ?? p') v = Some ? tf →
    ∃f : A.
      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;

(* * Commutation properties between matching between programs
  and operations over global environments. *)
*) *)

(* First, show that nextfunction only depends on the number of functions: *)

let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
match n with
[ O ⇒ p
| S m ⇒ succ (nat_plus_pos m p)
].

lemma nextfunction_length : ∀A,l,ge.
  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
#A #l elim l // #h #t #IH #ge
whd in ⊢ (??%%); >IH //
qed.

lemma alloc_pair : ∀m,m',l,h,l',h',r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].
  nextblock m = nextblock m' →
  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
  P (alloc m l h r) (alloc m' l' h' r).
* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H % 
qed.

lemma vars_irrelevant_to_find_funct_ptr :
  ∀F,G,V,W.
  ∀P:F → G → Prop.
  ∀init,init',b,vars,vars',ge,ge',m,m',f.
  (find_funct_ptr F ge b = Some ? f → ∃f'. find_funct_ptr G ge' b = Some ? f' ∧ P f f') →
  symbols F ge = symbols G ge' →
  nextblock m = nextblock m' →
  All2 … (λx,y. \fst x = \fst y) vars vars' →
  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f →
  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
#F #G #V #W #P #init #init'
* * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ] 
#vars elim vars
[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
    | #x #tl #ge #ge' #m #m' #f #_ #_ #_ *
    ]
| * * #id #r #v #tl #IH *
  [ #ge #ge' #m #m' #f #_ #_ #_ *
  | * * #id' #r' #v' #tl'
    #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH
    whd in match (add_globals ?????); whd in match (add_globals G ????);
    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
    @(alloc_pair … Enext) #m1 #m2 #b #Enext'
    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
    #FFP
    @(IH … MATCH FFP)
    [ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
      whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?));
      >Esym
      cases (lookup … id')
      [ @FFP1
      | * * * try @FFP1 #p try @FFP1
        normalize
        cases (decidable_eq_pos blk p)
        [ #E destruct >lookup_opt_pm_set_hit #E destruct
        | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE)
          @FFP1
        ]
      ]
    | whd in match (add_symbol ????); whd in match (drop_fn ???);
      whd in match (add_symbol ????); whd in match (drop_fn ???);
      >Esym %
    | assumption
    ]
  ]
] qed.

(* Now link functions in related programs, but without dealing with the type
   casts yet. *)

lemma symbols_drop_fn_eq : ∀A,B,ge,ge',id.
  symbols A ge = symbols B ge' →
  symbols A (drop_fn A id ge) = symbols B (drop_fn B id ge').
#A #B #ge #ge' #id #E
whd in ⊢ (??(??%)(??%));
>E %
qed.

lemma ge_add_functs : ∀A,B,fns,fns'.
  All2 ?? (λx,y. \fst x = \fst y) fns fns' →
  symbols A (add_functs A (empty ?) fns) = symbols B (add_functs B (empty ?) fns') ∧
  nextfunction A (add_functs A (empty ?) fns) = nextfunction B (add_functs B (empty ?) fns').
#A #B
#fns elim fns
[ * [ #_ % % | #h #t * ]
| * #id #a #tl #IH * * #id' #b #tl' * #E destruct #TL
  whd in match (add_functs ???); whd in match (add_functs B ??);
  cases (IH ? TL) #S #N >N % [2: % ]
  >(symbols_drop_fn_eq A B (foldr ??? (empty A) tl) (foldr ?? (add_funct B) (empty B) tl'))
  [ %
  | @S
  ]
] qed.

lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
#F #ge #id #b #f
whd in match (drop_fn F id ge);
cases (lookup … id)
[ #_ % #E destruct
| * * * [2,3,5,6: #b'] normalize
  [4: cases (decidable_eq_pos b b') 
    [ #E destruct >lookup_opt_pm_set_hit #E destruct
    | #NE #_ @(not_to_not … NE) #E destruct //
    ]
  | *: #_ % #E destruct
  ]
] qed. 

lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
#F #ge #id #b
whd in match (drop_fn F id ge);
cases (lookup … id)
[ //
| * * * //
  #b' normalize #NE
  @lookup_opt_pm_set_miss
  @(not_to_not … NE)
  #E destruct %
] qed.

lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
  All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
  All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') →
  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
#Mfns
cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
[ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
@vars_irrelevant_to_find_funct_ptr
[ letin varnames ≝ (map ??? vars)
  generalize in match fns' in Mfns ⊢ %;
  elim fns
  [ #fns' #Mfns whd in ⊢ (??%? → ?); #E destruct
  | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl
    whd in ⊢ (??%? → ?);
    whd in match (functions ??);
    change with (add_functs ???) in match (foldr ?????);
    cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … Mtl) * #idA #a * #idB #b * // ]
    #SYMS #NEXT
    cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl)))
    [ #E destruct >lookup_opt_insert_hit #E destruct
      %{fn'} % // whd in ⊢ (??%?);
      whd in match (functions ??);
      change with (add_functs ???) in match (foldr ???? tl');
      >NEXT >lookup_opt_insert_hit @refl
    | #NE >lookup_opt_insert_miss //
      #FFP cases (IH tl' Mtl ?)
      [ #fn'' * #FFP' #P' %{fn''} %
        [ whd in ⊢ (??%?);
          >lookup_opt_insert_miss [2: <NEXT // ]
          lapply (lookup_drop_fn_different ????? FFP)
          >SYMS
          #L >lookup_drop_fn_irrelevant // @FFP'
        | @P'
        ]
      | @(drop_fn_lfn … FFP)
      ]
    ]
  ]
| cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ]
  #S #_ @S
| @refl
] qed.

(* lazy proof *)
lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P.
  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
  All ? (λx. P (\snd x)) (prog_funct ?? p) →
  P f.
#A #V #b #p #f #initV #P #FFP #ALL
cut (All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
[ elim (prog_funct … p) in ALL ⊢ %;
  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
cut (All2 ?? (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p))
[ elim (prog_vars … p) [ // | * #x #x' #tl #TL /2/ ] ]
#VARS2 #FNS2
cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FNS2 VARS2 FFP)
#x * //
qed.


discriminator Prod.

(* Now prove the full version. *)

lemma find_funct_ptr_match:
    ∀M:matching.∀initV,initW.
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    ∀MATCH:match_program … M p p'.
    ∀b: block. ∀f: m_A M (prog_var_names … p).
    find_funct_ptr … (globalenv … initV p) b = Some ? f →
    ∃tf : m_B M (prog_var_names … p').
    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
* #A #B #V #W #match_fn #match_var #initV #initW
#p #p' * #Mvars #Mfn #Mmain
#b #f #FFP
@(find_funct_ptr_All2 A B V W ????????? FFP)
[ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
  #E
  @(All2_mp … Mfn) 
  * #id #f * #id' #f'
  <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
  normalize #H @(match_funct_entry_inv … H)
  #vs #id1 #f1 #f2 #M % //
| @(All2_mp … Mvars)
  * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct //
qed.

lemma
  find_funct_ptr_transf_partial2:
    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
    ∀b: block. ∀f: A ?.
    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
    ∃f'.
    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
[2: @iW
| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
#TF %{f'} % //
-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
qed.

lemma match_funct_entry_id : ∀M,vs,vs',f,g.
  match_funct_entry M vs vs' f g → \fst f = \fst g.
#M #vs #vs' #f #g * //
qed.

lemma
  find_symbol_match:
    ∀M:matching.
    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    match_program … M p p' →
    ∀s: ident.
    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
* #A #B #V #W #match_fun #match_var #initV #initW #initsize
* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
whd in ⊢ (??%%);
@sym_eq
@(eq_f ??(λx. lookup SymbolTag block x s))
whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
change with (add_globals ?????) in match (foldl ?????);
change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
@(proj1 … (add_globals_match … Mvars))
[ @(matching_fns_get_same_blocks … Mfns) 
  #f #g @match_funct_entry_id
| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
] qed.
  
lemma
  find_symbol_transf_partial2:
    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
           ∀p: program A V. ∀p': program B W.
    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
    ∀s: ident.
    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
@(find_symbol_match … (transform_partial_program2_match … TPP2))
#v0 #w0 * #id #r #v #w @sizeOK
qed.

lemma
  find_funct_ptr_transf:
    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
    ∀b: block. ∀f: A ?.
    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
[ 2: @iV
| #f' * #FFP'
  whd in ⊢ (???(match % with [_⇒?]) → ?);  (* XXX this line only required to workaround unification bug *)
  generalize in match (matching_vars ????);
  whd in match (prog_var_names ???); whd in match (prog_vars ???);
  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
] qed.

lemma
  find_funct_transf:
    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
    ∀v: val. ∀f: A ?.
    find_funct ? (globalenv … iV p) v = Some ? f →
    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
#A #B #V #iV #tf #p #v #f #FF
cases (find_funct_find_funct_ptr ???? FF)
#b * #E destruct #FFP
change with (find_funct_ptr ???) in ⊢ (??%?);
@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
qed.

lemma
  find_symbol_transf:
    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
    ∀s: ident.
    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
    find_symbol ? (globalenv … iV p) s.
#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
#v0 #w0 * //
qed.

lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
  symbols A ge = symbols … ge' →
  store_init_data A ge m b o d = store_init_data B ge' m b o d.
#A #B #ge #ge' #m #b #o #d #SYM
whd in ⊢ (??%%);
cases d try #d' try @refl
#n whd in ⊢ (??%%);
whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
qed.

lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
  symbols A ge = symbols … ge' →
  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
#A #B #ge #ge' #b #SYM #d elim d
[ //
| #hd #tl #IH #m #o
  whd in ⊢ (??%%);
  >(store_init_data_symbols … SYM)
  cases (store_init_data ??????) 
  [ %
  | #m' @IH
  ]
] qed.

lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
  ∀ge:genv_t A. ∀ge':genv_t B.
  symbols … ge = symbols … ge' →
   ∀m. ∀vars,vars'.
  All2 … P vars vars' →
  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
whd in ⊢ (? → ? → ??%%);
generalize in match (OK ? m);
elim vars
[ #rm *
  [ #_ % 
  | #h #t *
  ]
| * #idr #v #tl #IH #rm
  * [ * ]
  * #idr' #w #tl'
  * #p cases (varsOK … p) #E1 #E2 destruct #TL
  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
  whd in ⊢ (??(????%?)(????%?));
  [ whd in match (find_symbol ?? id);
    whd in match (find_symbol B ? id);
    >SYM cases (lookup ??? id)
    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
  ] @IH //
] qed.

lemma
  init_mem_match:
    ∀M:matching.
    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    match_program … M p p' →
    init_mem … iW p' = init_mem … iV p.
* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
whd in ⊢ (??%%);
change with (add_globals ?????) in match (globalenv_allocmem ??? p'); 
change with (add_globals ?????) in match (globalenv_allocmem ??? p);
cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
[ 8: @(matching_fns_get_same_blocks … Mfns)
     #f0 #g0 * //
| cases (add_globals ?????) #ge1 #m1
  cases (add_globals ?????) #ge2 #m2
  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
  [ #v0 #w0 * #id #r #v #w /3/
  | @SYM
  ]
| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
| *: skip
] qed.

lemma
  init_mem_transf:
    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
    init_mem … iV (transform_program … p transf) = init_mem … iV p.
#A #B #C #iV #transf #p
@(init_mem_match … (transform_program_match … transf ?))
//
qed.

lemma
  init_mem_transf_gen:
    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
#tag #A #B #C #iV #g #transf #p
@(init_mem_match … (transform_program_gen_match … transf ?))
//
qed.
    

(* Package up transform_program results for global envs nicely. *)

record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
  rg_find_symbol: ∀s.
    find_symbol … ge s = find_symbol … ge' s;
  rg_find_funct: ∀v,f.
    find_funct … ge v = Some ? f →
    find_funct … ge' v = Some ? (t f);
  rg_find_funct_ptr: ∀b,f.
    find_funct_ptr … ge b = Some ? f →
    find_funct_ptr … ge' b = Some ? (t f)
}.

theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
#A #B #V #iV #p #tf %
[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
| @(find_funct_transf A B V iV tf p)
| @(find_funct_ptr_transf A B V iV p tf)
] qed.

record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
  rgg_find_symbol: ∀s.
    find_symbol … ge s = find_symbol … ge' s;
  rgg_find_funct_ptr: ∀b,f.
    find_funct_ptr … ge b = Some ? f →
    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
  rgg_find_funct: ∀v,f.
    find_funct … ge v = Some ? f →
    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
}.

include "utilities/bool.ma".

theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
  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))).
#tag #A #B #V #iV #g #p #tf %
[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
  #v #w * //
| #b #f #FFP
  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
  [ 2: @iV
  | #fn' * #FFP'
    generalize in match (matching_vars ????);
    whd in match (prog_var_names ???); whd in match (prog_vars ???);
    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
  | skip
  ]
| * [ 4: #ptr #fn whd in match (find_funct ???);
     @if_elim #Eoff #FFP
     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
       [ 2: @iV
       | #fn' * #FFP'
         generalize in match (matching_vars ????);
         whd in match (prog_var_names ???); whd in match (prog_vars ???);
         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
       ]
     | destruct
     ]
    | *: normalize #A #B try #C try #D destruct
    ]
] qed.


(*

  find_funct_ptr_match:
    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    match_program … match_fun match_var p p' →
    ∀b: block. ∀f: A.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    ∃tf : B.
    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
  find_funct_ptr_rev_match:
    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    match_program … match_fun match_var p p' →
    ∀b: block. ∀tf: B.
    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
    ∃f : A.
    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
  find_funct_match:
    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    match_program … match_fun match_var p p' →
    ∀v: val. ∀f: A.
    find_funct ? (globalenv ?? p) v = Some ? f →
    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
  find_funct_rev_match:
    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    match_program … match_fun match_var p p' →
    ∀v: val. ∀tf: B.
    find_funct ? (globalenv ?? p') v = Some ? tf →
    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
  find_symbol_match:
    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    match_program … match_fun match_var p p' →
    ∀s: ident.
    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
*)
(*
Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
  ZMap.get b g.(functions).

Definition find_funct (g: genv) (v: val) : option F :=
  match v with
  | Vptr b ofs =>
      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
  | _ =>
      None
  end.

Definition find_symbol ? (g: genv) (symb: ident) : option block :=
  PTree.get symb g.(symbols).

Lemma find_funct_inv:
  forall (ge: t) (v: val) (f: F),
  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
Proof.
  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
  exists b. congruence.
  discriminate.
Qed.

Lemma find_funct_find_funct_ptr:
  forall (ge: t) (b: block),
  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. 
Proof.
  intros. simpl. 
  generalize (Int.eq_spec Int.zero Int.zero).
  case (Int.eq Int.zero Int.zero); intros.
  auto. tauto.
Qed.
*)

(*
##[ #A B C transf p b f; elim p; #fns main vars;
    elim fns;
    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
        nrewrite > (?:nextfunction ?? = length ? t);
        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
        ##| nrewrite > (?:nextfunction ?? = length ? t);
          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
            ##[ #H; destruct (H); //;
            ##| #H; napply IH; napply H;
            ##]
          ##]
        ##]
    ##]
##| #A B C transf p v f; elim v;
    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
        whd in ⊢ (??%? → ??%?);
        ##[ elim p; #fns main vars; elim fns;
          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
          ##| #h t; elim h; #f fn IH;
              whd in ⊢ (??%? → ??%?);
              nrewrite > (?:nextfunction ?? = length ? t);
              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
              ##| nrewrite > (?:nextfunction ?? = length ? t);
                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
                  ##[ destruct (H); //;
                  ##| napply IH; napply H;
                  ##]
                ##]
              ##]
          ##]
       ##| #H; destruct;
       ##]
    ##]
##| #A B C transf p id; elim p; #fns main vars;
    elim fns;
    ##[ normalize; //
    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
        elim (ident_eq fid id); #e;
        ##[ whd in ⊢ (??%%);
          nrewrite > (?:nextfunction ?? = length ? t);
          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
          ##| nrewrite > (?:nextfunction ?? = length ? t);
            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
            ##| //
            ##]
          ##]
        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
        ##]
    ##]
##| //;
##| #A B C transf p b tf; elim p; #fns main vars;
    elim fns;
    ##[ normalize; #H; destruct;
    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
        nrewrite > (?:nextfunction ?? = length ? t);
        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
        ##| nrewrite > (?:nextfunction ?? = length ? t);
          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
            ##| #H; napply IH; napply H;
            ##]
          ##]
        ##]
    ##]
##| #A B C transf p v tf; elim p; #fns main vars; elim v;
  ##[ normalize; #H; destruct;
  ##| ##2,3: #x; normalize; #H; destruct;
  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
      elim fns;
      ##[ normalize; #H; destruct;
      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
          nrewrite > (?:nextfunction ?? = length ? t);
          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
          ##| nrewrite > (?:nextfunction ?? = length ? t);
            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
              ##| #H; napply IH; napply H;
              ##]
            ##]
          ##]
      ##]
    ##| normalize; #H; destruct;
    ##]
 ##]
##] qed.
         

Lemma functions_globalenv:
  forall (p: program F V),
  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
Proof.
  assert (forall init vars,
     functions (fst (add_globals init vars)) = functions (fst init)).
  induction vars; simpl.
  reflexivity.
  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
  simpl. exact IHvars. 

  unfold add_globals; simpl. 
  intros. unfold globalenv; unfold globalenv_initmem.
  rewrite H. reflexivity.
Qed.

Lemma initmem_nullptr:
  forall (p: program F V),
  let m := init_mem p in
  valid_block m nullptr /\
  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
Proof.
  pose (P := fun m => valid_block m nullptr /\
        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
  induction vars; simpl; intros.
  auto.
  destruct a as [[id1 in1] inf1]. 
  destruct (add_globals init vars) as [g st]. 
  simpl in *. destruct IHvars. split.
  red; simpl. red in H0. omega.
  simpl. rewrite update_o. auto. unfold block. red in H0. omega. 

  intro. unfold init_mem, globalenv_initmem. apply H. 
  red; simpl. split. compute. auto. reflexivity.
Qed. 

Lemma initmem_inject_neutral:
  forall (p: program F V),
  mem_inject_neutral (init_mem p).
Proof.
  assert (forall g0 vars g1 m,
      add_globals (g0, Mem.empty) vars = (g1, m) →
      mem_inject_neutral m).
  Opaque alloc_init_data.
  induction vars; simpl. 
  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
  simpl in H1. rewrite Mem.getN_init in H1. 
  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
  destruct a as [[id1 init1] info1]. 
  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
  intros. inv H. 
  eapply Mem.alloc_init_data_neutral; eauto.
  intros. caseEq (globalenv_initmem p). intros g m EQ.
  unfold init_mem; rewrite EQ; simpl. 
  unfold globalenv_initmem in EQ. eauto.
Qed.      

Remark nextfunction_add_functs_neg:
  forall fns, nextfunction (add_functs empty fns) < 0.
Proof.
  induction fns; simpl; intros. omega. unfold Zpred. omega.
Qed.

Theorem find_funct_ptr_negative:
  forall (p: program F V) (b: block) (f: F),
  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
Proof.
  intros until f.
  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
    induction fns; simpl.
    rewrite ZMap.gi. congruence.
    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
    intro. rewrite e. apply nextfunction_add_functs_neg.
    auto. 
  unfold find_funct_ptr. rewrite functions_globalenv. 
  intros. eauto.
Qed.

Remark find_symbol_add_functs_negative:
  forall (fns: list (ident * F)) s b,
  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
Proof.
  induction fns; simpl; intros until b.
  rewrite PTree.gempty. congruence.
  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
  eauto.
Qed.

Remark find_symbol_add_symbols_not_fresh:
  forall fns vars g m s b,
  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
  (symbols g)!s = Some ? b →
  b < nextblock m.
Proof.
  induction vars; simpl; intros until b.
  intros. inversion H. subst g m. simpl. 
  generalize (find_symbol_add_functs_negative fns s H0). omega.
  Transparent alloc_init_data.
  destruct a as [[id1 init1] info1]. 
  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
  intro EQ; inversion EQ. omega.
  intro. generalize (IHvars _ _ _ _ ADG H). omega.
Qed.

Theorem find_symbol_not_fresh:
  forall (p: program F V) (id: ident) (b: block),
  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
Proof.
  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
                      (prog_vars p)); intros g m EQ.
  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. 
Qed.

Lemma find_symbol_exists:
  forall (p: program F V)
         (id: ident) (init: list init_data) (v: V),
  In (id, init, v) (prog_vars p) →
  ∃b. find_symbol ? (globalenv p) id = Some ? b.
Proof.
  intros until v.
  assert (forall initm vl, In (id, init, v) vl →
           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
  induction vl; simpl; intros.
  elim H.
  destruct a as [[id0 init0] v0]. 
  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. 
  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. 
  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
Qed.

Remark find_symbol_above_nextfunction:
  forall (id: ident) (b: block) (fns: list (ident * F)),
  let g := add_functs empty fns in
  PTree.get id g.(symbols) = Some ? b →
  b > g.(nextfunction).
Proof.
  induction fns; simpl.
  rewrite PTree.gempty. congruence.
  rewrite PTree.gsspec. case (peq id (fst a)); intro.
  intro EQ. inversion EQ. unfold Zpred. omega.
  intros. generalize (IHfns H). unfold Zpred; omega.
Qed.

Remark find_symbol_add_globals:
  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
  find_symbol ? (fst (add_globals ge_m vars)) id =
  find_symbol ? (fst ge_m) id.
Proof.
  unfold find_symbol; induction vars; simpl; intros.
  auto.
  destruct a as [[id0 init0] var0]. simpl in *.
  caseEq (add_globals ge_m vars); intros ge' m' EQ.
  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. 
  apply IHvars. tauto. intuition congruence.
Qed.

Lemma find_funct_ptr_exists:
  forall (p: program F V) (id: ident) (f: F),
  list_norepet (prog_funct_names p) →
  list_disjoint (prog_funct_names p) (prog_var_names p) →
  In (id, f) (prog_funct p) →
  ∃b. find_symbol ? (globalenv p) id = Some ? b
         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
Proof.
  intros until f.
  assert (forall (fns: list (ident * F)),
           list_norepet (map (@fst ident F) fns) →
           In (id, f) fns →
           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
  unfold find_symbol, find_funct_ptr. induction fns; intros.
  elim H0.
  destruct a as [id0 f0]; simpl in *. inv H. 
  unfold add_funct; simpl.
  rewrite PTree.gsspec. destruct (peq id id0). 
  subst id0. econstructor; split. eauto.
  replace f0 with f. apply ZMap.gss. 
  elim H0; intro. congruence. elim H3. 
  change id with (@fst ident F (id, f)). apply List.in_map. auto.
  exploit IHfns; eauto. elim H0; intro. congruence. auto.
  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
  generalize (find_symbol_above_nextfunction _ _ X).
  unfold block; unfold ZIndexed.t; intro; omega.

  intros. exploit H; eauto. intros [b [X Y]].
  exists b; split.
  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. 
  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. 
  unfold prog_funct_names. change id with (fst (id, f)). 
  apply List.in_map; auto.
  unfold find_funct_ptr. rewrite functions_globalenv. 
  assumption. 
Qed.

Lemma find_funct_ptr_inversion:
  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
  find_funct_ptr ? (globalenv p) b = Some ? f →
  ∃id. In (id, f) (prog_funct p).
Proof.
  intros until f.
  assert (forall fns: list (ident * F),
    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
    ∃id. In (id, f) fns).
  unfold find_funct_ptr. induction fns; simpl.
  rewrite ZMap.gi. congruence.
  destruct a as [id0 f0]; simpl. 
  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
  intro. inv H. exists id0; auto.
  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
Qed.

Lemma find_funct_ptr_prop:
  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
  (forall id f, In (id, f) (prog_funct p) → P f) →
  find_funct_ptr ? (globalenv p) b = Some ? f →
  P f.
Proof.
  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
Qed.

Lemma find_funct_inversion:
  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
  find_funct (globalenv p) v = Some ? f →
  ∃id. In (id, f) (prog_funct p).
Proof.
  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
  rewrite find_funct_find_funct_ptr ? in H. 
  eapply find_funct_ptr_inversion; eauto.
Qed.

Lemma find_funct_prop:
  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
  (forall id f, In (id, f) (prog_funct p) → P f) →
  find_funct (globalenv p) v = Some ? f →
  P f.
Proof.
  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
Qed.

Lemma find_funct_ptr_symbol_inversion:
  forall (p: program F V) (id: ident) (b: block) (f: F),
  find_symbol ? (globalenv p) id = Some ? b →
  find_funct_ptr ? (globalenv p) b = Some ? f →
  In (id, f) p.(prog_funct).
Proof.
  intros until f.
  assert (forall fns,
           let g := add_functs empty fns in
           PTree.get id g.(symbols) = Some ? b →
           ZMap.get b g.(functions) = Some ? f →
           In (id, f) fns).
    induction fns; simpl.
    rewrite ZMap.gi. congruence.
    set (g := add_functs empty fns). 
    rewrite PTree.gsspec. rewrite ZMap.gsspec. 
    case (peq id (fst a)); intro.
    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. 
    intro EQ2. left. destruct a. simpl in *. congruence. 
    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
  assert (forall g0 m0, b < 0 →
          forall vars g m,
          add_globals (g0, m0) vars = (g, m) →
          PTree.get id g.(symbols) = Some ? b →
          PTree.get id g0.(symbols) = Some ? b).
    induction vars; simpl.
    intros. inv H1. auto.
    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). 
    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
    unfold add_symbol; intros A B. rewrite <- B. simpl. 
    rewrite PTree.gsspec. case (peq id id1); intros.
    assert (b > 0). inv H1. apply nextblock_pos. 
    omegaContradiction.
    eauto. 
  intros. 
  generalize (find_funct_ptr_negative _ _ H2). intro.
  pose (g := add_functs empty (prog_funct p)). 
  apply H.  
  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
Qed.

Theorem find_symbol_not_nullptr:
  forall (p: program F V) (id: ident) (b: block),
  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
Proof.
  intros until b.
  assert (forall fns, 
          find_symbol ? (add_functs empty fns) id = Some ? b →
          b <> nullptr).
    unfold find_symbol; induction fns; simpl.
    rewrite PTree.gempty. congruence.
    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
    destruct (peq id id1); intros. 
    inversion H. generalize (nextfunction_add_functs_neg fns).
    unfold block, nullptr; omega.
    auto.
  set (g0 := add_functs empty p.(prog_funct)).
  assert (forall vars g m,
          add_globals (g0, Mem.empty) vars = (g, m) →
          find_symbol ? g id = Some ? b →
          b <> nullptr).
    induction vars; simpl; intros until m.
    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
    destruct a as [[id1 init1] info1]. 
    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. 
    destruct (peq id id1); intros. 
    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
    eauto.
  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
Qed. 

Theorem global_addresses_distinct:
  forall (p: program F V) id1 id2 b1 b2,
  id1<>id2 →
  find_symbol ? (globalenv p) id1 = Some ? b1 →
  find_symbol ? (globalenv p) id2 = Some ? b2 →
  b1<>b2.
Proof.
  intros.
  assert (forall fns,
    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
    b1 <> b2).
  unfold find_symbol. induction fns; simpl; intros.
  rewrite PTree.gempty in H2. discriminate.
  destruct a as [id f]; simpl in *. 
  rewrite PTree.gsspec in H2.
  destruct (peq id1 id). subst id. inv H2.
  rewrite PTree.gso in H3; auto. 
  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
  rewrite PTree.gsspec in H3. 
  destruct (peq id2 id). subst id. inv H3.
  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
  eauto.
  set (ge0 := add_functs empty p.(prog_funct)).
  assert (forall (vars: list (ident * list init_data * V)) ge m,
    add_globals (ge0, Mem.empty) vars = (ge, m) →
    find_symbol ? ge id1 = Some ? b1 →
    find_symbol ? ge id2 = Some ? b2 →
    b1 <> b2).
  unfold find_symbol. induction vars; simpl. 
  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto. 
  intros ge m. destruct a as [[id init] info]. 
  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
  unfold add_symbol. simpl. intros.
  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
  rewrite PTree.gso in H4; auto. 
  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
  eauto.
  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
  fold ge_m. apply surjective_pairing. auto. auto.
Qed.

End GENV.

(* Global environments and program transformations. *)

Section MATCH_PROGRAM.

Variable A B V W: Type.
Variable match_fun: A → B → Prop.
Variable match_var: V → W → Prop.
Variable p: program A V.
Variable p': program B W.
Hypothesis match_prog:
  match_program match_fun match_var p p'.

Lemma add_functs_match:
  forall (fns: list (ident * A)) (tfns: list (ident * B)),
  list_forall2 (match_funct_etry match_fun) fns tfns →
  let r := add_functs (empty A) fns in
  let tr := add_functs (empty B) tfns in
  nextfunction tr = nextfunction r /\
  symbols tr = symbols r /\
  forall (b: block) (f: A),
  ZMap.get b (functions r) = Some ? f →
  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
Proof.
  induction 1; simpl.

  split. reflexivity. split. reflexivity.
  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.

  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. 
  simpl. red in H. destruct H. 
  destruct IHlist_forall2 as [X [Y Z]].
  rewrite X. rewrite Y.  
  split. auto.
  split. congruence.
  intros b f.
  repeat (rewrite ZMap.gsspec). 
  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
  intro EQ; inv EQ. exists fn2; auto.
  auto.
Qed.

Lemma add_functs_rev_match:
  forall (fns: list (ident * A)) (tfns: list (ident * B)),
  list_forall2 (match_funct_etry match_fun) fns tfns →
  let r := add_functs (empty A) fns in
  let tr := add_functs (empty B) tfns in
  nextfunction tr = nextfunction r /\
  symbols tr = symbols r /\
  forall (b: block) (tf: B),
  ZMap.get b (functions tr) = Some ? tf →
  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
Proof.
  induction 1; simpl.

  split. reflexivity. split. reflexivity.
  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.

  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. 
  simpl. red in H. destruct H. 
  destruct IHlist_forall2 as [X [Y Z]].
  rewrite X. rewrite Y.  
  split. auto.
  split. congruence.
  intros b f.
  repeat (rewrite ZMap.gsspec). 
  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
  intro EQ; inv EQ. exists fn1; auto.
  auto.
Qed.

Lemma mem_add_globals_match:
  forall (g1: genv A) (g2: genv B) (m: mem) 
         (vars: list (ident * list init_data * V))
         (tvars: list (ident * list init_data * W)),
  list_forall2 (match_var_etry match_var) vars tvars →
  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
Proof.
  induction 1; simpl.
  auto.
  destruct a1 as [[id1 init1] info1].
  destruct b1 as [[id2 init2] info2].
  red in H. destruct H as [X [Y Z]]. subst id2 init2. 
  generalize IHlist_forall2. 
  destruct (add_globals (g1, m) al).
  destruct (add_globals (g2, m) bl).
  simpl. intro. subst m1. auto.
Qed.

Lemma symbols_add_globals_match:
  forall (g1: genv A) (g2: genv B) (m: mem),
  symbols g1 = symbols g2 →
  forall (vars: list (ident * list init_data * V))
         (tvars: list (ident * list init_data * W)),
  list_forall2 (match_var_etry match_var) vars tvars →
  symbols (fst (add_globals (g1, m) vars)) =
  symbols (fst (add_globals (g2, m) tvars)).
Proof.
  induction 2; simpl.
  auto.
  destruct a1 as [[id1 init1] info1].
  destruct b1 as [[id2 init2] info2].
  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. 
  generalize IHlist_forall2.
  generalize (mem_add_globals_match g1 g2 m H1).
  destruct (add_globals (g1, m) al).
  destruct (add_globals (g2, m) bl).
  simpl. intros. congruence.
Qed.

Theorem find_funct_ptr_match:
  forall (b: block) (f: A),
  find_funct_ptr ? (globalenv p) b = Some ? f →
  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
Proof.
  intros until f. destruct match_prog as [X [Y Z]]. 
  destruct (add_functs_match X) as [P [Q R]]. 
  unfold find_funct_ptr. repeat rewrite functions_globalenv.
  auto.
Qed.

Theorem find_funct_ptr_rev_match:
  forall (b: block) (tf: B),
  find_funct_ptr ? (globalenv p') b = Some ? tf →
  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
Proof.
  intros until tf. destruct match_prog as [X [Y Z]]. 
  destruct (add_functs_rev_match X) as [P [Q R]]. 
  unfold find_funct_ptr. repeat rewrite functions_globalenv.
  auto.
Qed.

Theorem find_funct_match:
  forall (v: val) (f: A),
  find_funct (globalenv p) v = Some ? f →
  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
Proof.
  intros until f. unfold find_funct. 
  case v; try (intros; discriminate).
  intros b ofs.
  case (Int.eq ofs Int.zero); try (intros; discriminate).
  apply find_funct_ptr_match.
Qed.

Theorem find_funct_rev_match:
  forall (v: val) (tf: B),
  find_funct (globalenv p') v = Some ? tf →
  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
Proof.
  intros until tf. unfold find_funct. 
  case v; try (intros; discriminate).
  intros b ofs.
  case (Int.eq ofs Int.zero); try (intros; discriminate).
  apply find_funct_ptr_rev_match.
Qed.

Lemma symbols_init_match:
  symbols (globalenv p') = symbols (globalenv p).
Proof.
  unfold globalenv. unfold globalenv_initmem.
  destruct match_prog as [X [Y Z]].
  destruct (add_functs_match X) as [P [Q R]]. 
  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
Qed.

Theorem find_symbol_match:
  forall (s: ident),
  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
Proof.
  intros. unfold find_symbol. 
  rewrite symbols_init_match. auto.
Qed.

Theorem init_mem_match:
  init_mem p' = init_mem p.
Proof.
  unfold init_mem. unfold globalenv_initmem.
  destruct match_prog as [X [Y Z]]. 
  symmetry. apply mem_add_globals_match. auto.
Qed.

End MATCH_PROGRAM.

Section TRANSF_PROGRAM_PARTIAL2.

Variable A B V W: Type.
Variable transf_fun: A → res B.
Variable transf_var: V → res W.
Variable p: program A V.
Variable p': program B W.
Hypothesis transf_OK:
  transform_partial_program2 transf_fun transf_var p = OK ? p'.

Remark prog_match:
  match_program
    (fun fd tfd => transf_fun fd = OK ? tfd)
    (fun info tinfo => transf_var info = OK ? tinfo)
    p p'.
Proof.
  apply transform_partial_program2_match; auto.
Qed.

Theorem find_funct_ptr_transf_partial2:
  forall (b: block) (f: A),
  find_funct_ptr ? (globalenv p) b = Some ? f →
  ∃f'.
  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
Proof.
  intros. 
  exploit find_funct_ptr_match. eexact prog_match. eauto. 
  intros [tf [X Y]]. exists tf; auto.
Qed.

Theorem find_funct_ptr_rev_transf_partial2:
  forall (b: block) (tf: B),
  find_funct_ptr ? (globalenv p') b = Some ? tf →
  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
Proof.
  intros. 
  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. 
Qed.

Theorem find_funct_transf_partial2:
  forall (v: val) (f: A),
  find_funct (globalenv p) v = Some ? f →
  ∃f'.
  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
Proof.
  intros. 
  exploit find_funct_match. eexact prog_match. eauto. 
  intros [tf [X Y]]. exists tf; auto.
Qed.

Theorem find_funct_rev_transf_partial2:
  forall (v: val) (tf: B),
  find_funct (globalenv p') v = Some ? tf →
  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
Proof.
  intros. 
  exploit find_funct_rev_match. eexact prog_match. eauto. auto. 
Qed.

Theorem find_symbol_transf_partial2:
  forall (s: ident),
  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
Proof.
  intros. eapply find_symbol_match. eexact prog_match.
Qed.

Theorem init_mem_transf_partial2:
  init_mem p' = init_mem p.
Proof.
  intros. eapply init_mem_match. eexact prog_match.
Qed.

End TRANSF_PROGRAM_PARTIAL2.

Section TRANSF_PROGRAM_PARTIAL.

Variable A B V: Type.
Variable transf: A → res B.
Variable p: program A V.
Variable p': program B V.
Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.

Remark transf2_OK:
  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
Proof.
  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
  rewrite map_partial_identity; auto. 
Qed.

Theorem find_funct_ptr_transf_partial:
  forall (b: block) (f: A),
  find_funct_ptr ? (globalenv p) b = Some ? f →
  ∃f'.
  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
Proof.
  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

Theorem find_funct_ptr_rev_transf_partial:
  forall (b: block) (tf: B),
  find_funct_ptr ? (globalenv p') b = Some ? tf →
  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
Proof.
  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

Theorem find_funct_transf_partial:
  forall (v: val) (f: A),
  find_funct (globalenv p) v = Some ? f →
  ∃f'.
  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
Proof.
  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

Theorem find_funct_rev_transf_partial:
  forall (v: val) (tf: B),
  find_funct (globalenv p') v = Some ? tf →
  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
Proof.
  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

Theorem find_symbol_transf_partial:
  forall (s: ident),
  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
Proof.
  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

Theorem init_mem_transf_partial:
  init_mem p' = init_mem p.
Proof.
  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
Qed.

End TRANSF_PROGRAM_PARTIAL.

Section TRANSF_PROGRAM.

Variable A B V: Type.
Variable transf: A → B.
Variable p: program A V.
Let tp := transform_program transf p.

Remark transf_OK:
  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
Proof.
  unfold tp, transform_program, transform_partial_program.
  rewrite map_partial_total. reflexivity.
Qed.

Theorem find_funct_ptr_transf:
  forall (b: block) (f: A),
  find_funct_ptr ? (globalenv p) b = Some ? f →
  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
Proof.
  intros. 
  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
  as [f' [X Y]]. congruence.
Qed.

Theorem find_funct_ptr_rev_transf:
  forall (b: block) (tf: B),
  find_funct_ptr ? (globalenv tp) b = Some ? tf →
  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
Proof.
  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
  intros [f [X Y]]. exists f; split. auto. congruence.
Qed.

Theorem find_funct_transf:
  forall (v: val) (f: A),
  find_funct (globalenv p) v = Some ? f →
  find_funct (globalenv tp) v = Some ? (transf f).
Proof.
  intros. 
  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
  as [f' [X Y]]. congruence.
Qed.

Theorem find_funct_rev_transf:
  forall (v: val) (tf: B),
  find_funct (globalenv tp) v = Some ? tf →
  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
Proof.
  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
  intros [f [X Y]]. exists f; split. auto. congruence.
Qed.

Theorem find_symbol_transf:
  forall (s: ident),
  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
Proof.
  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
Qed.

Theorem init_mem_transf:
  init_mem tp = init_mem p.
Proof.
  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
Qed.

End TRANSF_PROGRAM.

End Genv.
*)