Merge of Andrew Tolmach's HASP-related changes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 782 insertions, 105 deletions

diff --git a/common/AST.v b/common/AST.v
index becf4e4..bcd63a2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -131,11 +131,29 @@ Record program (F V: Type) : Type := mkprogram {
   prog_vars: list (ident * globvar V)
 }.
 
+Definition funct_names (F: Type) (fl: list (ident * F)) : list ident :=
+  map (@fst ident F) fl. 
+
+Lemma funct_names_app : forall (F: Type) (fl1 fl2 : list (ident * F)),
+  funct_names (fl1 ++ fl2) = funct_names fl1 ++ funct_names fl2. 
+Proof.
+  intros; unfold funct_names; apply list_append_map.
+Qed.
+  
+Definition var_names (V: Type) (vl: list (ident * globvar V)) : list ident :=
+  map (@fst ident (globvar V)) vl. 
+
+Lemma var_names_app : forall (V: Type) (vl1 vl2 : list (ident * globvar V)),
+  var_names (vl1 ++ vl2) = var_names vl1 ++ funct_names vl2. 
+Proof.
+  intros; unfold var_names; apply list_append_map.
+Qed.
+  
 Definition prog_funct_names (F V: Type) (p: program F V) : list ident :=
-  map (@fst ident F) p.(prog_funct).
+  funct_names p.(prog_funct).
 
 Definition prog_var_names (F V: Type) (p: program F V) : list ident :=
-  map (@fst ident (globvar V)) p.(prog_vars).
+  var_names p.(prog_vars).
 
 (** * Generic transformations over programs *)
 
@@ -337,12 +355,71 @@ Qed.
 
 End TRANSF_PARTIAL_PROGRAM2.
 
+(** The following is a variant of [transform_partial_program2] where the
+     where the set of functions and global data is augmented, and
+     the main function is potentially changed. *)
+
+Section TRANSF_PARTIAL_AUGMENT_PROGRAM.
+
+Variable A B V W: Type.
+Variable transf_partial_function: A -> res B.
+Variable transf_partial_variable: V -> res W.
+
+Variable new_functs : list (ident * B).
+Variable new_vars : list (ident * globvar W).
+Variable new_main : ident.
+
+Definition transform_partial_augment_program (p: program A V) : res (program B W)  :=
+  do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
+  do vl <- map_partial prefix_name (transf_globvar transf_partial_variable) p.(prog_vars);
+  OK (mkprogram (fl ++ new_functs) new_main (vl ++ new_vars)).
+
+Lemma transform_partial_augment_program_function:
+  forall p tp i tf,
+  transform_partial_augment_program p = OK tp ->
+  In (i, tf) tp.(prog_funct) ->
+  (exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf)
+  \/ In (i,tf) new_functs.
+Proof.
+  intros. monadInv H. simpl in H0.  
+  rewrite in_app in H0.  destruct H0. 
+  left. eapply In_map_partial; eauto.
+  right. auto. 
+Qed.
+
+Lemma transform_partial_augment_program_main:
+  forall p tp,
+  transform_partial_augment_program p = OK tp ->
+  tp.(prog_main) = new_main.
+Proof.
+  intros. monadInv H. reflexivity.
+Qed.
+
+
+Lemma transform_partial_augment_program_variable:
+  forall p tp i tg,
+  transform_partial_augment_program p = OK tp ->
+  In (i, tg) tp.(prog_vars) ->
+  (exists v, In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) /\ transf_partial_variable v = OK tg.(gvar_info))
+  \/ In (i,tg) new_vars.
+Proof.
+  intros. monadInv H. 
+  simpl in H0.  rewrite in_app in H0.  inversion H0. 
+  left. exploit In_map_partial; eauto.  intros [g [P Q]]. 
+  monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. 
+  right. auto.
+Qed.
+
+End TRANSF_PARTIAL_AUGMENT_PROGRAM.
+
+
 (** The following is a relational presentation of 
-  [transform_program_partial2].  Given relations between function
+  [transform_partial_augment_preogram].  Given relations between function
   definitions and between variable information, it defines a relation
-  between programs stating that the two programs have the same shape
-  (same global names, etc) and that identically-named function definitions 
-  are variable information are related. *)
+  between programs stating that the two programs have appropriately related
+  shapes (global names are preserved and possibly augmented, etc) 
+  and that identically-named function definitions
+  and variable information are related. *)
 
 Section MATCH_PROGRAM.
 
@@ -361,37 +438,50 @@ Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop :=
       match_var_entry (id, mkglobvar info1 init ro vo)
                       (id, mkglobvar info2 init ro vo).
 
-Definition match_program (p1: program A V) (p2: program B W) : Prop :=
-  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
-  /\ p1.(prog_main) = p2.(prog_main)
-  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
+Definition match_program (new_functs : list (ident * B))
+                         (new_vars : list (ident * globvar W))
+                         (new_main : ident)
+                         (p1: program A V)  (p2: program B W) : Prop :=
+  (exists tfuncts, list_forall2 match_funct_entry p1.(prog_funct) tfuncts /\
+                                (p2.(prog_funct) = tfuncts ++ new_functs)) /\
+  (exists tvars, list_forall2 match_var_entry p1.(prog_vars) tvars /\
+                                (p2.(prog_vars) = tvars ++ new_vars)) /\
+  p2.(prog_main) = new_main.
 
 End MATCH_PROGRAM.
 
-Remark transform_partial_program2_match:
+Remark transform_partial_augment_program_match:
   forall (A B V W: Type)
          (transf_partial_function: A -> res B)
-         (transf_partial_variable: V -> res W)
-         (p: program A V) (tp: program B W),
-  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
+         (transf_partial_variable : V -> res W)
+         (p: program A V) 
+         (new_functs : list (ident * B))
+         (new_vars : list (ident * globvar W))
+         (new_main : ident)
+         (tp: program B W),
+  transform_partial_augment_program transf_partial_function transf_partial_variable new_functs new_vars new_main p = OK tp ->
   match_program 
     (fun fd tfd => transf_partial_function fd = OK tfd)
     (fun info tinfo => transf_partial_variable info = OK tinfo)
+    new_functs new_vars new_main
     p tp.
 Proof.
-  intros. monadInv H. split.
+  intros. unfold transform_partial_augment_program in H. monadInv H. split.
+  exists x. split. 
   apply list_forall2_imply with
     (fun (ab: ident * A) (ac: ident * B) =>
        fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
   eapply map_partial_forall2. eauto. 
-  intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. constructor. auto.
-  split. auto.
+  intros. destruct v1; destruct v2; simpl in *.
+  destruct H1; subst. constructor. auto. 
+  auto. 
+  split. exists x0.  split.
   apply list_forall2_imply with
     (fun (ab: ident * globvar V) (ac: ident * globvar W) =>
        fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)).
-  eapply map_partial_forall2. eauto. 
+  eapply map_partial_forall2. eauto.
   intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. 
-  monadInv H2. destruct g; simpl in *. constructor. auto.
+  monadInv H2. destruct g; simpl in *.  constructor. auto.  auto.  auto. 
 Qed.
 
 (** * External functions *)
diff --git a/common/Errors.v b/common/Errors.v
index 36e70c5..a70ea6e 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -30,7 +30,8 @@ Set Implicit Arguments.
 
 Inductive errcode: Type :=
   | MSG: string -> errcode
-  | CTX: positive -> errcode.
+  | CTX: positive -> errcode    (* a top-level identifier *)
+  | CTXL: positive -> errcode.  (* an encoded local identifier *)
 
 Definition errmsg: Type := list errcode.
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index a9db51e..367f44a 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -3,6 +3,7 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*   with contributions from Andrew Tolmach (Portland State University)  *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -214,9 +215,22 @@ Qed.
 Definition add_functions (ge: t) (fl: list (ident * F)) : t :=
   List.fold_left add_function fl ge.
 
+Lemma add_functions_app : forall ge fl1 fl2,
+  add_functions ge (fl1 ++ fl2) = add_functions (add_functions ge fl1) fl2.
+Proof. 
+  intros. unfold add_functions. rewrite fold_left_app. auto.
+Qed.
+
+
 Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t :=
   List.fold_left add_variable vl ge.
 
+Lemma add_variables_app : forall ge vl1 vl2 ,
+  add_variables ge (vl1 ++ vl2) = add_variables (add_variables ge vl1) vl2.
+Proof. 
+  intros. unfold add_variables. rewrite fold_left_app. auto.
+Qed.
+
 Definition globalenv (p: program F V) :=
   add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars).
 
@@ -262,9 +276,49 @@ Proof.
   intros. unfold globalenv; eauto. 
 Qed.
 
+
+Remark add_variables_inversion : forall vs e x b,
+  find_symbol (add_variables e vs) x = Some b ->
+  In x (var_names vs) \/ find_symbol e x = Some b. 
+Proof.
+  induction vs; intros. 
+    simpl in H.  intuition.
+    simpl in H. destruct (IHvs _ _ _ H).
+       left. simpl. intuition.
+       destruct a as [y ?]. 
+       unfold add_variable, find_symbol in H0. simpl in H0. 
+       rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
+Qed.
+
+Remark add_functions_inversion : forall fs e x b,
+  find_symbol (add_functions e fs) x = Some b -> 
+  In x (funct_names fs) \/ find_symbol e x = Some b. 
+  induction fs; intros. 
+    simpl in H.  intuition.
+    simpl in H. destruct (IHfs _ _ _ H).
+       left. simpl. intuition.
+       destruct a as [y ?]. 
+       unfold add_variable, find_symbol in H0. simpl in H0. 
+       rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
+Qed.
+
+Lemma find_symbol_inversion : forall p x b,
+  find_symbol (globalenv p) x = Some b ->
+  In x (prog_var_names p ++ prog_funct_names p). 
+Proof.
+ unfold prog_var_names, prog_funct_names, globalenv. 
+ intros.
+ apply in_app.
+ apply add_variables_inversion in H. intuition.
+ apply add_functions_inversion in H0. inversion H0. intuition. 
+ unfold find_symbol in H. 
+ rewrite PTree.gempty in H. inversion H.
+Qed.
+ 
+
 Remark add_functions_same_symb:
   forall id fl ge, 
-  ~In id (map (@fst ident F) fl) ->
+  ~In id (funct_names fl) ->
   find_symbol (add_functions ge fl) id = find_symbol ge id.
 Proof.
   induction fl; simpl; intros. auto. 
@@ -284,7 +338,7 @@ Qed.
 
 Remark add_variables_same_symb:
   forall id vl ge, 
-  ~In id (map (@fst ident (globvar V)) vl) ->
+  ~In id (var_names vl) -> 
   find_symbol (add_variables ge vl) id = find_symbol ge id.
 Proof.
   induction vl; simpl; intros. auto. 
@@ -332,7 +386,7 @@ Theorem find_funct_ptr_exists:
 Proof.
   intros until f.
 
-  assert (forall fl ge, In (id, f) fl -> list_norepet (map (@fst ident F) fl) ->
+  assert (forall fl ge, In (id, f) fl -> list_norepet (funct_names fl) ->
           exists b, find_symbol (add_functions ge fl) id = Some b
                  /\ find_funct_ptr (add_functions ge fl) b = Some f).
   induction fl; simpl; intros. contradiction. inv H0. 
@@ -606,6 +660,15 @@ Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
       end
   end.
 
+Lemma alloc_variables_app : forall vl1 vl2 m m1,
+  alloc_variables m vl1 = Some m1 ->
+  alloc_variables m1 vl2 = alloc_variables m (vl1 ++ vl2).
+Proof.
+  induction vl1.
+    simpl. intros.  inversion H; subst. auto.
+    simpl. intros. destruct (alloc_variable m a); eauto. inversion H.
+Qed.
+
 Remark store_init_data_list_nextblock:
   forall idl b m p m',
   store_init_data_list m b p idl = Some m' ->
@@ -629,6 +692,28 @@ Proof.
   congruence.
 Qed.
 
+Remark alloc_variable_nextblock:
+  forall v m m',
+  alloc_variable m v = Some m' ->
+  Mem.nextblock m' = Zsucc(Mem.nextblock m).
+Proof.
+  unfold alloc_variable.
+  intros until m'.   
+  set (init := gvar_init v#2).
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
+  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar v#2)); try congruence. intros m4 DROP REC. 
+  inv REC; subst.
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
+  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  rewrite (store_zeros_nextblock _ _ _ STZ). 
+  rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). 
+  auto.
+Qed.
+
+
 Remark alloc_variables_nextblock:
   forall vl m m',
   alloc_variables m vl = Some m' ->
@@ -897,6 +982,17 @@ Proof.
   red. rewrite H1. rewrite <- H3. intuition.
 Qed.
 
+Lemma init_mem_genv_vars : forall p m,
+    init_mem p = Some m -> 
+    genv_nextvar (globalenv p) = Mem.nextblock m.
+Proof.
+    clear. unfold globalenv, init_mem.  intros.
+    exploit alloc_variables_nextblock; eauto.
+    simpl (Mem.nextblock Mem.empty). 
+    rewrite add_variables_nextvar.  rewrite add_functions_nextvar.
+    simpl (genv_nextvar empty_genv).  auto.
+Qed.
+
 Theorem find_var_info_not_fresh:
   forall p b gv m,
   init_mem p = Some m ->
@@ -1028,6 +1124,102 @@ Proof.
   omega.
 Qed.
 
+Section INITMEM_AUGMENT_INJ. 
+
+Variable ge: t.
+Variable thr: block.
+
+Lemma store_init_data_augment: 
+  forall m1 m2 b p id m2', 
+  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
+  b >= thr -> 
+  store_init_data ge m2 b p id = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof. 
+  intros until m2'. intros INJ BND ST. 
+  assert (P: forall chunk ofs v m2', 
+             Mem.store chunk m2 b ofs v = Some m2' -> 
+             Mem.inject (Mem.flat_inj thr) m1 m2'). 
+    intros. eapply Mem.store_outside_inject; eauto. 
+        intros b' ? INJ'. unfold Mem.flat_inj in INJ'. 
+         destruct (zlt b' thr); inversion INJ'; subst. omega. 
+  destruct id; simpl in ST; try (eapply P; eauto; fail).
+  inv ST; auto. 
+  revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. 
+Qed.
+
+Lemma store_init_data_list_augment:
+  forall b idl m1 m2 p m2', 
+  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
+  b >= thr -> 
+  store_init_data_list ge m2 b p idl = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof. 
+  induction idl; simpl.
+  intros; congruence.
+  intros until m2'; intros INJ FB.
+  caseEq (store_init_data ge m2 b p a); try congruence. intros. 
+  eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. 
+Qed.
+
+Lemma store_zeros_augment:
+  forall m1 m2 b n m2',
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  b >= thr ->
+  store_zeros m2 b n = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof.
+  intros until n. functional induction (store_zeros m2 b n); intros.
+  inv H1; auto.
+  apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. 
+  intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). 
+    inversion H2; subst; omega.  
+    discriminate.
+  inv H1.
+Qed.
+
+Lemma alloc_variable_augment:
+  forall id m1 m2 m2',
+  alloc_variable ge m2 id = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
+  Mem.nextblock m2 >= thr -> 
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof.
+  intros until m2'. unfold alloc_variable. 
+  set (sz := init_data_list_size (gvar_init id#2)).
+  caseEq (Mem.alloc m2 0 sz); try congruence. intros m3 b ALLOC.
+  caseEq (store_zeros m3 b sz); try congruence. intros m4 STZ.
+  caseEq (store_init_data_list ge m4 b 0 (gvar_init id#2)); try congruence.
+  intros m5 STORE DROP INJ NEXT.
+  assert (b >= thr). 
+     pose proof (Mem.fresh_block_alloc _ _ _ _ _ ALLOC).  
+     unfold Mem.valid_block in H.  unfold block in *; omega. 
+  eapply Mem.drop_outside_inject. 2: eauto.  
+  eapply store_init_data_list_augment. 2: eauto. 2: eauto. 
+  eapply store_zeros_augment. 2: eauto. 2: eauto.
+  eapply Mem.alloc_right_inject; eauto. 
+  intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0. 
+     subst; exfalso; omega.
+Qed.
+
+Lemma alloc_variables_augment:
+  forall idl m1 m2 m2',
+  alloc_variables ge m2 idl = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  Mem.nextblock m2 >= thr ->
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof.
+  induction idl; simpl.
+  intros. congruence.
+  intros until m2'. caseEq (alloc_variable ge m2 a); try congruence. intros.
+  eapply IHidl with (m2 := m); eauto.  
+    eapply alloc_variable_augment; eauto. 
+    rewrite (alloc_variable_nextblock _ _ _ H). 
+    unfold block in *; omega. 
+Qed.
+
+End INITMEM_AUGMENT_INJ. 
+
 End GENV.
 
 (** * Commutation with program transformations *)
@@ -1045,48 +1237,65 @@ Inductive match_globvar: globvar V -> globvar W -> Prop :=
       match_varinfo info1 info2 ->
       match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo).
 
-Record match_genvs (ge1: t A V) (ge2: t B W): Prop := {
-  mge_nextfun: genv_nextfun ge1 = genv_nextfun ge2;
-  mge_nextvar: genv_nextvar ge1 = genv_nextvar ge2;
-  mge_symb:    genv_symb ge1 = genv_symb ge2;
+Record match_genvs (new_functs : list (ident * B)) (new_vars : list (ident * globvar W)) 
+                   (ge1: t A V) (ge2: t B W): Prop := {
+  mge_nextfun: genv_nextfun ge2 = genv_nextfun ge1 - Z_of_nat(length new_functs);
+  mge_nextvar: genv_nextvar ge2 = genv_nextvar ge1 + Z_of_nat(length new_vars);
+  mge_symb:    forall id,  ~ In id ((funct_names new_functs) ++ (var_names new_vars)) -> 
+                   PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
   mge_funs:
     forall b f, ZMap.get b (genv_funs ge1) = Some f ->
     exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
   mge_rev_funs:
     forall b tf, ZMap.get b (genv_funs ge2) = Some tf ->
-    exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf;
+    if zlt (genv_nextfun ge1) b then 
+      exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf
+    else 
+      In tf (map (@snd ident B) new_functs);
   mge_vars:
     forall b v, ZMap.get b (genv_vars ge1) = Some v ->
     exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
   mge_rev_vars:
     forall b tv, ZMap.get b (genv_vars ge2) = Some tv ->
-    exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
+    if zlt b (genv_nextvar ge1) then
+      exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
+    else
+      In tv (map (@snd ident (globvar W)) new_vars)
 }.
 
 Lemma add_function_match:
   forall ge1 ge2 id f1 f2,
-  match_genvs ge1 ge2 ->
+  match_genvs nil nil ge1 ge2 ->
   match_fun f1 f2 ->
-  match_genvs (add_function ge1 (id, f1)) (add_function ge2 (id, f2)).
-Proof.
-  intros. destruct H. constructor; simpl. 
-  congruence. congruence. congruence.
-  rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-  destruct (ZIndexed.eq b (genv_nextfun ge2)). 
-  exists f2; split; congruence.
-  eauto.
+  match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)).
+Proof.
+  intros. destruct H. 
+     simpl in mge_nextfun0. rewrite Zminus_0_r in mge_nextfun0. 
+     simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. 
+  constructor; simpl. 
+  rewrite Zminus_0_r. congruence.
+  rewrite Zplus_0_r. congruence.
+  intros. rewrite mge_nextfun0. 
+    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
+    rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
+    destruct (ZIndexed.eq b (genv_nextfun ge1)). 
+     exists f2; split; congruence.
+     eauto.
   rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-  destruct (ZIndexed.eq b (genv_nextfun ge2)). 
-  exists f1; split; congruence.
-  eauto.
+   destruct (ZIndexed.eq b (genv_nextfun ge1)). 
+    subst b. destruct (zlt (genv_nextfun ge1 - 1) (genv_nextfun ge1)). 
+      exists f1; split; congruence. omega. 
+    pose proof (mge_rev_funs0 b tf H). 
+    destruct (zlt (genv_nextfun ge1) b); 
+      destruct (zlt (genv_nextfun ge1 - 1) b).  auto. omega. exfalso; omega. intuition.
   auto.
   auto.
 Qed.
 
 Lemma add_functions_match:
   forall fl1 fl2, list_forall2 (match_funct_entry match_fun) fl1 fl2 ->
-  forall ge1 ge2, match_genvs ge1 ge2 ->
-  match_genvs (add_functions ge1 fl1) (add_functions ge2 fl2).
+  forall ge1 ge2, match_genvs nil nil ge1 ge2 ->
+  match_genvs nil nil (add_functions ge1 fl1) (add_functions ge2 fl2).
 Proof.
   induction 1; intros; simpl. 
   auto.
@@ -1094,46 +1303,151 @@ Proof.
   destruct H. subst. apply IHlist_forall2. apply add_function_match; auto.
 Qed.
 
-Lemma add_variable_match:
-  forall ge1 ge2 id v1 v2,
-  match_genvs ge1 ge2 ->
-  match_globvar v1 v2 ->
-  match_genvs (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)).
+Lemma add_function_augment_match: 
+  forall new_functs new_vars ge1 ge2 id f2,
+  match_genvs new_functs new_vars ge1 ge2 ->
+  match_genvs (new_functs++((id,f2)::nil)) new_vars ge1 (add_function ge2 (id, f2)).
 Proof.
   intros. destruct H. constructor; simpl. 
-  congruence. congruence. congruence.
+  rewrite mge_nextfun0. rewrite app_length. 
+       simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
+  auto.
+  intros. unfold funct_names in H. rewrite map_app in H. rewrite in_app in H.  rewrite in_app in H. simpl in H. 
+     destruct (peq id id0). subst. intuition. rewrite PTree.gso. 
+     apply mge_symb0. intro.  apply H. rewrite in_app in H0. inversion H0; intuition. intuition. 
+  intros. rewrite ZMap.gso. auto. 
+     rewrite mge_nextfun0. pose proof (genv_funs_range ge1 b H). intro; subst; omega.
+  intros. rewrite ZMap.gsspec in H. 
+     destruct (ZIndexed.eq b (genv_nextfun ge2)). 
+       destruct (zlt (genv_nextfun ge1) b). 
+          exfalso.  rewrite mge_nextfun0 in e.  unfold block; omega. 
+          rewrite map_app. rewrite in_app.  simpl.  inversion H; intuition.
+       pose proof (mge_rev_funs0 b tf H). 
+          destruct (zlt (genv_nextfun ge1) b). 
+            auto.
+            rewrite map_app. rewrite in_app. intuition. 
+  auto.
+  auto.
+Qed.
+
+
+Lemma add_functions_augment_match:
+  forall fl new_functs new_vars ge1 ge2, 
+    match_genvs new_functs new_vars ge1 ge2 ->
+    match_genvs (new_functs++fl) new_vars ge1 (add_functions ge2 fl).
+Proof.
+  induction fl; simpl. 
+    intros. rewrite app_nil_r. auto. 
+    intros. replace (new_functs ++ a :: fl) with ((new_functs ++ (a::nil)) ++ fl) 
+       by (rewrite app_ass; auto). 
+     apply IHfl. destruct a. apply add_function_augment_match. auto.
+Qed.
+
+
+Lemma add_variable_match:
+  forall new_functs ge1 ge2 id v1 v2,
+  match_genvs new_functs nil ge1 ge2 ->
+  match_globvar v1 v2 ->
+  match_genvs new_functs nil (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)).
+Proof.
+  intros. destruct H. 
+     simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. 
+  constructor; simpl. 
+  auto. 
+    rewrite Zplus_0_r. rewrite mge_nextvar0. auto. 
+  intros. rewrite mge_nextvar0. 
+    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
   auto.
   auto.
   rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-  destruct (ZIndexed.eq b (genv_nextvar ge2)). 
-  exists v2; split; congruence.
-  eauto.
+    destruct (ZIndexed.eq b (genv_nextvar ge1)). 
+     exists v2; split; congruence.
+     eauto.
   rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-  destruct (ZIndexed.eq b (genv_nextvar ge2)). 
-  exists v1; split; congruence.
-  eauto.
+   destruct (ZIndexed.eq b (genv_nextvar ge1)). 
+    subst b. inversion H; subst. 
+      destruct (zlt (genv_nextvar ge1) (genv_nextvar ge1 + 1)). 
+        exists v1; split; congruence. omega. 
+      pose proof (mge_rev_vars0 _ _ H).
+        destruct (zlt b (genv_nextvar ge1));
+          destruct (zlt b (genv_nextvar ge1 + 1)).  auto. omega. exfalso; omega. intuition.
 Qed.
 
 Lemma add_variables_match:
   forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
-  forall ge1 ge2, match_genvs ge1 ge2 ->
-  match_genvs (add_variables ge1 vl1) (add_variables ge2 vl2).
+  forall new_functs ge1 ge2, match_genvs new_functs nil ge1 ge2 ->
+  match_genvs new_functs nil (add_variables ge1 vl1) (add_variables ge2 vl2).
 Proof.
   induction 1; intros; simpl. 
   auto.
   inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto.
 Qed.
 
+
+Lemma add_variable_augment_match:
+  forall ge1 new_functs new_vars ge2 id v2,
+  match_genvs new_functs new_vars ge1 ge2 ->
+  match_genvs new_functs (new_vars++((id,v2)::nil)) ge1 (add_variable ge2 (id, v2)).
+Proof.
+  intros. destruct H. constructor; simpl. 
+  auto.
+  rewrite mge_nextvar0. rewrite app_length. 
+       simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
+  intros. unfold funct_names, var_names in H. rewrite map_app in H. rewrite in_app in H.  rewrite in_app in H. simpl in H. 
+     destruct (peq id id0). subst. intuition. rewrite PTree.gso. 
+     apply mge_symb0. intro.  apply H. rewrite in_app in H0. inversion H0; intuition. intuition. 
+  auto.
+  auto.
+  intros. rewrite ZMap.gso. auto. 
+     rewrite mge_nextvar0. pose proof (genv_vars_range ge1 b H). intro; subst; omega.
+  intros. rewrite ZMap.gsspec in H. 
+     destruct (ZIndexed.eq b (genv_nextvar ge2)). 
+       destruct (zlt b (genv_nextvar ge1)). 
+          exfalso.  rewrite mge_nextvar0 in e.  unfold block; omega. 
+          rewrite map_app. rewrite in_app.  simpl.  inversion H; intuition.
+       pose proof (mge_rev_vars0 b tv H). 
+          destruct (zlt b (genv_nextvar ge1)). 
+            auto.
+            rewrite map_app. rewrite in_app. intuition. 
+
+Qed.
+
+Lemma add_variables_augment_match:
+  forall vl ge1 new_functs new_vars ge2, 
+    match_genvs new_functs new_vars ge1 ge2 ->
+    match_genvs new_functs (new_vars++vl) ge1  (add_variables ge2 vl).
+Proof.
+  induction vl; simpl. 
+    intros. rewrite app_nil_r. auto. 
+    intros. replace (new_vars ++ a :: vl) with ((new_vars ++ (a::nil)) ++ vl) 
+       by (rewrite app_ass; auto). 
+     apply IHvl. destruct a. apply add_variable_augment_match. auto.
+Qed.
+
+Variable new_functs : list (ident * B).
+Variable new_vars : list (ident * globvar W).
+Variable new_main : ident.
+
 Variable p: program A V.
 Variable p': program B W.
-Hypothesis progmatch: match_program match_fun match_varinfo p p'.
+Hypothesis progmatch: 
+  match_program match_fun match_varinfo new_functs new_vars new_main p p'.
 
 Lemma globalenvs_match:
-  match_genvs (globalenv p) (globalenv p').
-Proof.
-  unfold globalenv. destruct progmatch. destruct H0. 
-  apply add_variables_match; auto. apply add_functions_match; auto. 
-  constructor; simpl; auto; intros; rewrite ZMap.gi in H2; congruence.
+  match_genvs new_functs new_vars (globalenv p) (globalenv p').
+Proof.
+  unfold globalenv. destruct progmatch. clear progmatch.
+  destruct H as [tfuncts [P1 P2]]. destruct H0.  clear H0. destruct H as [tvars [Q1 Q2]]. 
+  rewrite P2.  rewrite Q2. clear P2 Q2.
+  rewrite add_variables_app. 
+  rewrite add_functions_app. 
+  pattern new_vars at 1. replace new_vars with (nil++new_vars) by auto.
+  apply add_variables_augment_match.
+  apply add_variables_match; auto. 
+  pattern new_functs at 1. replace new_functs with (nil++new_functs) by auto. 
+  apply add_functions_augment_match.
+  apply add_functions_match; auto. 
+  constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence.
 Qed.
 
 Theorem find_funct_ptr_match:
@@ -1146,8 +1460,10 @@ Proof (mge_funs globalenvs_match).
 Theorem find_funct_ptr_rev_match:
   forall (b : block) (tf : B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  exists f : A,
-  find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.
+  if zlt (genv_nextfun (globalenv p)) b then 
+      exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
+  else 
+      In tf (map (@snd ident B) new_functs).
 Proof (mge_rev_funs globalenvs_match).
 
 Theorem find_funct_match:
@@ -1161,15 +1477,17 @@ Proof.
   apply find_funct_ptr_match. auto.
 Qed.
 
-Theorem find_funct_rev_match:
+Theorem find_funct_rev_match: (* a little weak *)
   forall (v : val) (tf : B),
   find_funct (globalenv p') v = Some tf ->
-  exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf.
+  (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) 
+  \/ (In tf (map (@snd ident B) new_functs)).
 Proof.
   intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. 
   rewrite find_funct_find_funct_ptr in H. 
   rewrite find_funct_find_funct_ptr.
-  apply find_funct_ptr_rev_match. auto.
+  apply find_funct_ptr_rev_match in H. 
+   destruct (zlt (genv_nextfun (globalenv p)) b); intuition. 
 Qed.
 
 Theorem find_var_info_match:
@@ -1182,78 +1500,104 @@ Proof (mge_vars globalenvs_match).
 Theorem find_var_info_rev_match:
   forall (b : block) (tv : globvar W),
   find_var_info (globalenv p') b = Some tv ->
-  exists v,
-  find_var_info (globalenv p) b = Some v /\ match_globvar v tv.
+  if zlt b (genv_nextvar (globalenv p)) then 
+    exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
+  else
+    In tv (map (@snd ident (globvar W)) new_vars).  
 Proof (mge_rev_vars globalenvs_match).
 
 Theorem find_symbol_match:
   forall (s : ident),
+  ~In s (funct_names new_functs ++ var_names new_vars) -> 
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
-  intros. destruct globalenvs_match. unfold find_symbol. congruence. 
+  intros. destruct globalenvs_match. unfold find_symbol.  auto. 
 Qed.
 
+Hypothesis new_ids_fresh : 
+  (forall s', find_symbol (globalenv p) s' <> None  -> 
+             ~In s' (funct_names new_functs ++ var_names new_vars)).
+
 Lemma store_init_data_list_match:
-  forall idl m b ofs,
-  store_init_data_list (globalenv p') m b ofs idl =
-  store_init_data_list (globalenv p) m b ofs idl.
+  forall idl m b ofs m',
+  store_init_data_list (globalenv p) m b ofs idl = Some m' ->
+  store_init_data_list (globalenv p') m b ofs idl = Some m'.
 Proof.
   induction idl; simpl; intros. 
   auto.
-  assert (store_init_data (globalenv p') m b ofs a =
-          store_init_data (globalenv p) m b ofs a).
-  destruct a; simpl; auto. rewrite find_symbol_match. auto. 
-  rewrite H. destruct (store_init_data (globalenv p) m b ofs a); auto. 
+  assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' ->
+          store_init_data (globalenv p') m b ofs a = Some m').
+   destruct a; simpl; auto. rewrite find_symbol_match. auto. 
+     inversion H.  case_eq (find_symbol (globalenv p) i). 
+       intros. apply new_ids_fresh. intro. rewrite H0 in H2; inversion H2. 
+       intro. rewrite H0 in H1. inversion H1. 
+  case_eq (store_init_data (globalenv p) m b ofs a); intros. 
+    rewrite H1 in H. 
+    pose proof (H0 _ H1). rewrite H2. auto. 
+    rewrite H1 in H. inversion H. 
 Qed.
 
 Lemma alloc_variables_match:
   forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
-  forall m,
-  alloc_variables (globalenv p') m vl2 = alloc_variables (globalenv p) m vl1.
+  forall m m',
+  alloc_variables (globalenv p) m vl1 = Some m' -> 
+  alloc_variables (globalenv p') m vl2 = Some m'.
 Proof.
-  induction 1; intros; simpl.
+  induction 1; intros until m'; simpl.
   auto.
   inv H. 
   unfold alloc_variable; simpl. 
   destruct (Mem.alloc m 0 (init_data_list_size init)). 
-  destruct (store_zeros m0 b (init_data_list_size init)); auto.
-  rewrite store_init_data_list_match. 
-  destruct (store_init_data_list (globalenv p) m1 b 0 init); auto.
+  destruct (store_zeros m0 b (init_data_list_size init)); auto. 
+  case_eq (store_init_data_list (globalenv p) m1 b 0 init); intros m2 P. 
+  rewrite (store_init_data_list_match _ _ _ _ P). 
   change (perm_globvar (mkglobvar info2 init ro vo))
     with (perm_globvar (mkglobvar info1 init ro vo)).
   destruct (Mem.drop_perm m2 b 0 (init_data_list_size init)
-    (perm_globvar (mkglobvar info1 init ro vo))); auto.
+    (perm_globvar (mkglobvar info1 init ro vo))); auto. 
+  inversion P. 
 Qed.
 
 Theorem init_mem_match:
-  forall m, init_mem p = Some m -> init_mem p' = Some m.
+  forall m, init_mem p = Some m -> 
+  init_mem p' = alloc_variables (globalenv p') m new_vars.
 Proof.
-  intros. rewrite <- H. unfold init_mem. destruct progmatch. destruct H1. 
-  apply alloc_variables_match; auto. 
+  unfold init_mem. destruct progmatch. destruct H0.  destruct H0 as [tvars [P1 P2]].
+  rewrite P2. 
+  intros. 
+  erewrite <- alloc_variables_app; eauto. 
+  eapply alloc_variables_match; eauto. 
 Qed.
 
 End MATCH_PROGRAMS.
 
-Section TRANSF_PROGRAM_PARTIAL2.
+Section TRANSF_PROGRAM_AUGMENT.
 
 Variable A B V W: Type.
 Variable transf_fun: A -> res B.
 Variable transf_var: V -> res W.
+
+Variable new_functs : list (ident * B).
+Variable new_vars : list (ident * globvar W).
+Variable new_main : ident.
+
 Variable p: program A V.
 Variable p': program B W.
+
 Hypothesis transf_OK:
-  transform_partial_program2 transf_fun transf_var p = OK p'.
+  transform_partial_augment_program transf_fun transf_var new_functs new_vars new_main p = OK p'.
 
 Remark prog_match:
   match_program
     (fun fd tfd => transf_fun fd = OK tfd)
     (fun info tinfo => transf_var info = OK tinfo)
+    new_functs new_vars new_main
     p p'.
 Proof.
-  apply transform_partial_program2_match; auto.
+  apply transform_partial_augment_program_match; auto.
 Qed.
 
-Theorem find_funct_ptr_transf_partial2:
+Theorem find_funct_ptr_transf_augment:
   forall (b: block) (f: A),
   find_funct_ptr (globalenv p) b = Some f ->
   exists f',
@@ -1264,16 +1608,52 @@ Proof.
   intros [tf [X Y]]. exists tf; auto.
 Qed.
 
-Theorem find_funct_ptr_rev_transf_partial2:
+
+
+(* This may not yet be in the ideal form for easy use .*)
+Theorem find_new_funct_ptr_exists: 
+  list_norepet (prog_funct_names p ++ funct_names new_functs) ->
+  list_disjoint (prog_funct_names p ++ funct_names new_functs)  (prog_var_names p ++ var_names new_vars) ->
+  forall id f, In (id, f) new_functs -> 
+  exists b, find_symbol (globalenv p') id = Some b
+         /\ find_funct_ptr (globalenv p') b = Some f.
+Proof.
+  intros. 
+  destruct p. 
+  unfold transform_partial_augment_program in transf_OK. 
+  monadInv transf_OK. rename x into prog_funct'.  rename x0 into prog_vars'. simpl in *.
+  assert (funct_names prog_funct = funct_names prog_funct').
+   clear - EQ.  generalize dependent prog_funct'. induction prog_funct; intros.
+      simpl in EQ. inversion EQ; subst; auto.
+      simpl in EQ. destruct a. destruct (transf_fun a); try discriminate. monadInv EQ.
+      simpl; f_equal; auto.
+  assert (var_names prog_vars = var_names prog_vars').
+   clear - EQ1.  generalize dependent prog_vars'. induction prog_vars; intros.
+      simpl in EQ1. inversion EQ1; subst; auto.
+      simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1.
+      simpl; f_equal; auto.
+  apply find_funct_ptr_exists. 
+  unfold prog_funct_names in *; simpl in *. 
+  rewrite funct_names_app. rewrite <- H2. auto.
+  unfold prog_funct_names, prog_var_names in *; simpl in *.  
+  rewrite funct_names_app. rewrite var_names_app. rewrite <- H2. rewrite <- H3.  auto.
+  simpl. intuition.
+Qed.
+
+Theorem find_funct_ptr_rev_transf_augment:
   forall (b: block) (tf: B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
+  if (zlt (genv_nextfun (globalenv p)) b) then
+   (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
+  else 
+   In tf (map (@snd ident B) new_functs).
 Proof.
   intros. 
-  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. 
+  exploit find_funct_ptr_rev_match;eauto. eexact prog_match; eauto. auto. 
 Qed.
 
-Theorem find_funct_transf_partial2:
+
+Theorem find_funct_transf_augment:
   forall (v: val) (f: A),
   find_funct (globalenv p) v = Some f ->
   exists f',
@@ -1284,16 +1664,17 @@ Proof.
   intros [tf [X Y]]. exists tf; auto.
 Qed.
 
-Theorem find_funct_rev_transf_partial2:
+Theorem find_funct_rev_transf_augment: 
   forall (v: val) (tf: B),
   find_funct (globalenv p') v = Some tf ->
-  exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
+  (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/
+  In tf (map (@snd ident B) new_functs). 
 Proof.
   intros. 
   exploit find_funct_rev_match. eexact prog_match. eauto. auto. 
 Qed.
 
-Theorem find_var_info_transf_partial2:
+Theorem find_var_info_transf_augment:
   forall (b: block) (v: globvar V),
   find_var_info (globalenv p) b = Some v ->
   exists v',
@@ -1305,29 +1686,172 @@ Proof.
   rewrite H0; simpl. auto.
 Qed.
 
+
+(* This may not yet be in the ideal form for easy use .*)
+Theorem find_new_var_exists: 
+  list_norepet (prog_var_names p ++ var_names new_vars) -> 
+  forall id gv m, In (id, gv) new_vars -> 
+  init_mem p' = Some m -> 
+  exists b, find_symbol (globalenv p') id = Some b
+         /\ find_var_info (globalenv p') b = Some gv
+         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
+         /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p') m b 0 gv.(gvar_init)).
+Proof.
+  intros. 
+  destruct p. 
+  unfold transform_partial_augment_program in transf_OK. 
+  monadInv transf_OK. rename x into prog_funct'.  rename x0 into prog_vars'. simpl in *.
+  assert (var_names prog_vars = var_names prog_vars').
+   clear - EQ1.  generalize dependent prog_vars'. induction prog_vars; intros.
+      simpl in EQ1. inversion EQ1; subst; auto.
+      simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1.
+      simpl; f_equal; auto.
+  apply find_var_exists. 
+  unfold prog_var_names in *; simpl in *.  
+  rewrite var_names_app. rewrite <- H2. auto.
+  simpl. intuition.
+  auto.
+Qed.
+
+Theorem find_var_info_rev_transf_augment:
+  forall (b: block) (v': globvar W),
+  find_var_info (globalenv p') b = Some v' ->
+  if zlt b (genv_nextvar (globalenv p)) then
+    (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v')
+  else
+    (In v' (map (@snd ident (globvar W)) new_vars)).
+Proof.
+  intros. 
+  exploit find_var_info_rev_match. eexact prog_match. eauto.
+  destruct (zlt b (genv_nextvar (globalenv p))); auto.
+  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. 
+  rewrite H0; simpl. auto.
+Qed.
+
+Theorem find_symbol_transf_augment:  
+  forall (s: ident), 
+  ~ In s (funct_names new_functs ++ var_names new_vars) -> 
+  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+Proof.
+  intros. eapply find_symbol_match. eexact prog_match. auto.
+Qed.
+
+Theorem init_mem_transf_augment: 
+   (forall s', find_symbol (globalenv p) s' <> None -> 
+     ~ In s' (funct_names new_functs ++ var_names new_vars)) -> 
+   forall m, init_mem p = Some m -> 
+   init_mem p' = alloc_variables (globalenv p') m new_vars.
+Proof.
+  intros. eapply init_mem_match. eexact prog_match. auto. auto.
+Qed.
+ 
+Theorem init_mem_inject_transf_augment:
+   (forall s', find_symbol (globalenv p) s' <> None -> 
+     ~ In s' (funct_names new_functs ++ var_names new_vars)) -> 
+  forall m, init_mem p = Some m ->
+  forall m', init_mem p' = Some m' -> 
+  Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'.
+Proof.
+  intros. 
+  pose proof (initmem_inject p H0). 
+  erewrite init_mem_transf_augment in H1; eauto. 
+  eapply alloc_variables_augment; eauto. omega.
+Qed.
+
+
+End TRANSF_PROGRAM_AUGMENT.
+
+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 transf_augment_OK:
+  transform_partial_augment_program transf_fun transf_var nil nil p.(prog_main) p = OK p'.
+Proof.
+  rewrite <- transf_OK. 
+  unfold transform_partial_augment_program, transform_partial_program2. 
+  destruct (map_partial prefix_name transf_fun (prog_funct p)); auto. simpl. 
+  destruct (map_partial prefix_name (transf_globvar transf_var) (prog_vars p)); simpl. 
+  repeat rewrite app_nil_r. auto. auto.
+Qed.
+
+Theorem find_funct_ptr_transf_partial2:
+  forall (b: block) (f: A),
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists f',
+  find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
+Proof.
+  exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+Qed.
+
+Theorem find_funct_ptr_rev_transf_partial2:
+  forall (b: block) (tf: B),
+  find_funct_ptr (globalenv p') b = Some tf ->
+  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
+Proof.
+  pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  intros.  pose proof (H b tf H0). 
+  destruct (zlt (genv_nextfun (globalenv p)) b).  auto. inversion H1. 
+Qed.
+
+Theorem find_funct_transf_partial2:
+  forall (v: val) (f: A),
+  find_funct (globalenv p) v = Some f ->
+  exists f',
+  find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
+Proof.
+  exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+Qed.
+
+Theorem find_funct_rev_transf_partial2:
+  forall (v: val) (tf: B),
+  find_funct (globalenv p') v = Some tf ->
+  exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
+Proof.
+  pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  intros. pose proof (H v tf H0). 
+  destruct H1. auto. inversion H1. 
+Qed.
+
+Theorem find_var_info_transf_partial2:
+  forall (b: block) (v: globvar V),
+  find_var_info (globalenv p) b = Some v ->
+  exists v',
+  find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
+Proof.
+  exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+Qed.
+
 Theorem find_var_info_rev_transf_partial2:
   forall (b: block) (v': globvar W),
   find_var_info (globalenv p') b = Some v' ->
   exists v,
   find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'.
 Proof.
-  intros. 
-  exploit find_var_info_rev_match. eexact prog_match. eauto. 
-  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl.
-  rewrite H0; simpl. auto.
+  pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  intros.  pose proof (H b v' H0). 
+  destruct (zlt b (genv_nextvar (globalenv p))).  auto. inversion H1. 
 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.
+  pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  auto.
 Qed.
 
 Theorem init_mem_transf_partial2:
   forall m, init_mem p = Some m -> init_mem p' = Some m.
 Proof.
-  intros. eapply init_mem_match. eexact prog_match. auto.
+  pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  intros. simpl in H. apply H; auto.  
 Qed.
 
 End TRANSF_PROGRAM_PARTIAL2.
diff --git a/common/Memory.v b/common/Memory.v
index e1c68bd..059a27e 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -2817,6 +2817,41 @@ Proof.
   auto.
 Qed.
 
+Lemma drop_outside_inj: forall f m1 m2 b lo hi p m2',
+  mem_inj f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  mem_inj f m1 m2'.
+Proof. 
+  intros. destruct H. constructor; intros.
+
+  (* access *)
+  inversion H2.
+  destruct (range_perm_in_bounds _ _ _ _ _ H3). 
+    pose proof (size_chunk_pos chunk). omega.
+  pose proof (mi_access0 b1 b2 delta chunk ofs p0 H H2). clear mi_access0 H2 H3. 
+  unfold valid_access in *.  intuition. clear H3. 
+  unfold range_perm in *. intros. 
+  eapply perm_drop_3; eauto.  
+  destruct (eq_block b2 b); subst; try (intuition; fail).  
+    destruct (H1 b1 delta H); intuition omega. 
+
+  (* memval *)
+  pose proof (mi_memval0 _ _ _ _  H H2). clear mi_memval0. 
+  unfold Mem.drop_perm in H0. 
+  destruct (Mem.range_perm_dec m2 b lo hi p); inversion H0; subst; clear H0. 
+  simpl.  unfold update.  destruct (zeq b2 b); subst; auto. 
+    pose proof (perm_in_bounds _ _ _ _ H2). 
+    destruct (H1 b1 delta H). 
+       destruct (zle lo (ofs + delta)); simpl; auto. exfalso; omega. 
+       destruct (zle lo (ofs + delta)); destruct (zlt (ofs + delta) hi); simpl; auto. 
+           exfalso; omega. 
+Qed.
+
+
 (** * Memory extensions *)
 
 (**  A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
@@ -3868,6 +3903,23 @@ Proof.
 Qed.
 *)
 
+Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2',
+  inject f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  inject f m1 m2'.
+Proof.
+  intros. destruct H. constructor; eauto.
+  eapply drop_outside_inj; eauto.
+
+  intros.  unfold valid_block in *. erewrite nextblock_drop; eauto. 
+
+  intros.  erewrite bounds_drop; eauto. 
+Qed.
+
 (** Injecting a memory into itself. *)
 
 Definition flat_inj (thr: block) : meminj :=
diff --git a/common/Memtype.v b/common/Memtype.v
index f763581..2e44331 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -1159,6 +1159,16 @@ Axiom free_inject:
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 
+Axiom drop_outside_inject:
+  forall f m1 m2 b lo hi p m2',
+  inject f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  inject f m1 m2'.
+
 (** Memory states that inject into themselves. *)
 
 Definition flat_inj (thr: block) : meminj :=