Merge pull request #93 from AbsInt/separate-compilation

This pull request implements "approach A" to separate compilation in CompCert from the paper

Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190

In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.

This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.

1 files changed, 506 insertions, 23 deletions

diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 78345b42..9faa6d40 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -15,10 +15,8 @@
 
 (** Type expressions for the Compcert C and Clight languages *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
+Require Import Axioms Coqlib Maps Errors.
+Require Import AST Linking.
 Require Archi.
 
 (** * Syntax of types *)
@@ -157,6 +155,20 @@ Definition members : Type := list (ident * type).
 Inductive composite_definition : Type :=
   Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).
 
+Definition name_composite_def (c: composite_definition) : ident :=
+  match c with Composite id su m a => id end.
+
+Definition composite_def_eq (x y: composite_definition): {x=y} + {x<>y}.
+Proof.
+  decide equality.
+- decide equality. decide equality. apply N.eq_dec. apply bool_dec.
+- apply list_eq_dec. decide equality. apply type_eq. apply ident_eq.
+- decide equality.
+- apply ident_eq.
+Defined.
+
+Global Opaque composite_def_eq. 
+
 (** For type-checking, compilation and semantics purposes, the composite
   definitions are collected in the following [composite_env] environment.
   The [composite] record contains additional information compared with
@@ -960,6 +972,29 @@ Record composite_consistent (env: composite_env) (co: composite) : Prop := {
 Definition composite_env_consistent (env: composite_env) : Prop :=
   forall id co, env!id = Some co -> composite_consistent env co.
 
+Lemma composite_consistent_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         co,
+  composite_consistent env co -> composite_consistent env' co.
+Proof.
+  intros. destruct H as [A B C D]. constructor. 
+  eapply complete_members_stable; eauto.
+  symmetry; rewrite B. f_equal. apply alignof_composite_stable; auto. 
+  symmetry; rewrite C. f_equal. apply sizeof_composite_stable; auto.
+  symmetry; rewrite D. apply rank_members_stable; auto.
+Qed.
+
+Lemma composite_of_def_consistent:
+  forall env id su m a co,
+  composite_of_def env id su m a = OK co ->
+  composite_consistent env co.
+Proof.
+  unfold composite_of_def; intros. 
+  destruct (env!id); try discriminate. destruct (complete_members env m) eqn:C; inv H.
+  constructor; auto.
+Qed. 
+
 Theorem build_composite_env_consistent:
   forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
 Proof.
@@ -973,28 +1008,15 @@ Proof.
 - destruct d1; monadInv H.
   eapply IHdefs; eauto.
   set (env1 := PTree.set id x env0) in *.
-  unfold composite_of_def in EQ.
-  destruct (env0!id) eqn:E; try discriminate.
-  destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ.
+  assert (env0!id = None). 
+  { unfold composite_of_def in EQ. destruct (env0!id). discriminate. auto. }
   assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1).
   { intros. unfold env1. rewrite PTree.gso; auto. congruence. }
-  red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
+  red; intros. apply composite_consistent_stable with env0; auto.
+  unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
 + subst id0. inversion H2; clear H2. subst co.
-(*
-  assert (A: alignof_composite env1 m = alignof_composite env0 m)
-  by (apply alignof_composite_stable; assumption).
-*)
-  rewrite <- H1; constructor; simpl.
-* eapply complete_members_stable; eauto.
-* f_equal. symmetry. apply alignof_composite_stable; auto.
-* f_equal. symmetry. apply sizeof_composite_stable; auto.
-* symmetry. apply rank_members_stable; auto.
-+ exploit H0; eauto. intros [P Q R S].
-  constructor; intros.
-* eapply complete_members_stable; eauto.
-* rewrite Q. f_equal. symmetry. apply alignof_composite_stable; auto.
-* rewrite R. f_equal. symmetry. apply sizeof_composite_stable; auto.
-* rewrite S. symmetry; apply rank_members_stable; auto.
+  eapply composite_of_def_consistent; eauto.
++ eapply H0; eauto. 
 Qed.
 
 (** Moreover, every composite definition is reflected in the composite environment. *)
@@ -1018,6 +1040,29 @@ Proof.
   subst x; auto.
 Qed.
 
+Theorem build_composite_env_domain:
+  forall env defs id co,
+  build_composite_env defs = OK env ->
+  env!id = Some co ->
+  In (Composite id (co_su co) (co_members co) (co_attr co)) defs.
+Proof.
+  intros env0 defs0 id co.
+  assert (REC: forall l env env',
+    add_composite_definitions env l = OK env' ->
+    env'!id = Some co ->
+    env!id = Some co \/ In (Composite id (co_su co) (co_members co) (co_attr co)) l).
+  { induction l; simpl; intros. 
+  - inv H; auto.
+  - destruct a; monadInv H. exploit IHl; eauto.
+    unfold composite_of_def in EQ. destruct (env!id0) eqn:E; try discriminate.
+    destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
+    rewrite PTree.gsspec. intros [A|A]; auto.
+    destruct (peq id id0); auto.
+    inv A. rewrite <- H1; auto.
+  }
+  intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
+Qed.
+
 (** As a corollay, in a consistent environment, the rank of a composite type
   is strictly greater than the ranks of its member types. *)
 
@@ -1054,3 +1099,441 @@ Proof.
   exploit (rank_type_members ce); eauto.
   omega.
 Qed.
+
+(** * Programs and compilation units *)
+
+(** The definitions in this section are parameterized over a type [F] of 
+  internal function definitions, so that they apply both to CompCert C and to Clight. *)
+
+Set Implicit Arguments.
+
+Section PROGRAMS.
+
+Variable F: Type.
+
+(** Functions can either be defined ([Internal]) or declared as
+  external functions ([External]). *)
+
+Inductive fundef : Type :=
+  | Internal: F -> fundef
+  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+
+(** A program, or compilation unit, is composed of:
+- a list of definitions of functions and global variables;
+- the names of functions and global variables that are public (not static);
+- the name of the function that acts as entry point ("main" function).
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
+
+Record program : Type := {
+  prog_defs: list (ident * globdef fundef type);
+  prog_public: list ident;
+  prog_main: ident;
+  prog_types: list composite_definition;
+  prog_comp_env: composite_env;
+  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
+}.
+
+Definition program_of_program (p: program) : AST.program fundef type :=
+  {| AST.prog_defs := p.(prog_defs);
+     AST.prog_public := p.(prog_public);
+     AST.prog_main := p.(prog_main) |}.
+
+Coercion program_of_program: program >-> AST.program.
+
+Program Definition make_program (types: list composite_definition)
+                                (defs: list (ident * globdef fundef type))
+                                (public: list ident)
+                                (main: ident) : res program :=
+  match build_composite_env types with
+  | Error e => Error e
+  | OK ce =>
+      OK {| prog_defs := defs;
+            prog_public := public;
+            prog_main := main;
+            prog_types := types;
+            prog_comp_env := ce;
+            prog_comp_env_eq := _ |}
+  end.
+
+End PROGRAMS.
+
+Arguments External {F} _ _ _ _.
+
+Unset Implicit Arguments.
+
+(** * Separate compilation and linking *)
+
+(** ** Linking types *)
+
+Instance Linker_types : Linker type := {
+  link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
+  linkorder := fun t1 t2 => t1 = t2
+}.
+Proof.
+  auto.
+  intros; congruence.
+  intros. destruct (type_eq x y); inv H. auto.
+Defined.
+
+Global Opaque Linker_types.
+
+(** ** Linking composite definitions *)
+
+Definition check_compat_composite (l: list composite_definition) (cd: composite_definition) : bool :=
+  List.forallb
+    (fun cd' =>
+      if ident_eq (name_composite_def cd') (name_composite_def cd) then composite_def_eq cd cd' else true)
+    l.
+
+Definition filter_redefs (l1 l2: list composite_definition) :=
+  let names1 := map name_composite_def l1 in
+  List.filter (fun cd => negb (In_dec ident_eq (name_composite_def cd) names1)) l2.
+
+Definition link_composite_defs (l1 l2: list composite_definition): option (list composite_definition) :=
+  if List.forallb (check_compat_composite l2) l1
+  then Some (l1 ++ filter_redefs l1 l2)
+  else None.
+
+Lemma link_composite_def_inv:
+  forall l1 l2 l,
+  link_composite_defs l1 l2 = Some l ->
+     (forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)
+  /\ l = l1 ++ filter_redefs l1 l2
+  /\ (forall x, In x l <-> In x l1 \/ In x l2).
+Proof.
+  unfold link_composite_defs; intros.
+  destruct (forallb (check_compat_composite l2) l1) eqn:C; inv H.
+  assert (A: 
+    forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1).
+  { rewrite forallb_forall in C. intros.
+    apply C in H. unfold check_compat_composite in H. rewrite forallb_forall in H. 
+    apply H in H0. rewrite H1, dec_eq_true in H0. symmetry; eapply proj_sumbool_true; eauto. }
+  split. auto. split. auto. 
+  unfold filter_redefs; intros. 
+  rewrite in_app_iff. rewrite filter_In. intuition auto. 
+  destruct (in_dec ident_eq (name_composite_def x) (map name_composite_def l1)); simpl; auto.
+  exploit list_in_map_inv; eauto. intros (y & P & Q).
+  assert (x = y) by eauto. subst y. auto.
+Qed.
+
+Instance Linker_composite_defs : Linker (list composite_definition) := {
+  link := link_composite_defs;
+  linkorder := @List.incl composite_definition
+}.
+Proof.
+- intros; apply incl_refl.
+- intros; red; intros; eauto.
+- intros. apply link_composite_def_inv in H; destruct H as (A & B & C).
+  split; red; intros; apply C; auto.
+Defined.
+
+(** Connections with [build_composite_env]. *)
+
+Lemma add_composite_definitions_append:
+  forall l1 l2 env env'',
+  add_composite_definitions env (l1 ++ l2) = OK env'' <->
+  exists env', add_composite_definitions env l1 = OK env' /\ add_composite_definitions env' l2 = OK env''.
+Proof.
+  induction l1; simpl; intros.
+- split; intros. exists env; auto. destruct H as (env' & A & B). congruence.
+- destruct a; simpl. destruct (composite_of_def env id su m a); simpl.
+  apply IHl1. 
+  split; intros. discriminate. destruct H as (env' & A & B); discriminate.
+Qed.
+
+Lemma composite_eq:
+  forall su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1
+         su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2,
+  su1 = su2 -> m1 = m2 -> a1 = a2 -> sz1 = sz2 -> al1 = al2 -> r1 = r2 ->
+  Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2.
+Proof.
+  intros. subst.
+  assert (pos1 = pos2) by apply proof_irr. 
+  assert (al2p1 = al2p2) by apply proof_irr.
+  assert (szal1 = szal2) by apply proof_irr.
+  subst. reflexivity.
+Qed.
+
+Lemma composite_of_def_eq:
+  forall env id co,
+  composite_consistent env co ->
+  env!id = None ->
+  composite_of_def env id (co_su co) (co_members co) (co_attr co) = OK co.
+Proof.
+  intros. destruct H as [A B C D]. unfold composite_of_def. rewrite H0, A.
+  destruct co; simpl in *. f_equal. apply composite_eq; auto. rewrite C, B; auto. 
+Qed.
+
+Lemma composite_consistent_unique:
+  forall env co1 co2,
+  composite_consistent env co1 ->
+  composite_consistent env co2 ->
+  co_su co1 = co_su co2 ->
+  co_members co1 = co_members co2 ->
+  co_attr co1 = co_attr co2 ->
+  co1 = co2.
+Proof.
+  intros. destruct H, H0. destruct co1, co2; simpl in *. apply composite_eq; congruence.
+Qed.
+
+Lemma composite_of_def_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         id su m a co,
+  env'!id = None ->
+  composite_of_def env id su m a = OK co ->
+  composite_of_def env' id su m a = OK co.
+Proof.
+  intros. 
+  unfold composite_of_def in H0. 
+  destruct (env!id) eqn:E; try discriminate.
+  destruct (complete_members env m) eqn:CM; try discriminate.
+  transitivity (composite_of_def env' id (co_su co) (co_members co) (co_attr co)).
+  inv H0; auto. 
+  apply composite_of_def_eq; auto. 
+  apply composite_consistent_stable with env; auto. 
+  inv H0; constructor; auto.
+Qed.
+
+Lemma link_add_composite_definitions:
+  forall l0 env0,
+  build_composite_env l0 = OK env0 ->
+  forall l env1 env1' env2,
+  add_composite_definitions env1 l = OK env1' ->
+  (forall id co, env1!id = Some co -> env2!id = Some co) ->
+  (forall id co, env0!id = Some co -> env2!id = Some co) ->
+  (forall id, env2!id = if In_dec ident_eq id (map name_composite_def l0) then env0!id else env1!id) ->
+  ((forall cd1 cd2, In cd1 l0 -> In cd2 l -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)) ->
+  { env2' |
+      add_composite_definitions env2 (filter_redefs l0 l) = OK env2'
+  /\ (forall id co, env1'!id = Some co -> env2'!id = Some co)
+  /\ (forall id co, env0!id = Some co -> env2'!id = Some co) }.
+Proof.
+  induction l; simpl; intros until env2; intros ACD AGREE1 AGREE0 AGREE2 UNIQUE.
+- inv ACD. exists env2; auto.
+- destruct a. destruct (composite_of_def env1 id su m a) as [x|e] eqn:EQ; try discriminate.
+  simpl in ACD.
+  generalize EQ. unfold composite_of_def at 1. 
+  destruct (env1!id) eqn:E1; try congruence.
+  destruct (complete_members env1 m) eqn:CM1; try congruence. 
+  intros EQ1.
+  simpl. destruct (in_dec ident_eq id (map name_composite_def l0)); simpl.
++ eapply IHl; eauto.
+* intros. rewrite PTree.gsspec in H0. destruct (peq id0 id); auto.
+  inv H0.
+  exploit list_in_map_inv; eauto. intros ([id' su' m' a'] & P & Q).
+  assert (X: Composite id su m a = Composite id' su' m' a').
+  { eapply UNIQUE. auto. auto. rewrite <- P; auto. }
+  inv X.
+  exploit build_composite_env_charact; eauto. intros (co' & U & V & W & X). 
+  assert (co' = co).
+  { apply composite_consistent_unique with env2.
+    apply composite_consistent_stable with env0; auto. 
+    eapply build_composite_env_consistent; eauto.
+    apply composite_consistent_stable with env1; auto.
+    inversion EQ1; constructor; auto. 
+    inversion EQ1; auto.
+    inversion EQ1; auto.
+    inversion EQ1; auto. }
+  subst co'. apply AGREE0; auto. 
+* intros. rewrite AGREE2. destruct (in_dec ident_eq id0 (map name_composite_def l0)); auto. 
+  rewrite PTree.gsspec. destruct (peq id0 id); auto. subst id0. contradiction.
++ assert (E2: env2!id = None).
+  { rewrite AGREE2. rewrite pred_dec_false by auto. auto. }
+  assert (E3: composite_of_def env2 id su m a = OK x).
+  { eapply composite_of_def_stable. eexact AGREE1. eauto. eauto. }
+  rewrite E3. simpl. eapply IHl; eauto. 
+* intros until co; rewrite ! PTree.gsspec. destruct (peq id0 id); auto.
+* intros until co; rewrite ! PTree.gsspec. intros. destruct (peq id0 id); auto.
+  subst id0. apply AGREE0 in H0. congruence.
+* intros. rewrite ! PTree.gsspec. destruct (peq id0 id); auto. subst id0. 
+  rewrite pred_dec_false by auto. auto.
+Qed.
+
+Theorem link_build_composite_env:
+  forall l1 l2 l env1 env2,
+  build_composite_env l1 = OK env1 ->
+  build_composite_env l2 = OK env2 ->
+  link l1 l2 = Some l ->
+  { env |
+     build_composite_env l = OK env
+  /\ (forall id co, env1!id = Some co -> env!id = Some co)
+  /\ (forall id co, env2!id = Some co -> env!id = Some co) }.
+Proof.
+  intros. edestruct link_composite_def_inv as (A & B & C); eauto.
+  edestruct link_add_composite_definitions as (env & P & Q & R).
+  eexact H.
+  eexact H0.
+  instantiate (1 := env1). intros. rewrite PTree.gempty in H2; discriminate.
+  auto.
+  intros. destruct (in_dec ident_eq id (map name_composite_def l1)); auto.
+  rewrite PTree.gempty. destruct (env1!id) eqn:E1; auto. 
+  exploit build_composite_env_domain. eexact H. eauto.
+  intros. apply (in_map name_composite_def) in H2. elim n; auto. 
+  auto.
+  exists env; split; auto. subst l. apply add_composite_definitions_append. exists env1; auto. 
+Qed.
+
+(** ** Linking function definitions *)
+
+Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
+  match fd1, fd2 with
+  | Internal _, Internal _ => None
+  | External ef1 targs1 tres1 cc1, External ef2 targs2 tres2 cc2 =>
+      if external_function_eq ef1 ef2
+      && typelist_eq targs1 targs2
+      && type_eq tres1 tres2
+      && calling_convention_eq cc1 cc2
+      then Some (External ef1 targs1 tres1 cc1)
+      else None
+  | Internal f, External ef targs tres cc =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  | External ef targs tres cc, Internal f =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  end.
+
+Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
+  | linkorder_fundef_refl: forall fd,
+      linkorder_fundef fd fd
+  | linkorder_fundef_ext_int: forall f id sg targs tres cc,
+      linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
+
+Instance Linker_fundef (F: Type): Linker (fundef F) := {
+  link := link_fundef;
+  linkorder := linkorder_fundef
+}.
+Proof.
+- intros; constructor.
+- intros. inv H; inv H0; constructor.
+- intros x y z EQ. destruct x, y; simpl in EQ.
++ discriminate.
++ destruct e; inv EQ. split; constructor.
++ destruct e; inv EQ. split; constructor.
++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ.
+  InvBooleans. subst. split; constructor.
+Defined.
+
+Remark link_fundef_either:
+  forall (F: Type) (f1 f2 f: fundef F), link f1 f2 = Some f -> f = f1 \/ f = f2.
+Proof.
+  simpl; intros. unfold link_fundef in H. destruct f1, f2; try discriminate.
+- destruct e; inv H. auto.
+- destruct e; inv H. auto.
+- destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0); inv H; auto.
+Qed.
+
+Global Opaque Linker_fundef.
+
+(** ** Linking programs *)
+
+Definition lift_option {A: Type} (opt: option A) : { x | opt = Some x } + { opt = None }.
+Proof.
+  destruct opt. left; exists a; auto. right; auto. 
+Defined.
+
+Definition link_program {F:Type} (p1 p2: program F): option (program F) :=
+  match link (program_of_program p1) (program_of_program p2) with
+  | None => None
+  | Some p =>
+      match lift_option (link p1.(prog_types) p2.(prog_types)) with
+      | inright _ => None
+      | inleft (exist typs EQ) =>
+          match link_build_composite_env
+                   p1.(prog_types) p2.(prog_types) typs
+                   p1.(prog_comp_env) p2.(prog_comp_env)
+                   p1.(prog_comp_env_eq) p2.(prog_comp_env_eq) EQ with
+          | exist env (conj P Q) =>
+              Some {| prog_defs := p.(AST.prog_defs);
+                      prog_public := p.(AST.prog_public);
+                      prog_main := p.(AST.prog_main);
+                      prog_types := typs;
+                      prog_comp_env := env;
+                      prog_comp_env_eq := P |}
+          end
+      end
+  end.
+
+Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
+     linkorder (program_of_program p1) (program_of_program p2)
+  /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
+
+Instance Linker_program (F: Type): Linker (program F) := {
+  link := link_program;
+  linkorder := linkorder_program
+}.
+Proof.
+- intros; split. apply linkorder_refl. auto. 
+- intros. destruct H, H0. split. eapply linkorder_trans; eauto.
+  intros; auto.
+- intros until z. unfold link_program. 
+  destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate.
+  destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types x) (prog_types y) typs
+       (prog_comp_env x) (prog_comp_env y) (prog_comp_env_eq x)
+       (prog_comp_env_eq y) EQ) as (env & P & Q & R).
+  destruct (link_linkorder _ _ _ LP). 
+  intros X; inv X.
+  split; split; auto.
+Defined.
+
+Global Opaque Linker_program.
+
+(** ** Commutation between linking and program transformations *)
+
+Section LINK_MATCH_PROGRAM.
+
+Context {F G: Type}.
+Variable match_fundef: fundef F -> fundef G -> Prop.
+
+Hypothesis link_match_fundef:
+  forall f1 tf1 f2 tf2 f,
+  link f1 f2 = Some f ->
+  match_fundef f1 tf1 -> match_fundef f2 tf2 ->
+  exists tf, link tf1 tf2 = Some tf /\ match_fundef f tf.
+
+Let match_program (p: program F) (tp: program G) : Prop :=
+    Linking.match_program (fun ctx f tf => match_fundef f tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Theorem link_match_program:
+  forall p1 p2 tp1 tp2 p,
+  link p1 p2 = Some p -> match_program p1 tp1 -> match_program p2 tp2 ->
+  exists tp, link tp1 tp2 = Some tp /\ match_program p tp.
+Proof.
+  intros. destruct H0, H1. 
+Local Transparent Linker_program.
+  simpl in H; unfold link_program in H.
+  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
+  assert (A: exists tpp,
+               link (program_of_program tp1) (program_of_program tp2) = Some tpp
+             /\ Linking.match_program (fun ctx f tf => match_fundef f tf) eq pp tpp).
+  { eapply Linking.link_match_program. 
+  - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
+  - intros.
+    Local Transparent Linker_types.
+    simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto.
+  - eauto.
+  - eauto.
+  - eauto.
+  - apply (link_linkorder _ _ _ LP).
+  - apply (link_linkorder _ _ _ LP). }
+  destruct A as (tpp & TLP & MP).
+  simpl; unfold link_program. rewrite TLP.
+  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
+           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
+           (prog_comp_env_eq p2) EQ) as (env & P & Q). 
+  rewrite <- H2, <- H3 in EQ.
+  destruct (lift_option (link (prog_types tp1) (prog_types tp2))) as [[ttyps EQ']|EQ']; try congruence.
+  assert (ttyps = typs) by congruence. subst ttyps. 
+  destruct (link_build_composite_env (prog_types tp1) (prog_types tp2) typs
+         (prog_comp_env tp1) (prog_comp_env tp2) (prog_comp_env_eq tp1)
+         (prog_comp_env_eq tp2) EQ') as (tenv & R & S).
+  assert (tenv = env) by congruence. subst tenv.
+  econstructor; split; eauto. inv H. split; auto.
+  unfold program_of_program; simpl. destruct pp, tpp; exact MP.
+Qed.
+
+End LINK_MATCH_PROGRAM.