Module SepComp

Require Import UpperBound_A UpperBound_B LowerBound.
Require Import CompilerC.
Require Import CoqlibC.
Require Import BehaviorsC LinkingC EventsC MapsC ASTC CtypesC.


Lemma back_propagate_ub_behav
      beh0
      (INITUB: behavior_improves beh0 (Goes_wrong E0)):
    <<INITUB: beh0 = Goes_wrong E0>>.
Proof.
  rr in INITUB. des; clarify; et.
  rr in INITUB0. des. unfold behavior_app in *. des_ifs. destruct t; ss.
Qed.

Lemma back_propagate_ub_program
      sem0 sem1
      (IMPR: improves sem0 sem1)
      (INITUB: program_behaves sem1 (Goes_wrong E0)):
    <<INITUB: program_behaves sem0 (Goes_wrong E0)>>.
Proof.
  exploit IMPR; eauto. i; des.
  hexploit back_propagate_ub_behav; et. i ;des. clarify.
Qed.

Theorem separate_compilation_correct
        (srcs: list Csyntax.program) (tgts: list Asm.program) builtins src_link
        (TYPECHECKS: Forall (fun src => CsemC.typechecked builtins src) srcs)
        (TYPECHECKLINK: CsemC.typechecked builtins src_link)
        (LINK: link_list srcs = Some src_link)
        (MAIN: exists main_f,
            (<<INTERNAL: src_link.(prog_defmap) ! (src_link.(prog_main)) = Some (Gfun (Ctypes.Internal main_f))>>) /\
            (<<SIG: type_of_function main_f = Tfunction Ctypes.Tnil type_int32s cc_default>>))
        (TR: Errors.mmap transf_c_program srcs = Errors.OK tgts):
    (<<INITUB: program_behaves (Csem.semantics src_link) (Goes_wrong E0)>>) \/
    exists tgt_link, <<LINK: link_list tgts = Some tgt_link>> /\
                     <<IMPROVES: improves (Csem.semantics src_link) (Asm.semantics tgt_link)>>.
Proof.
  hexploit upperbound_b_correct; eauto. { des. esplits; et. } intro A.
  hexploit upperbound_a_correct; eauto. instantiate (1:= []). ss. intro B; des.
  hexploit compiler_correct_full; eauto.
  { do 2 instantiate (1:= []). ss. }
  instantiate (1:= []). ss. rewrite ! app_nil_r. intro C; des.
  hexploit (lower_bound_correct tgts); eauto. intro D. des.
  { left.
    hexploit back_propagate_ub_program; try apply C; et. intro CUB.
    hexploit back_propagate_ub_program; try apply CUB; et. intro BUB.
    hexploit back_propagate_ub_program; try apply BUB; et.
  }
  right. esplits; et. etrans; et. etrans; et. etrans; et.
Qed.