(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(* Trying an abstract compiler with labels instead of nats as source code addressing *)

Require Import List Arith Omega.

Require Import utils subcode sss bsm_defs compiler.


(** ** Semantic Correctness of Compiled Code *)

Set Implicit Arguments.

Section comp.

  (** This is an abstract proof of compiler soundness & completeness 

      The principle of this compiler is to map every source individual
      instruction into a list of target instructions that simulate the
      source instruction. We describe our assumptions later on ...

    *)

  Variable (X Y : Set)                                  (* X is a small type of source instructions and 
                                                           Y of destination instructions *) 
           (icomp : (nat -> nat) -> nat -> X -> list Y) (* instruction compiler w.r.t. a given linker & a position 
                                                           icomp lnk i x compiles instruction x at position i 
                                                           using linker lnk into a list of target instructions
                                                         *)
           (ilen  : X -> nat)                           (* compiled code length does not depend on linker or position,
                                                           it only depends on the original instruction
                                                           whether this assumption is strong or not is debatable
                                                           but we only encountered cases which satisfy this assuption
                                                         *)
           (Hilen : forall lnk n x, length (icomp lnk n x) = ilen x)
           (*Hilen2  : forall x, 1 <= ilen x*).           (* compiled code should not be empty, even if the source
                                                           instruction is something like NO-OP, to ensure progress
                                                           in the simulation as source code executes 
                                                           also not a strong requirement

                                                           This can be removed because it can be deduced (where it
                                                           is used) from Hilen1 & step_X_tot & Hicomp 
                                                         *)

  (* Semantics for X and Y instructions *)

  Variables (state_X state_Y : Type)
            (step_X : X -> (nat*state_X) -> (nat*state_X) -> Prop)
            (step_Y : Y -> (nat*state_Y) -> (nat*state_Y) -> Prop).

  Notation "i '/X/' s -1> t" := (step_X i s t) (at level 70, no associativity).
  Notation "P '/X/' s '-[' k ']->' t" := (sss_steps step_X P k s t) (at level 70, no associativity).
  Notation "P '/X/' s '-+>' t" := (sss_progress step_X P s t) (at level 70, no associativity).
  Notation "P '/X/' s ->> t" := (sss_compute step_X P s t) (at level 70, no associativity).
  Notation "P '/X/' s '~~>' t" := (sss_output step_X P s t) (at level 70, no associativity).
  Notation "P '/X/' s ↓" := (sss_terminates step_X P s)(at level 70, no associativity).

  Notation "i '/Y/' s -1> t" := (step_Y i s t) (at level 70, no associativity).
  Notation "P '/Y/' s '-[' k ']->' t" := (sss_steps step_Y P k s t) (at level 70, no associativity).
  Notation "P '/Y/' s '-+>' t" := (sss_progress step_Y P s t) (at level 70, no associativity).
  Notation "P '/Y/' s ->> t" := (sss_compute step_Y P s t) (at level 70, no associativity).
  Notation "P '/Y/' s '~~>' t" := (sss_output step_Y P s t) (at level 70, no associativity).
  Notation "P '/Y/' s ↓" := (sss_terminates step_Y P s)(at level 70, no associativity).

  (** We assume totality of X semantics, i.e. no instruction can block the computation
      and functionality of Y semantics 

      Totality is not necessary achieved ... think of a HALT instruction 
      what should we do in that case ? It should not be too difficult to
      embed a partial model of computation into a total one by transforming
      blocking cases into jumps at a PC value outside of the code.
    *)

  Hypothesis (step_X_tot : forall I st1, exists st2, I /X/ st1 -1> st2)
             (step_Y_fun : forall I st st1 st2, I /Y/ st -1> st1 -> I /Y/ st -1> st2 -> st1 = st2).

 (** simul is an invariant: simul st_X st_Y means that st_X is simulated by st_Y *)

  Variable (simul : state_X -> state_Y -> Prop).

  Infix "⋈" := simul (at level 70, no associativity).

  (** Simulation is preserved by compiled instructions 
      this of course ensures the *semantic correctness of
      the compilation of individual instructions*

      Notice the important hypothesis of preservation of the +1
      relative address by the linker otherwise it might not be
      possible to establish the below predicate.

      If the source language involves other relative addresses like
      +2 or +d or -d, the present compiler might have to be substantially
      updated.

      +1 is very likely to be used even implicitly because every instruction
      that does not branch (like INC or PUSH) implicitly jumps at +1 ...
    *) 

  Definition instruction_compiler_sound := forall lnk I i1 v1 i2 v2 w1, 
                     I /X/ (i1,v1) -1> (i2,v2)
                  -> lnk (1+i1) = length (icomp lnk i1 I) + lnk i1
                  -> v1 ⋈ w1
       -> exists w2, (lnk i1,icomp lnk i1 I) /Y/ (lnk i1,w1) -+> (lnk i2,w2)
                  /\ v2 ⋈ w2.

  Hypothesis Hicomp : instruction_compiler_sound.

  Section correctness. 

    (** We assume each instruction in P is compiled in Q according to the individual 
        instruction compiler combined with what the linker says for branching. 
        This is a *syntactic correctness criterion* for the whole compiled program Q
      *)

    Variables (linker : nat -> nat) (P : nat * list X) (Q : nat * list Y)
              (HPQ : forall i I, (i,I::nil) <sc P -> (linker i, icomp linker i I) <sc Q
                                                   /\ linker (1+i) = ilen I + linker i).

    (** From semantic correctness of individually compiled instructions and
        syntactic correctness of the whole compiled program, we derive
        soundness and completeness of the compiled program Q wrt the
        source program P *)

    Theorem compiler_sound i1 v1 i2 v2 w1 :
                      v1 ⋈ w1 /\ P /X/ (i1,v1) ->> (i2,v2)
        -> exists w2, v2 ⋈ w2 /\ Q /Y/ (linker i1,w1) ->> (linker i2,w2).
    Proof.
(* Goal: forall _ : and (simul v1 w1) (@sss_compute X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)), @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker i1) w1) (@pair nat state_Y (linker i2) w2))) *)
      change i1 with (fst (i1,v1)) at 2; change v1 with (snd (i1,v1)) at 1.
(* Goal: forall _ : and (simul (@snd nat state_X (@pair nat state_X i1 v1)) w1) (@sss_compute X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)), @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (@fst nat state_X (@pair nat state_X i1 v1))) w1) (@pair nat state_Y (linker i2) w2))) *)
      change i2 with (fst (i2,v2)) at 2; change v2 with (snd (i2,v2)) at 2.
(* Goal: forall _ : and (simul (@snd nat state_X (@pair nat state_X i1 v1)) w1) (@sss_compute X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)), @ex state_Y (fun w2 : state_Y => and (simul (@snd nat state_X (@pair nat state_X i2 v2)) w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (@fst nat state_X (@pair nat state_X i1 v1))) w1) (@pair nat state_Y (linker (@fst nat state_X (@pair nat state_X i2 v2))) w2))) *)
      generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2.
(* Goal: forall (p p0 : prod nat state_X) (_ : and (simul (@snd nat state_X p) w1) (@sss_compute X state_X step_X P p p0)), @ex state_Y (fun w2 : state_Y => and (simul (@snd nat state_X p0) w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (@fst nat state_X p)) w1) (@pair nat state_Y (linker (@fst nat state_X p0)) w2))) *)
      intros st1 st2 (H1 & q & H2); revert H2 w1 H1.
(* Goal: forall (_ : @sss_steps X state_X step_X P q st1 st2) (w1 : state_Y) (_ : simul (@snd nat state_X st1) w1), @ex state_Y (fun w2 : state_Y => and (simul (@snd nat state_X st2) w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (@fst nat state_X st1)) w1) (@pair nat state_Y (linker (@fst nat state_X st2)) w2))) *)
      induction 1 as [ (i1,v1) | q (i1,v1) (i2,v2) st3 H1 H2 IH2]; simpl; intros w1 H0.
      + exists w1; split; auto; exists 0; constructor.
      + destruct H1 as (k & l & I & r & v' & G1 & G2 & G3).
(* Goal: @ex state_Y (fun w2 : state_Y => and (simul (@snd nat state_X st3) w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker i1) w1) (@pair nat state_Y (linker (@fst nat state_X st3)) w2))) *)
        inversion G2; subst v' i1; clear G2.
        destruct (Hicomp linker) with (1 := G3) (3 := H0)
          as (w2 & G4 & G5).
        * rewrite Hilen; apply HPQ; subst; exists l, r; auto.
        * destruct (IH2 _ G5) as (w3 & G6 & G7).
(* Goal: @ex state_Y (fun w2 : state_Y => and (simul (@snd nat state_X st3) w2) (@sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (Init.Nat.add k (@length X l))) w1) (@pair nat state_Y (linker (@fst nat state_X st3)) w2))) *)
          exists w3; split; auto.
(* Goal: @sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (Init.Nat.add k (@length X l))) w1) (@pair nat state_Y (linker (@fst nat state_X st3)) w3) *)
          apply sss_compute_trans with (2 := G7); simpl.
(* Goal: @sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker (Init.Nat.add k (@length X l))) w1) (@pair nat state_Y (linker i2) w2) *)
          apply sss_progress_compute.
(* Goal: @sss_progress Y state_Y step_Y Q (@pair nat state_Y (linker (Init.Nat.add k (@length X l))) w1) (@pair nat state_Y (linker i2) w2) *)
          revert G4; apply subcode_sss_progress.
(* Goal: @subcode Y (@pair nat (list Y) (linker (Init.Nat.add k (@length X l))) (icomp linker (Init.Nat.add k (@length X l)) I)) Q *)
          apply HPQ; subst; exists l, r; auto.
    Qed.

    (* When still inside of P, the computation in Q simulates
       a computation in P *)

    Local Lemma compiler_complete_step p st1 w1 w3 :
           snd st1 ⋈ snd w1
        -> linker (fst st1) = fst w1
        -> in_code (fst st1) P
        -> out_code (fst w3) Q
        -> Q /Y/ w1 -[p]-> w3
        -> exists q st2 w2, snd st2 ⋈ snd w2
                        /\ linker (fst st2) = fst w2
                        /\ P /X/ st1 ->> st2
                        /\ Q /Y/ w2 -[q]-> w3
                        /\ q < p.
    Proof.
      revert st1 w1 w3; intros (i1,v1) (j1,w1) (j3,w3); simpl fst; simpl snd.
      intros H1 H2 H3 H4 H5.
      destruct (in_code_subcode H3) as (I & HI).
      destruct HPQ with (1 := HI) as (H6 & H7).
      assert (out_code j3 (linker i1, icomp linker i1 I)) as G2.
      { revert H4; apply subcode_out_code; auto. }
      assert (H8 : ilen I <> 0).
      { intros H.
        destruct (step_X_tot I (i1,v1)) as ((i2,v2) & Hst).
        apply (Hicomp linker) with (3 := H1) in Hst; auto.
        2: rewrite Hilen; auto.
        destruct Hst as (w2 & (q & Hq1 & Hq2) & _).
        rewrite <- (Hilen linker i1) in H.
        destruct (icomp linker i1 I); try discriminate.
        apply sss_steps_stall, proj1 in Hq2; simpl; omega. }
      assert (in_code (linker i1) (linker i1, icomp linker i1 I)) as G3.
      { simpl; rewrite (Hilen linker i1 I); omega. }
      rewrite <- H2 in H5.
      destruct (step_X_tot I (i1,v1)) as ((i2,v2) & G4).
      destruct (Hicomp linker) with (1 := G4) (3 := H1) as (w2 & G5 & G6).
      * rewrite H7, Hilen; auto.
      * apply subcode_sss_progress_inv with (3 := H6) (4 := G5) in H5; auto.
        destruct H5 as (q & H5 & G7).
        exists q, (i2,v2), (linker i2, w2); simpl; repeat (split; auto).
        apply subcode_sss_compute with (1 := HI).
        exists 1; apply sss_steps_1.
        exists i1, nil, I, nil, v1; repeat (split; auto).
        f_equal; simpl; omega.
    Qed.

    (* Termination in Q simulates termination in P *)

    Theorem compiler_complete i1 v1 w1 : 
          v1 ⋈ w1 -> Q /Y/ (linker i1,w1) ↓ -> P /X/ (i1,v1) ↓.
    Proof.
(* Goal: forall (_ : simul v1 w1) (_ : @sss_terminates Y state_Y step_Y Q (@pair nat state_Y (linker i1) w1)), @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
      intros H1 (st & (q & H2) & H3). 
(* Goal: @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
      revert i1 v1 w1 H1 H2 H3.
(* Goal: forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (_ : simul v1 w1) (_ : @sss_steps Y state_Y step_Y Q q (@pair nat state_Y (linker i1) w1) st) (_ : @out_code Y (@fst nat state_Y st) Q), @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
      induction q as [ q IHq ] using (well_founded_induction lt_wf).
(* Goal: forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (_ : simul v1 w1) (_ : @sss_steps Y state_Y step_Y Q q (@pair nat state_Y (linker i1) w1) st) (_ : @out_code Y (@fst nat state_Y st) Q), @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
      intros i1 v1 w1 H1 H2 H3.
(* Goal: @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
      destruct (in_out_code_dec i1 P) as [ H4 | H4 ].
      + destruct compiler_complete_step with (5 := H2) (st1 := (i1,v1))
          as (p & (i2,v2) & (j2,w2) & G1 & G2 & G3 & G4 & G5); auto; simpl in *; subst j2.
        destruct IHq with (1 := G5) (2 := G1) (3 := G4)
          as ((i3 & v3) & F3 & F4); auto.
(* Goal: @sss_terminates X state_X step_X P (@pair nat state_X i1 v1) *)
        exists (i3,v3); repeat (split; auto).
(* Goal: @sss_compute X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i3 v3) *)
        apply sss_compute_trans with (1 := G3); auto.
      + exists (i1,v1); repeat (split; auto).
(* Goal: @sss_compute X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i1 v1) *)
        exists 0; constructor.
    Qed.

    Corollary compiler_complete' i1 v1 w1 st : 
                            v1 ⋈ w1 /\ Q /Y/ (linker i1,w1) ~~> st
        -> exists i2 v2 w2, v2 ⋈ w2 /\ P /X/ (i1,v1) ~~> (i2,v2)
                                    /\ Q /Y/ (linker i2,w2) ~~> st.
    Proof.
(* Goal: forall _ : and (simul v1 w1) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i1) w1) st), @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (and (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st))))) *)
      intros (H1 & H2).
      destruct compiler_complete with (1 := H1) (2 := ex_intro (fun x => Q /Y/ (linker i1, w1) ~~> x) _ H2)
        as ((i2,v2) & H3 & H4).
(* Goal: @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (and (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st))))) *)
      exists i2, v2.
(* Goal: @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (and (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st))) *)
      destruct (compiler_sound (conj H1 H3)) as (w2 & H5 & H6).
(* Goal: @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (and (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st))) *)
      exists w2; do 2 (split; auto).
(* Goal: @sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2) *)
(* Goal: @sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st *)
      split; auto.
(* Goal: @sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2) *)
(* Goal: @sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st *)
      destruct H2 as (H2 & H0); split; auto.
(* Goal: @sss_compute Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st *)
      apply sss_compute_inv with (3 := H6); auto.
    Qed.

  End correctness.

  (** ** A Syntactically Correct Compiler *)

  (** Now we build a correct linker & compiled program pair *)

  Variable (P : nat * list X) (iQ : nat).

  Let iP := fst P.
  Let cP := snd P.

  Let err := iQ+length_compiler ilen cP.

  Definition gen_linker := linker ilen (iP,cP) iQ err.
  Definition gen_compiler := compiler icomp ilen (iP,cP) iQ err.

  Notation cQ := gen_compiler.
  Notation lnk := gen_linker.

  Let P_eq : P = (iP,cP).
  Proof. unfold iP, cP; destruct P; auto. Qed.

  Fact gen_linker_out i : out_code i (iP,cP) -> lnk i = iQ+length cQ.
  Proof.
(* Goal: forall _ : @out_code X i (@pair nat (list X) iP cP), @eq nat (gen_linker i) (Init.Nat.add iQ (@length Y gen_compiler)) *)
    intros H.
(* Goal: @eq nat (gen_linker i) (Init.Nat.add iQ (@length Y gen_compiler)) *)
    unfold lnk.
(* Goal: @eq nat (@linker X ilen (@pair nat (list X) iP cP) iQ err i) (Init.Nat.add iQ (@length Y gen_compiler)) *)
    rewrite linker_out_err; unfold err; simpl; auto.
    * unfold cQ; rewrite compiler_length; auto.
    * omega.
  Qed.

  Theorem gen_compiler_sound i1 v1 i2 v2 w1 : 
                    v1 ⋈ w1 /\ (iP,cP) /X/ (i1,v1) ~~> (i2,v2)
      -> exists w2, v2 ⋈ w2 /\ (iQ,cQ) /Y/ (lnk i1,w1) ~~> (lnk i2,w2).
  Proof.
(* Goal: forall _ : and (simul v1 w1) (@sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)), @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1) (@pair nat state_Y (gen_linker i2) w2))) *)
    intros (H1 & H2 & H3).
    destruct compiler_sound with (2 := conj H1 H2) (linker := gen_linker) (Q := (iQ,cQ))
      as (w2 & G1 & G2).
    + apply compiler_subcode; auto.
    + simpl fst in H3.
(* Goal: @sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2) *)
(* Goal: @sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st *)
      exists w2; split; auto.
(* Goal: @sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1) (@pair nat state_Y (gen_linker i2) w2) *)
      split; auto; simpl.
(* Goal: or (lt (gen_linker i2) iQ) (le (Init.Nat.add iQ (@length Y gen_compiler)) (gen_linker i2)) *)
      rewrite <- gen_linker_out with i2; auto.
  Qed.

  Theorem gen_compiler_complete i1 v1 w1 :
            v1 ⋈ w1 -> (iQ,gen_compiler) /Y/ (gen_linker i1,w1) ↓ -> (iP,cP) /X/ (i1,v1) ↓.
  Proof.
(* Goal: forall (_ : simul v1 w1) (_ : @sss_terminates Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1)), @sss_terminates X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) *)
    apply compiler_complete, compiler_subcode; auto.
  Qed.

  Corollary gen_compiler_output v w i' v' : 
        v ⋈ w -> (iP,cP) /X/ (iP,v) ~~> (i',v') -> exists w', (iQ,gen_compiler) /Y/ (iQ,w) ~~> (code_end (iQ,cQ),w') /\ v' ⋈ w'.
  Proof.
(* Goal: forall (_ : simul v w) (_ : @sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X iP v) (@pair nat state_X i' v')), @ex state_Y (fun w' : state_Y => and (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y iQ w) (@pair nat state_Y (@code_end Y (@pair nat (list Y) iQ gen_compiler)) w')) (simul v' w')) *)
    intros H H1.
(* Goal: @ex state_Y (fun w' : state_Y => and (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y iQ w) (@pair nat state_Y (@code_end Y (@pair nat (list Y) iQ gen_compiler)) w')) (simul v' w')) *)
    destruct gen_compiler_sound with (1 := conj H H1) as (w1 & H2 & H3).
(* Goal: @ex state_Y (fun w' : state_Y => and (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y iQ w) (@pair nat state_Y (@code_end Y (@pair nat (list Y) iQ gen_compiler)) w')) (simul v' w')) *)
    exists w1.
(* Goal: and (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y iQ w) (@pair nat state_Y (@code_end Y (@pair nat (list Y) iQ gen_compiler)) w1)) (simul v' w1) *)
    simpl; rewrite <- gen_linker_out with i'.
    + rewrite <- (linker_code_start ilen (iP,cP) iQ err) at 2; auto.
    + apply H1.
  Qed.

  Corollary gen_compiler_terminates v w : 
          v ⋈ w -> (iQ,gen_compiler) /Y/ (iQ,w) ↓ -> (iP,cP) /X/ (iP,v) ↓.
  Proof.
(* Goal: forall (_ : simul v w) (_ : @sss_terminates Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y iQ w)), @sss_terminates X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X iP v) *)
    intros H (w' & H').
(* Goal: @sss_terminates X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X iP v) *)
    apply gen_compiler_complete with (1 := H).
(* Goal: @sss_terminates Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker iP) w) *)
    unfold gen_linker; rewrite linker_code_start; auto; firstorder.
  Qed.

  Theorem gen_compiler_correction : 
           { lnk : nat -> nat 
           & { Q | fst Q = iQ 
                /\ lnk iP = iQ
                /\ (forall i, out_code i P -> lnk i = code_end Q)
                /\ (forall i1 v1 w1 i2 v2, v1 ⋈ w1 /\ P /X/ (i1,v1) ~~> (i2,v2)     -> exists w2,    v2 ⋈ w2 /\ Q /Y/ (lnk i1,w1) ~~> (lnk i2,w2)) 
                /\ (forall i1 v1 w1 j2 w2, v1 ⋈ w1 /\ Q /Y/ (lnk i1,w1) ~~> (j2,w2) -> exists i2 v2, v2 ⋈ w2 /\ P /X/ (i1,v1) ~~> (i2,v2) /\ j2 = lnk i2) 
           } }.
  Proof.
(* Goal: @sigT (forall _ : nat, nat) (fun lnk : forall _ : nat, nat => @sig (prod nat (list Y)) (fun Q : prod nat (list Y) => and (@eq nat (@fst nat (list Y) Q) iQ) (and (@eq nat (lnk iP) iQ) (and (forall (i : nat) (_ : @out_code X i P), @eq nat (lnk i) (@code_end Y Q)) (and (forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (i2 : nat) (v2 : state_X) (_ : and (simul v1 w1) (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2))), @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (lnk i1) w1) (@pair nat state_Y (lnk i2) w2)))) (forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (j2 : nat) (w2 : state_Y) (_ : and (simul v1 w1) (@sss_output Y state_Y step_Y Q (@pair nat state_Y (lnk i1) w1) (@pair nat state_Y j2 w2))), @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => and (simul v2 w2) (and (@sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@eq nat j2 (lnk i2))))))))))) *)
    exists lnk, (iQ,cQ); split; auto; split; [ | split ].
    + rewrite <- (linker_code_start ilen (iP,cP) iQ err); auto.
    + rewrite P_eq; apply gen_linker_out.
    + rewrite P_eq.
(* Goal: and (forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (i2 : nat) (v2 : state_X) (_ : and (simul v1 w1) (@sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) (@pair nat state_X i2 v2))), @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1) (@pair nat state_Y (gen_linker i2) w2)))) (forall (i1 : nat) (v1 : state_X) (w1 : state_Y) (j2 : nat) (w2 : state_Y) (_ : and (simul v1 w1) (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1) (@pair nat state_Y j2 w2))), @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => and (simul v2 w2) (and (@sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@eq nat j2 (gen_linker i2)))))) *)
      split.
      * intros i1 v1 w1 i2 v2 H.
(* Goal: @ex state_Y (fun w2 : state_Y => and (simul v2 w2) (@sss_output Y state_Y step_Y (@pair nat (list Y) iQ gen_compiler) (@pair nat state_Y (gen_linker i1) w1) (@pair nat state_Y (gen_linker i2) w2))) *)
        destruct gen_compiler_sound with (1 := H) as (w2 & H3 & H4).
(* Goal: @sss_output X state_X step_X P (@pair nat state_X i1 v1) (@pair nat state_X i2 v2) *)
(* Goal: @sss_output Y state_Y step_Y Q (@pair nat state_Y (linker i2) w2) st *)
        exists w2; split; auto.
      * intros i1 v1 w1 j2 w2 (H1 & H2).
        destruct gen_compiler_complete with (1 := H1) (i1 := i1) 
          as ((i3,v3) & H3).
        - exists (j2,w2); auto.
        - destruct gen_compiler_sound with (1 := conj H1 H3) as (w3 & H4 & H5).
(* Goal: @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => and (simul v2 w2) (and (@sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@eq nat j2 (gen_linker i2))))) *)
          generalize (sss_output_fun step_Y_fun H2 H5); inversion 1.
(* Goal: @ex nat (fun i2 : nat => @ex state_X (fun v2 : state_X => and (simul v2 w3) (and (@sss_output X state_X step_X (@pair nat (list X) iP cP) (@pair nat state_X i1 v1) (@pair nat state_X i2 v2)) (@eq nat (gen_linker i3) (gen_linker i2))))) *)
          exists i3, v3; auto.
  Qed.

End comp.
